X✝ : Type ?u.22569
Y : Type ?u.22572
Z : Type ?u.22575
α : Type ?u.22578
inst✝¹ : TopologicalSpace X✝
X : Type u_1
inst✝ : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h : ∀ (x : X), ↑f x = 0 ↔ ↑g x = 0
⊢ f = g
X✝ : Type ?u.22569
Y : Type ?u.22572
Z : Type ?u.22575
α : Type ?u.22578
inst✝¹ : TopologicalSpace X✝
X : Type u_1
inst✝ : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h : ↑f ⁻¹' {0} = ↑g ⁻¹' {0}
⊢ f = g
simp only [Set.ext_iff, mem_singleton_iff, mem_preimage] at h
case h
X✝ : Type ?u.22569
Y : Type ?u.22572
Z : Type ?u.22575
α : Type ?u.22578
inst✝¹ : TopologicalSpace X✝
X : Type u_1
inst✝ : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h : ∀ (x : X), ↑f x = 0 ↔ ↑g x = 0
x : X
⊢ ↑f x = ↑g x
X✝ : Type ?u.22569
Y : Type ?u.22572
Z : Type ?u.22575
α : Type ?u.22578
inst✝¹ : TopologicalSpace X✝
X : Type u_1
inst✝ : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h : ∀ (x : X), ↑f x = 0 ↔ ↑g x = 0
⊢ f = g
ext1 x
no goals
case h
X✝ : Type ?u.22569
Y : Type ?u.22572
Z : Type ?u.22575
α : Type ?u.22578
inst✝¹ : TopologicalSpace X✝
X : Type u_1
inst✝ : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h : ∀ (x : X), ↑f x = 0 ↔ ↑g x = 0
x : X
⊢ ↑f x = ↑g x
exact Fin.fin_two_eq_of_eq_zero_iff (h x)