no goals
C : Type u₁
inst✝⁴ : Category C
X Y Z : C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
x : β
h : ↑e.symm x ∈ s
⊢ ↑e (↑e.symm x) = x
simp
case intro.intro
C : Type u₁
inst✝⁴ : Category C
X Y Z : C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
a : α
m : a ∈ s
⊢ ↑e.symm (↑e a) ∈ s
C : Type u₁
inst✝⁴ : Category C
X Y Z : C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
x : β
⊢ x ∈ ↑e '' s → ↑e.symm x ∈ s
rintro ⟨a, m, rfl⟩
no goals
case intro.intro
C : Type u₁
inst✝⁴ : Category C
X Y Z : C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
a : α
m : a ∈ s
⊢ ↑e.symm (↑e a) ∈ s
simpa using m