case h.e'_2.h.e'_4.h
α : Type u_3
β : Type ?u.61579
β₂ : Type ?u.61582
γ : Type ?u.61585
ι : Sort u_1
ι' : Sort u_2
κ : ι → Sort ?u.61596
κ' : ι' → Sort ?u.61601
inst✝ : SupSet α
f g✝ : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
x✝ : ι
⊢ f x✝ = g (h x✝)
α : Type u_3
β : Type ?u.61579
β₂ : Type ?u.61582
γ : Type ?u.61585
ι : Sort u_1
ι' : Sort u_2
κ : ι → Sort ?u.61596
κ' : ι' → Sort ?u.61601
inst✝ : SupSet α
f g✝ : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
⊢ (⨆ (x : ι), f x) = ⨆ (y : ι'), g y
convert h1.iSup_comp g
no goals
case h.e'_2.h.e'_4.h
α : Type u_3
β : Type ?u.61579
β₂ : Type ?u.61582
γ : Type ?u.61585
ι : Sort u_1
ι' : Sort u_2
κ : ι → Sort ?u.61596
κ' : ι' → Sort ?u.61601
inst✝ : SupSet α
f g✝ : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
x✝ : ι
⊢ f x✝ = g (h x✝)
exact (h2 _).symm