awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
R : Type u_2
inst_2 : DivisionSemiring R
inst_3 : PartialOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : PosMulReflectLT R
inst_6 : TopologicalSpace R
inst_7 : ContinuousInv₀ R
refine :
  Continuous (Y := { r : R // 0 ≤ r }) fun (x : { r : R // 0 < r }) ↦
    (↑((Equiv.invFun (MulEquiv.toEquiv (unitsEquivPos R)) x)⁻¹ : { r : R // 0 ≤ r }ˣ) : { r : R // 0 ≤ r })
⊢ Continuous (X := { r : R // 0 < r })
      (Function.comp (β := { r : R // 0 ≤ r }ˣ) (Units.val : (self : { r : R // 0 ≤ r }ˣ) → { r : R // 0 ≤ r })
        (Equiv.invFun (MulEquiv.toEquiv (unitsEquivPos R)) : { r : R // 0 < r } → { r : R // 0 ≤ r }ˣ)) ∧
    Continuous (Y := { r : R // 0 ≤ r }) fun (x : { r : R // 0 < r }) ↦
      (↑((Equiv.invFun (MulEquiv.toEquiv (unitsEquivPos R)) x)⁻¹ : { r : R // 0 ≤ r }ˣ) : { r : R // 0 ≤ r })

Tactic:
refine ⟨by fun_prop, ?_⟩
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
R : Type u_2
inst_2 : DivisionSemiring R
inst_3 : PartialOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : PosMulReflectLT R
inst_6 : TopologicalSpace R
inst_7 : ContinuousInv₀ R
this : Continuous (Y := R) fun (x : { r : R // 0 < r }) ↦ (↑x : R)⁻¹
⊢ Continuous (Y := { r : R // 0 ≤ r }) fun (x : { r : R // 0 < r }) ↦
    (↑((Equiv.invFun (MulEquiv.toEquiv (unitsEquivPos R)) x)⁻¹ : { r : R // 0 ≤ r }ˣ) : { r : R // 0 ≤ r })

Tactic:
simpa [Topology.IsEmbedding.subtypeVal.continuous_iff, Function.comp_def]

Premises used: Function.comp_def, Topology.IsEmbedding.subtypeVal, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
R : Type u_2
inst_2 : DivisionSemiring R
inst_3 : PartialOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : PosMulReflectLT R
inst_6 : TopologicalSpace R
inst_7 : ContinuousInv₀ R
suffices : Continuous (Y := R) fun (x : { r : R // 0 < r }) ↦ (↑x : R)⁻¹
⊢ Continuous (Y := { r : R // 0 ≤ r }) fun (x : { r : R // 0 < r }) ↦
    (↑((Equiv.invFun (MulEquiv.toEquiv (unitsEquivPos R)) x)⁻¹ : { r : R // 0 ≤ r }ˣ) : { r : R // 0 ≤ r })

Tactic:
suffices Continuous fun (x : { r : R // 0 < r }) ↦ (x⁻¹ : R) by
      simpa [Topology.IsEmbedding.subtypeVal.continuous_iff, Function.comp_def]
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
R : Type u_2
inst_2 : DivisionSemiring R
inst_3 : PartialOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : PosMulReflectLT R
inst_6 : TopologicalSpace R
inst_7 : ContinuousInv₀ R
rw : ∀ (x : { r : R // 0 < r }), ContinuousAt (Y := R) (fun (x : { r : R // 0 < r }) ↦ (↑x : R)⁻¹) x
⊢ Continuous (Y := R) fun (x : { r : R // 0 < r }) ↦ (↑x : R)⁻¹

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
R : Type u_2
inst_2 : DivisionSemiring R
inst_3 : PartialOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : PosMulReflectLT R
inst_6 : TopologicalSpace R
inst_7 : ContinuousInv₀ R
x : { r : R // 0 < r }
⊢ ContinuousAt (Subtype.val (p := fun (r : R) ↦ 0 < r)) x

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
R : Type u_2
inst_2 : DivisionSemiring R
inst_3 : PartialOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : PosMulReflectLT R
inst_6 : TopologicalSpace R
inst_7 : ContinuousInv₀ R
⊢ ∀ (x : { r : R // 0 < r }), ContinuousAt (Y := R) (fun (x : { r : R // 0 < r }) ↦ (↑x : R)⁻¹) x

Tactic:
exact fun x ↦ ContinuousAt.inv₀ (by fun_prop) x.2.ne'

Premises used: ContinuousAt.inv₀
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b : 𝕜
h : a ≠ 0
x : 𝕜
simp : a * x / a = x
⊢ (fun (y : 𝕜) ↦ (y - b) / a) ((fun (x : 𝕜) ↦ a * x + b) x) = x

Tactic:
simp only [add_sub_cancel_right]

Premises used: add_sub_cancel_right
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b : 𝕜
h : a ≠ 0
x : 𝕜
⊢ a * x / a = x

Tactic:
mul_div_cancel_left₀ x h

Premises used: mul_div_cancel_left₀
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b : 𝕜
h : a ≠ 0
x : 𝕜
⊢ a * x / a = x

Tactic:
exact mul_div_cancel_left₀ x h

Premises used: mul_div_cancel_left₀
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b : 𝕜
h : a ≠ 0
y : 𝕜
⊢ (fun (x : 𝕜) ↦ a * x + b) ((fun (y : 𝕜) ↦ (y - b) / a) y) = y

Tactic:
simp [mul_div_cancel₀ _ h]

Premises used: mul_div_cancel₀
-- Module: Mathlib.Topology.Algebra.Field
Goal:
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b c d : 𝕜
h : 0 < a
⊢ (⇑(affineHomeomorph a b ⋯) : (a : 𝕜) → 𝕜) '' Set.Icc c d = Set.Icc (a * c + b) (a * d + b)

Tactic:
simp [h]
-- Module: Mathlib.Topology.Algebra.Field
Goal:
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b c d : 𝕜
h : 0 < a
⊢ (⇑(affineHomeomorph a b ⋯) : (a : 𝕜) → 𝕜) '' Set.Ico c d = Set.Ico (a * c + b) (a * d + b)

Tactic:
simp [h]
-- Module: Mathlib.Topology.Algebra.Field
Goal:
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b c d : 𝕜
h : 0 < a
⊢ (⇑(affineHomeomorph a b ⋯) : (a : 𝕜) → 𝕜) '' Set.Ioc c d = Set.Ioc (a * c + b) (a * d + b)

Tactic:
simp [h]
-- Module: Mathlib.Topology.Algebra.Field
Goal:
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b c d : 𝕜
h : 0 < a
⊢ (⇑(affineHomeomorph a b ⋯) : (a : 𝕜) → 𝕜) '' Set.Ioo c d = Set.Ioo (a * c + b) (a * d + b)

Tactic:
simp [h]
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Semifield β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
f : α → β
a : α
h1 : IsLocalMin f a
h2 : ∀ᶠ (z : α) in 𝓝 a, 0 < f z
z : α
h3 : f a ≤ f z
h4 : 0 < f z
⊢ f⁻¹ z ≤ f⁻¹ a

Tactic:
(inv_le_inv₀ h4 h2.self_of_nhds).mpr h3

Premises used: Iff.mpr, Filter.Eventually.self_of_nhds, inv_le_inv₀
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Semifield β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
f : α → β
a : α
h1 : IsLocalMin f a
h2 : ∀ᶠ (z : α) in 𝓝 a, 0 < f z
h :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f a ≤ f x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (z : α) ↦ 0 < f z) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f⁻¹ x ≤ f⁻¹ a) x} x}
            x}
      a_1
h₁ h₂ : ∀ (z : α) (h3 : f a ≤ f z) (h4 : 0 < f z), f⁻¹ z ≤ f⁻¹ a
⊢ IsLocalMax f⁻¹ a

Tactic:
filter_upwards [h1, h2] with z h3 h4 using (inv_le_inv₀ h4 h2.self_of_nhds).mpr h3
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
𝕜 : Type u_3
f : α → 𝕜
S : Set α
inst : TopologicalSpace α
inst_1 : TopologicalSpace 𝕜
inst_2 : T1Space 𝕜
inst_3 : Ring 𝕜
inst_4 : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (HPow.hPow (β := ℕ) f 2) 1 S
⊢ MapsTo f S {1, -1}

Tactic:
simpa only [EqOn, Pi.one_apply, Pi.pow_apply, sq_eq_one_iff] using hsq

Premises used: sq_eq_one_iff, Pi.one_apply, Set.EqOn, Pi.pow_apply
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
𝕜 : Type u_3
f : α → 𝕜
S : Set α
inst : TopologicalSpace α
inst_1 : TopologicalSpace 𝕜
inst_2 : T1Space 𝕜
inst_3 : Ring 𝕜
inst_4 : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (HPow.hPow (β := ℕ) f 2) 1 S
⊢ MapsTo f S {1, -1}

Tactic:
have hmaps : MapsTo f S {1, -1} := by
    simpa only [EqOn, Pi.one_apply, Pi.pow_apply, sq_eq_one_iff] using hsq
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
𝕜 : Type u_3
f : α → 𝕜
S : Set α
inst : TopologicalSpace α
inst_1 : TopologicalSpace 𝕜
inst_2 : T1Space 𝕜
inst_3 : Ring 𝕜
inst_4 : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (HPow.hPow (β := ℕ) f 2) 1 S
hmaps : MapsTo f S {1, -1}
⊢ EqOn f 1 S ∨ EqOn f (-1) S

Tactic:
simpa using hS.eqOn_const_of_mapsTo (toFinite _).isDiscrete hf hmaps

Premises used: IsPreconnected.eqOn_const_of_mapsTo, Set.Finite.isDiscrete, Set.toFinite
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst : TopologicalSpace α
inst_1 : TopologicalSpace 𝕜
inst_2 : T1Space 𝕜
inst_3 : Field 𝕜
inst_4 : ContinuousInv₀ 𝕜
inst_5 : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (HPow.hPow (β := ℕ) f 2) (HPow.hPow (β := ℕ) g 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
x : α
hx : x ∈ S
⊢ HPow.hPow (β := ℕ) (f / g) 2 x = 1 x

Tactic:
simpa [div_eq_one_iff_eq (pow_ne_zero _ (hg_ne hx)), div_pow] using hsq hx

Premises used: div_eq_one_iff_eq, pow_ne_zero, div_pow
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst : TopologicalSpace α
inst_1 : TopologicalSpace 𝕜
inst_2 : T1Space 𝕜
inst_3 : Field 𝕜
inst_4 : ContinuousInv₀ 𝕜
inst_5 : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (HPow.hPow (β := ℕ) f 2) (HPow.hPow (β := ℕ) g 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
⊢ EqOn (HPow.hPow (β := ℕ) (f / g) 2) 1 S

Tactic:
have hsq : EqOn ((f / g) ^ 2) 1 S := fun x hx => by
    simpa [div_eq_one_iff_eq (pow_ne_zero _ (hg_ne hx)), div_pow] using hsq hx
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst : TopologicalSpace α
inst_1 : TopologicalSpace 𝕜
inst_2 : T1Space 𝕜
inst_3 : Field 𝕜
inst_4 : ContinuousInv₀ 𝕜
inst_5 : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq_1 : EqOn (HPow.hPow (β := ℕ) f 2) (HPow.hPow (β := ℕ) g 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
hsq : EqOn (HPow.hPow (β := ℕ) (f / g) 2) 1 S
⊢ EqOn f g S ∨ EqOn f (-g) S

Tactic:
simpa +contextual [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

Premises used: ContinuousOn.div, Set.EqOn, IsPreconnected.eq_one_or_eq_neg_one_of_sq_eq, div_eq_iff
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst : TopologicalSpace α
inst_1 : TopologicalSpace 𝕜
inst_2 : T1Space 𝕜
inst_3 : Field 𝕜
inst_4 : ContinuousInv₀ 𝕜
inst_5 : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (HPow.hPow (β := ℕ) f 2) (HPow.hPow (β := ℕ) g 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
inl : ∀ (h : EqOn f g S), f x = g x
inr : ∀ (h : EqOn f (-g) S), f x = g x
⊢ f x = g x

Tactic:
rcases hS.eq_or_eq_neg_of_sq_eq hf hg @hsq @hg_ne with (h | h)

Premises used: IsPreconnected.eq_or_eq_neg_of_sq_eq
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst : TopologicalSpace α
inst_1 : TopologicalSpace 𝕜
inst_2 : T1Space 𝕜
inst_3 : Field 𝕜
inst_4 : ContinuousInv₀ 𝕜
inst_5 : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (HPow.hPow (β := ℕ) f 2) (HPow.hPow (β := ℕ) 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

Tactic:
h hx
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst : TopologicalSpace α
inst_1 : TopologicalSpace 𝕜
inst_2 : T1Space 𝕜
inst_3 : Field 𝕜
inst_4 : ContinuousInv₀ 𝕜
inst_5 : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (HPow.hPow (β := ℕ) f 2) (HPow.hPow (β := ℕ) 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

Tactic:
exact h hx
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst : TopologicalSpace α
inst_1 : TopologicalSpace 𝕜
inst_2 : T1Space 𝕜
inst_3 : Field 𝕜
inst_4 : ContinuousInv₀ 𝕜
inst_5 : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (HPow.hPow (β := ℕ) f 2) (HPow.hPow (β := ℕ) 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
inr :
  ∀ (hy' : Eq.{u_3 + 1} (α := 𝕜) 2 0 ∨ False) (x : α) (hx : x ∈ S) (h : EqOn f (-g) S),
    Eq.{u_3 + 1} (α := 𝕜) 2 0 ∨ False
rw : ∀ (hy' : Eq.{u_3 + 1} (α := 𝕜) 2 0 ∨ False) (x : α) (hx : x ∈ S) (h : EqOn f (-g) S), x ∈ S
rw₁ : ∀ (hy' : Eq.{u_3 + 1} (α := 𝕜) 2 0 ∨ g y = 0) (x : α) (hx : x ∈ S) (h : EqOn f (-g) S), y ∈ S
rw₂ : ∀ (hy' : (-g) y = g y) (x : α) (hx : x ∈ S) (h : EqOn f (-g) S), x ∈ S
rw₃ : y ∈ S
⊢ f x = g x

Tactic:
rw [h _, Pi.neg_apply, neg_eq_iff_add_eq_zero, ← two_mul, mul_eq_zero,
      (iff_of_eq (iff_false _)).2 (hg_ne _)] at hy' ⊢

Premises used: Iff.mpr, iff_false, neg_eq_iff_add_eq_zero, two_mul, mul_eq_zero, Pi.neg_apply, iff_of_eq
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst : TopologicalSpace α
inst_1 : TopologicalSpace 𝕜
inst_2 : T1Space 𝕜
inst_3 : Field 𝕜
inst_4 : ContinuousInv₀ 𝕜
inst_5 : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (HPow.hPow (β := ℕ) f 2) (HPow.hPow (β := ℕ) g 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : Eq.{u_3 + 1} (α := 𝕜) 2 0 ∨ False
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ Eq.{u_3 + 1} (α := 𝕜) 2 0 ∨ False

Tactic:
assumption
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst : TopologicalSpace α
inst_1 : TopologicalSpace 𝕜
inst_2 : T1Space 𝕜
inst_3 : Field 𝕜
inst_4 : ContinuousInv₀ 𝕜
inst_5 : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (HPow.hPow (β := ℕ) f 2) (HPow.hPow (β := ℕ) g 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : Eq.{u_3 + 1} (α := 𝕜) 2 0 ∨ False
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ x ∈ S

Tactic:
assumption
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst : TopologicalSpace α
inst_1 : TopologicalSpace 𝕜
inst_2 : T1Space 𝕜
inst_3 : Field 𝕜
inst_4 : ContinuousInv₀ 𝕜
inst_5 : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (HPow.hPow (β := ℕ) f 2) (HPow.hPow (β := ℕ) g 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : Eq.{u_3 + 1} (α := 𝕜) 2 0 ∨ g y = 0
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ y ∈ S

Tactic:
assumption
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst : TopologicalSpace α
inst_1 : TopologicalSpace 𝕜
inst_2 : T1Space 𝕜
inst_3 : Field 𝕜
inst_4 : ContinuousInv₀ 𝕜
inst_5 : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (HPow.hPow (β := ℕ) f 2) (HPow.hPow (β := ℕ) 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

Tactic:
assumption
-- Module: Mathlib.Topology.Algebra.Field
Goal:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst : TopologicalSpace α
inst_1 : TopologicalSpace 𝕜
inst_2 : T1Space 𝕜
inst_3 : Field 𝕜
inst_4 : ContinuousInv₀ 𝕜
inst_5 : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (HPow.hPow (β := ℕ) f 2) (HPow.hPow (β := ℕ) 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

Tactic:
assumption
-- Module: Mathlib.Topology.Algebra.Field
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : TopologicalSpace K
F : Type u_2
inst_2 : DivisionRing F
inst_3 : TopologicalSpace F
inst_4 : IsTopologicalRing F
X : Type u_3
inst_5 : TopologicalSpace X
inst_6 : MulAction F X
inst_7 : ContinuousSMul F X
M : Subfield F
⊢ ContinuousSMul.{u_2, u_3} (↥M) X

Tactic:
Subring.continuousSMul M.toSubring X

Premises used: Set.Mem, Subring.continuousSMul, Subfield.toSubring
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u_1
inst : CommGroup G
sets : Set (Set G)
nonempty : sets.Nonempty
inter_sets : ∀ (x y : Set G), x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y
one : ∀ U ∈ sets, 1 ∈ U
mul : ∀ U ∈ sets, ∃ V ∈ sets, V * V ⊆ U
inv : ∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (fun (x : G) ↦ x⁻¹) ⁻¹' U
x : G
U : Set G
U_in : U ∈ sets
simp : U ⊆ U
⊢ U ⊆ (fun (x_1 : G) ↦ x * x_1 * x⁻¹) ⁻¹' U

Tactic:
simp only [mul_inv_cancel_comm, preimage_id']

Premises used: mul_inv_cancel_comm, Set.preimage_id'
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u_1
inst : CommGroup G
sets : Set (Set G)
nonempty : sets.Nonempty
inter_sets : ∀ (x y : Set G), x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y
one : ∀ U ∈ sets, 1 ∈ U
mul : ∀ U ∈ sets, ∃ V ∈ sets, V * V ⊆ U
inv : ∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (fun (x : G) ↦ x⁻¹) ⁻¹' U
x : G
U : Set G
U_in : U ∈ sets
⊢ U ⊆ U

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
U : Set G
⊢ U ∈ B → 1 ∈ U

Tactic:
GroupFilterBasis.one'

Premises used: GroupFilterBasis.one'
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
U : Set G
⊢ U ∈ B → ∃ V ∈ B, V * V ⊆ U

Tactic:
GroupFilterBasis.mul'

Premises used: GroupFilterBasis.mul'
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
U : Set G
⊢ U ∈ B → ∃ V ∈ B, V ⊆ (fun (x : G) ↦ x⁻¹) ⁻¹' U

Tactic:
GroupFilterBasis.inv'

Premises used: GroupFilterBasis.inv'
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
⊢ ∀ (x₀ : G) {U : Set G}, U ∈ B → ∃ V ∈ B, V ⊆ (fun (x : G) ↦ x₀ * x * x₀⁻¹) ⁻¹' U

Tactic:
GroupFilterBasis.conj'

Premises used: GroupFilterBasis.conj'
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
⊢ ∀ {x y : Set G},
    Membership.mem (γ := Set (Set G)) {{1}} x →
      Membership.mem (γ := Set (Set G)) {{1}} y → ∃ (z : Set G), Membership.mem (γ := Set (Set G)) {{1}} z ∧ z ⊆ x ∩ y

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G}, Membership.mem (γ := Set (Set G)) {{1}} U → 1 ∈ U

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G},
    Membership.mem (γ := Set (Set G)) {{1}} U → ∃ (V : Set G), Membership.mem (γ := Set (Set G)) {{1}} V ∧ V * V ⊆ U

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G},
    Membership.mem (γ := Set (Set G)) {{1}} U →
      ∃ (V : Set G), Membership.mem (γ := Set (Set G)) {{1}} V ∧ V ⊆ (fun (x : G) ↦ x⁻¹) ⁻¹' U

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
⊢ ∀ (x₀ : G) {U : Set G},
    Membership.mem (γ := Set (Set G)) {{1}} U →
      ∃ (V : Set G), Membership.mem (γ := Set (Set G)) {{1}} V ∧ V ⊆ (fun (x : G) ↦ x₀ * x * x₀⁻¹) ⁻¹' U

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
U : Set G
h : U ∈ B
⊢ U ⊆ U * U

Tactic:
fun x x_in ↦ ⟨1, one h, x, x_in, one_mul x⟩

Premises used: GroupFilterBasis.one, Set.Mem, setOf, Set.Subset, Set.image2, And.intro, Exists.intro, OfNat.ofNat, one_mul
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
⊢ B.N 1 = FilterBasis.filter (@toFilterBasis _ inst _)

Tactic:
simp only [N, one_mul, map_id']

Premises used: GroupFilterBasis.N, Filter.map_id', one_mul
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
x : G
⊢ (B.N x).HasBasis (fun (V : Set G) ↦ V ∈ B) fun (V : Set G) ↦ (fun (y : G) ↦ x * y) '' V

Tactic:
HasBasis.map (fun y ↦ x * y) toFilterBasis.hasBasis

Premises used: HMul.hMul, FilterBasis.hasBasis, GroupFilterBasis.N, Filter.HasBasis.map, GroupFilterBasis.toFilterBasis
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
x₀ : G
hpure :
  ∀ (a : G) (i : Set G),
    Membership.mem (γ := FilterBasis G) (@toFilterBasis _ inst _) i →
      Membership.mem (γ := Set G) ((fun (y : G) ↦ a * y) '' id i) a
hopen :
  ∀ (a : G) (i : Set G),
    Membership.mem (γ := FilterBasis G) (@toFilterBasis _ inst _) i →
      ∀ᶠ (x : G) in map (fun (y : G) ↦ a * y) (FilterBasis.filter (@toFilterBasis _ inst _)),
        Membership.mem (γ := Filter G) (map (fun (y : G) ↦ x * y) (FilterBasis.filter (@toFilterBasis _ inst _)))
          ((fun (y : G) ↦ a * y) '' id i)
⊢ 𝓝 x₀ = B.N x₀

Tactic:
apply TopologicalSpace.nhds_mkOfNhds_of_hasBasis (fun x ↦ (FilterBasis.hasBasis _).map _)

Premises used: FilterBasis.hasBasis, Filter.HasBasis.map, TopologicalSpace.nhds_mkOfNhds_of_hasBasis
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : Membership.mem (γ := FilterBasis G) (@toFilterBasis _ inst _) U
⊢ Membership.mem (γ := Set G) ((fun (y : G) ↦ a * y) '' id U) a

Tactic:
⟨1, B.one U_in, mul_one a⟩

Premises used: GroupFilterBasis.one, Set.Mem, setOf, And.intro, Exists.intro, Set.image, mul_one, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : Membership.mem (γ := FilterBasis G) (@toFilterBasis _ inst _) U
⊢ Membership.mem (γ := Set G) ((fun (y : G) ↦ a * y) '' id U) a

Tactic:
exact ⟨1, B.one U_in, mul_one a⟩
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : Membership.mem (γ := FilterBasis G) (@toFilterBasis _ inst _) U
hopen :
  ∀ (V : Set G) (V_in : V ∈ B) (hVU : V * V ⊆ U),
    ∀ᶠ (x : G) in map (fun (y : G) ↦ a * y) (FilterBasis.filter (@toFilterBasis _ inst _)),
      Membership.mem (γ := Filter G) (map (fun (y : G) ↦ x * y) (FilterBasis.filter (@toFilterBasis _ inst _)))
        ((fun (y : G) ↦ a * y) '' id U)
⊢ ∀ᶠ (x : G) in map (fun (y : G) ↦ a * y) (FilterBasis.filter (@toFilterBasis _ inst _)),
    Membership.mem (γ := Filter G) (map (fun (y : G) ↦ x * y) (FilterBasis.filter (@toFilterBasis _ inst _)))
      ((fun (y : G) ↦ a * y) '' id U)

Tactic:
rcases GroupFilterBasis.mul U_in with ⟨V, V_in, hVU⟩

Premises used: GroupFilterBasis.mul
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : Membership.mem (γ := FilterBasis G) (@toFilterBasis _ inst _) U
V : Set G
V_in : V ∈ B
hVU : V * V ⊆ U
h :
  ∀ (a_1 : G),
    Membership.mem (γ := Set G) ((fun (y : G) ↦ a * y) '' V) a_1 →
      Membership.mem (γ := Filter G) (map (fun (y : G) ↦ a_1 * y) (FilterBasis.filter (@toFilterBasis _ inst _)))
        ((fun (y : G) ↦ a * y) '' id U)
⊢ ∀ᶠ (x : G) in map (fun (y : G) ↦ a * y) (FilterBasis.filter (@toFilterBasis _ inst _)),
    Membership.mem (γ := Filter G) (map (fun (y : G) ↦ x * y) (FilterBasis.filter (@toFilterBasis _ inst _)))
      ((fun (y : G) ↦ a * y) '' id U)

Tactic:
filter_upwards [image_mem_map (B.mem_filter_of_mem V_in)]

Premises used: FilterBasis.mem_filter_of_mem, Filter.image_mem_map, GroupFilterBasis.toFilterBasis