[GOAL]
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalDivisionRing α
K : Subfield α
src✝ : Subring α := Subring.topologicalClosure K.toSubring
x : α
hx :
  x ∈
    {
              toSubsemiring :=
                {
                  toSubmonoid :=
                    {
                      toSubsemigroup :=
                        { carrier := _root_.closure ↑K,
                          mul_mem' := (_ : ∀ {a b : α}, a ∈ src✝.carrier → b ∈ src✝.carrier → a * b ∈ src✝.carrier) },
                      one_mem' := (_ : 1 ∈ src✝.carrier) },
                  add_mem' := (_ : ∀ {a b : α}, a ∈ src✝.carrier → b ∈ src✝.carrier → a + b ∈ src✝.carrier),
                  zero_mem' := (_ : 0 ∈ src✝.carrier) },
              neg_mem' :=
                (_ : ∀ {x : α}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
⊢ x⁻¹ ∈
    {
              toSubsemiring :=
                {
                  toSubmonoid :=
                    {
                      toSubsemigroup :=
                        { carrier := _root_.closure ↑K,
                          mul_mem' := (_ : ∀ {a b : α}, a ∈ src✝.carrier → b ∈ src✝.carrier → a * b ∈ src✝.carrier) },
                      one_mem' := (_ : 1 ∈ src✝.carrier) },
                  add_mem' := (_ : ∀ {a b : α}, a ∈ src✝.carrier → b ∈ src✝.carrier → a + b ∈ src✝.carrier),
                  zero_mem' := (_ : 0 ∈ src✝.carrier) },
              neg_mem' :=
                (_ : ∀ {x : α}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
[PROOFSTEP]
dsimp only at hx ⊢
[GOAL]
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalDivisionRing α
K : Subfield α
src✝ : Subring α := Subring.topologicalClosure K.toSubring
x : α
hx : x ∈ _root_.closure ↑K
⊢ x⁻¹ ∈ _root_.closure ↑K
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | h)
[GOAL]
case inl
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalDivisionRing α
K : Subfield α
src✝ : Subring α := Subring.topologicalClosure K.toSubring
hx : 0 ∈ _root_.closure ↑K
⊢ 0⁻¹ ∈ _root_.closure ↑K
[PROOFSTEP]
rwa [inv_zero]
[GOAL]
case inr
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalDivisionRing α
K : Subfield α
src✝ : Subring α := Subring.topologicalClosure K.toSubring
x : α
hx : x ∈ _root_.closure ↑K
h : x ≠ 0
⊢ x⁻¹ ∈ _root_.closure ↑K
[PROOFSTEP]
rw [← @inv_coe_set α (Subfield α) _ _ SubfieldClass.toInvMemClass K, ← Set.image_inv]
[GOAL]
case inr
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalDivisionRing α
K : Subfield α
src✝ : Subring α := Subring.topologicalClosure K.toSubring
x : α
hx : x ∈ _root_.closure ↑K
h : x ≠ 0
⊢ x⁻¹ ∈ _root_.closure (Inv.inv '' ↑K)
[PROOFSTEP]
exact mem_closure_image (continuousAt_inv₀ h) hx
[GOAL]
K : Type u_1
inst✝⁴ : DivisionRing K
inst✝³ : TopologicalSpace K
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : a ≠ 0
x : 𝕜
⊢ (fun y => (y - b) / a) ((fun x => a * x + b) x) = x
[PROOFSTEP]
simp only [add_sub_cancel]
[GOAL]
K : Type u_1
inst✝⁴ : DivisionRing K
inst✝³ : TopologicalSpace K
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : a ≠ 0
x : 𝕜
⊢ a * x / a = x
[PROOFSTEP]
exact mul_div_cancel_left x h
[GOAL]
K : Type u_1
inst✝⁴ : DivisionRing K
inst✝³ : TopologicalSpace K
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : TopologicalRing 𝕜
a b : 𝕜
h : a ≠ 0
y : 𝕜
⊢ (fun x => a * x + b) ((fun y => (y - b) / a) y) = y
[PROOFSTEP]
simp [mul_div_cancel' _ h]
[GOAL]
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : TopologicalSpace K
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedSemifield β
a✝ : α
f : α → β
a : α
h1 : IsLocalMin f a
h2 : ∀ᶠ (z : α) in 𝓝 a, 0 < f z
⊢ IsLocalMax f⁻¹ a
[PROOFSTEP]
filter_upwards [h1, h2] with z h3 h4 using (inv_le_inv h4 h2.self_of_nhds).mpr h3
[GOAL]
K : Type u_1
inst✝⁶ : DivisionRing K
inst✝⁵ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
⊢ EqOn f 1 S ∨ EqOn f (-1) S
[PROOFSTEP]
have : DiscreteTopology ({1, -1} : Set 𝕜) := discrete_of_t1_of_finite
[GOAL]
K : Type u_1
inst✝⁶ : DivisionRing K
inst✝⁵ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
this : DiscreteTopology ↑{1, -1}
⊢ EqOn f 1 S ∨ EqOn f (-1) S
[PROOFSTEP]
have hmaps : MapsTo f S {1, -1}
[GOAL]
case hmaps
K : Type u_1
inst✝⁶ : DivisionRing K
inst✝⁵ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
this : DiscreteTopology ↑{1, -1}
⊢ MapsTo f S {1, -1}
[PROOFSTEP]
simpa only [EqOn, Pi.one_apply, Pi.pow_apply, sq_eq_one_iff] using hsq
[GOAL]
K : Type u_1
inst✝⁶ : DivisionRing K
inst✝⁵ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
this : DiscreteTopology ↑{1, -1}
hmaps : MapsTo f S {1, -1}
⊢ EqOn f 1 S ∨ EqOn f (-1) S
[PROOFSTEP]
simpa using hS.eqOn_const_of_mapsTo hf hmaps
[GOAL]
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
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
[PROOFSTEP]
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
[GOAL]
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
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
[PROOFSTEP]
simpa [div_eq_one_iff_eq (pow_ne_zero _ (hg_ne hx))] using hsq hx
[GOAL]
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
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
[PROOFSTEP]
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
[GOAL]
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
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
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
⊢ f x = g x
[PROOFSTEP]
rcases hS.eq_or_eq_neg_of_sq_eq hf hg @hsq @hg_ne with (h | h)
[GOAL]
case inl
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
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
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f g S
⊢ f x = g x
[PROOFSTEP]
exact h hx
[GOAL]
case inr
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
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
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ f x = g x
[PROOFSTEP]
rw [h _, Pi.neg_apply, neg_eq_iff_add_eq_zero, ← two_mul, mul_eq_zero, iff_false_iff.2 (hg_ne _)] at hy' ⊢
[GOAL]
case inr
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
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
y : α
hy : y ∈ S
hy' : 2 = 0 ∨ False
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ 2 = 0 ∨ False
[PROOFSTEP]
assumption
[GOAL]
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
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
y : α
hy : y ∈ S
hy' : 2 = 0 ∨ False
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ x ∈ S
[PROOFSTEP]
assumption
[GOAL]
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
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
y : α
hy : y ∈ S
hy' : 2 = 0 ∨ g y = 0
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ y ∈ S
[PROOFSTEP]
assumption
[GOAL]
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
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
y : α
hy : y ∈ S
hy' : (-g) y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ x ∈ S
[PROOFSTEP]
assumption
[GOAL]
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_3
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
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ y ∈ S
[PROOFSTEP]
assumption
