case a
α : Type u_2
β : Type u_1
γ : Type ?u.98446
ι : Sort ?u.98449
ι' : Sort ?u.98452
f✝ : ι → α
s t : Set α
f : α → β
x : ↑(range f)
⊢ ↑(rangeFactorization f (rangeSplitting f x)) = ↑x
α : Type u_2
β : Type u_1
γ : Type ?u.98446
ι : Sort ?u.98449
ι' : Sort ?u.98452
f✝ : ι → α
s t : Set α
f : α → β
x : ↑(range f)
⊢ rangeFactorization f (rangeSplitting f x) = x
apply Subtype.ext
case a
α : Type u_2
β : Type u_1
γ : Type ?u.98446
ι : Sort ?u.98449
ι' : Sort ?u.98452
f✝ : ι → α
s t : Set α
f : α → β
x : ↑(range f)
⊢ f (rangeSplitting f x) = ↑x
case a
α : Type u_2
β : Type u_1
γ : Type ?u.98446
ι : Sort ?u.98449
ι' : Sort ?u.98452
f✝ : ι → α
s t : Set α
f : α → β
x : ↑(range f)
⊢ ↑(rangeFactorization f (rangeSplitting f x)) = ↑x
simp only [rangeFactorization_coe]
no goals
case a
α : Type u_2
β : Type u_1
γ : Type ?u.98446
ι : Sort ?u.98449
ι' : Sort ?u.98452
f✝ : ι → α
s t : Set α
f : α → β
x : ↑(range f)
⊢ f (rangeSplitting f x) = ↑x
apply apply_rangeSplitting