α : Type u_3
β : Type ?u.60572
β₂ : Type ?u.60575
γ : Type ?u.60578
ι : Sort u_1
ι' : Sort u_2
κ : ι → Sort ?u.60589
κ' : ι' → Sort ?u.60594
inst✝ : SupSet α
f✝ g✝ : ι → α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ sSup (range fun x => g (f x)) = sSup (range fun y => g y)
α : Type u_3
β : Type ?u.60572
β₂ : Type ?u.60575
γ : Type ?u.60578
ι : Sort u_1
ι' : Sort u_2
κ : ι → Sort ?u.60589
κ' : ι' → Sort ?u.60594
inst✝ : SupSet α
f✝ g✝ : ι → α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ (⨆ (x : ι), g (f x)) = ⨆ (y : ι'), g y
simp [iSup]
case e_a
α : Type u_3
β : Type ?u.60572
β₂ : Type ?u.60575
γ : Type ?u.60578
ι : Sort u_1
ι' : Sort u_2
κ : ι → Sort ?u.60589
κ' : ι' → Sort ?u.60594
inst✝ : SupSet α
f✝ g✝ : ι → α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ (range fun x => g (f x)) = range fun y => g y
α : Type u_3
β : Type ?u.60572
β₂ : Type ?u.60575
γ : Type ?u.60578
ι : Sort u_1
ι' : Sort u_2
κ : ι → Sort ?u.60589
κ' : ι' → Sort ?u.60594
inst✝ : SupSet α
f✝ g✝ : ι → α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ sSup (range fun x => g (f x)) = sSup (range fun y => g y)
congr
no goals
case e_a
α : Type u_3
β : Type ?u.60572
β₂ : Type ?u.60575
γ : Type ?u.60578
ι : Sort u_1
ι' : Sort u_2
κ : ι → Sort ?u.60589
κ' : ι' → Sort ?u.60594
inst✝ : SupSet α
f✝ g✝ : ι → α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ (range fun x => g (f x)) = range fun y => g y
exact hf.range_comp g