K : Type ?u.21895
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_1
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq✝ : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
hsq : EqOn ((f / g) ^ 2) 1 S
⊢ EqOn f g S ∨ EqOn f (-g) S
K : Type ?u.21895
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_1
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
⊢ EqOn f g S ∨ EqOn f (-g) S
have hsq : EqOn ((f / g) ^ 2) 1 S := fun x hx => by
  simpa [div_eq_one_iff_eq (pow_ne_zero _ (hg_ne hx))] using hsq hx
no goals
K : Type ?u.21895
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_1
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq✝ : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
hsq : EqOn ((f / g) ^ 2) 1 S
⊢ EqOn f g S ∨ EqOn f (-g) S
simpa (config := { contextual := true }) [EqOn, div_eq_iff (hg_ne _)]
  using hS.eq_one_or_eq_neg_one_of_sq_eq (hf.div hg fun z => hg_ne) hsq
no goals
K : Type ?u.21895
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_1
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
x : α
hx : x ∈ S
⊢ ((f / g) ^ 2) x = OfNat.ofNat 1 x
simpa [div_eq_one_iff_eq (pow_ne_zero _ (hg_ne hx))] using hsq hx