awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
M : Type u_1
N : Type u_2
inst_2 : TopologicalSpace M
inst_3 : TopologicalSpace N
inst_4 : Mul M
inst_5 : Mul N
g : M ≃ₜ* N
toMulEquiv : M ≃* N
continuous_toFun : Continuous toMulEquiv.toFun
continuous_invFun : Continuous toMulEquiv.invFun
h₁ :
  { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        M ≃ₜ* N }.toFun =
    g.toFun
h₂ :
  { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        M ≃ₜ* N }.invFun =
    g.invFun
⊢ { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun : M ≃ₜ* N } =
    g
have mk : ∀ (toMulEquiv_1 : M ≃* N) (continuous_toFun_1 : Continuous toMulEquiv_1.toFun)
  (continuous_invFun_1 : Continuous toMulEquiv_1.invFun)
  (h₁ :
    { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
          M ≃ₜ* N }.toFun =
      { toMulEquiv := toMulEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
          M ≃ₜ* N }.toFun)
  (h₂ :
    { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
          M ≃ₜ* N }.invFun =
      { toMulEquiv := toMulEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
          M ≃ₜ* N }.invFun),
  { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun : M ≃ₜ* N } =
    { toMulEquiv := toMulEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 }
Tactic: cases g
Cleared hypotheses: g, h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
M : Type u_1
N : Type u_2
inst_2 : TopologicalSpace M
inst_3 : TopologicalSpace N
inst_4 : Mul M
inst_5 : Mul N
toMulEquiv : M ≃* N
continuous_toFun : Continuous toMulEquiv.toFun
continuous_invFun : Continuous toMulEquiv.invFun
toMulEquiv_1 : M ≃* N
continuous_toFun_1 : Continuous toMulEquiv_1.toFun
continuous_invFun_1 : Continuous toMulEquiv_1.invFun
h₁ :
  { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        M ≃ₜ* N }.toFun =
    { toMulEquiv := toMulEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
        M ≃ₜ* N }.toFun
h₂ :
  { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun :
        M ≃ₜ* N }.invFun =
    { toMulEquiv := toMulEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 :
        M ≃ₜ* N }.invFun
⊢ { toMulEquiv := toMulEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun : M ≃ₜ* N } =
    { toMulEquiv := toMulEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 }
have mk : toMulEquiv = toMulEquiv_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
M : Type u_1
N : Type u_2
inst_2 : TopologicalSpace M
inst_3 : TopologicalSpace N
inst_4 : Mul M
inst_5 : Mul N
⊢ Continuous (MulEquiv.toEquiv (MulEquiv.refl M)).toFun
have dsimp : Continuous.{u_1, u_1} (X := M) id
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
M : Type u_1
N : Type u_2
inst_2 : TopologicalSpace M
inst_3 : TopologicalSpace N
inst_4 : Mul M
inst_5 : Mul N
⊢ Continuous (MulEquiv.toEquiv (MulEquiv.refl M)).invFun
have dsimp : Continuous.{u_1, u_1} (X := M) id
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousMonoidHom (goal)
Goal:
G : Type u
inst : TopologicalSpace G
H : Type v
inst_1 : TopologicalSpace H
inst_2 : Mul G
inst_3 : Mul H
e : G ≃* H
he : ∀ (s : Set H), IsOpen.{u} (X := G) ((⇑e : (a : G) → H) ⁻¹' s) ↔ IsOpen s
s : Set G
⊢ IsOpen.{v} (X := H) ((⇑e.symm : (a : H) → G) ⁻¹' s) ↔ IsOpen s
have h : s = Set.preimage.{u, v} (β := H) (⇑e : (a : G) → H) ((⇑e.symm : (a : H) → G) ⁻¹' s)
Tactic: convert! (he _).symm
-- Lean 4 proof step from Mathlib.Topology.Algebra.Equicontinuity (goal)
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : TopologicalSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsTopologicalGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt.{u_1, u_2, u_3} (X := G) (α := M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1
⊢ Equicontinuous.{u_1, u_2, u_3} (X := G) (α := M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)
have rw : Continuous (X := G) (Y := ι →ᵤ M)
  (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
    (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
Tactic: rw [equicontinuous_iff_continuous]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Equicontinuity (hypothesis)
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : TopologicalSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsTopologicalGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt.{u_1, u_2, u_3} (X := G) (α := M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1
⊢ Continuous (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
have hf₁ : ContinuousAt (X := G) (Y := ι →ᵤ M)
  (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
    (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
  1
Tactic: rw [equicontinuousAt_iff_continuousAt] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Equicontinuity (goal)
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : TopologicalSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsTopologicalGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
⊢ Eq (α := ι → M) (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1) 1
have h : ∀ (x : ι),
  Eq.{u_3 + 1} (α := M) (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1 x) (1 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Equicontinuity (goal)
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : TopologicalSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsTopologicalGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
a b : G
⊢ swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) (a * b) =
    HMul.hMul (α := ι → M) (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) a)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) b)
have h : ∀ (x : ι),
  swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) (a * b) x =
    HMul.hMul (α := ι → M) (β := ι → M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) a)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) b) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Equicontinuity (goal)
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : UniformSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsUniformGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt.{u_1, u_2, u_3} (X := G) (α := M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1
⊢ UniformEquicontinuous.{u_1, u_3, u_2} (α := M) (β := G) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)
have rw : UniformContinuous (α := G) (β := ι →ᵤ M)
  (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
    (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
Tactic: rw [uniformEquicontinuous_iff_uniformContinuous]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Equicontinuity (hypothesis)
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : UniformSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsUniformGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt.{u_1, u_2, u_3} (X := G) (α := M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1
⊢ UniformContinuous (α := G) (β := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
have hf₁ : ContinuousAt (X := G) (Y := ι →ᵤ M)
  (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
    (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
  1
Tactic: rw [equicontinuousAt_iff_continuousAt] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Equicontinuity (goal)
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : UniformSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsUniformGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
⊢ Eq (α := ι → M) (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1) 1
have h : ∀ (x : ι),
  Eq.{u_3 + 1} (α := M) (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) 1 x) (1 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Equicontinuity (goal)
Goal:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst : UniformSpace G
inst_1 : UniformSpace M
inst_2 : Group G
inst_3 : Group M
inst_4 : IsUniformGroup G
inst_5 : IsUniformGroup M
inst_6 : FunLike hom G M
inst_7 : MonoidHomClass hom G M
F : ι → hom
hf :
  ContinuousAt (X := G) (Y := ι →ᵤ M)
    (comp (β := ι → M) (⇑UniformFun.ofFun : (a : ι → M) → ι →ᵤ M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F)))
    1
a b : G
⊢ swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) (a * b) =
    HMul.hMul (α := ι → M) (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) a)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) b)
have h : ∀ (x : ι),
  swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) (a * b) x =
    HMul.hMul (α := ι → M) (β := ι → M)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) a)
      (swap (φ := fun (a : ι) (a_1 : G) ↦ M) (DFunLike.coe (β := fun (x : G) ↦ M) ∘ F) b) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
Goal:
K : Type u_2
inst : DivisionRing K
inst_1 : TopologicalSpace K
inst_2 : IsTopologicalRing K
inst_3 : CompactSpace K
inst_4 : T2Space K
⊢ Finite K
have suffices : DiscreteTopology K
Tactic: suffices DiscreteTopology K by
    exact finite_of_compact_of_discrete
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
Goal:
K : Type u_2
inst : DivisionRing K
inst_1 : TopologicalSpace K
inst_2 : IsTopologicalRing K
inst_3 : CompactSpace K
inst_4 : T2Space K
⊢ DiscreteTopology K
have rw : IsOpen (X := K) {0}
Tactic: rw [discreteTopology_iff_isOpen_singleton_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
Goal:
K_1 : Type u_1
inst : DivisionRing K_1
inst_1 : TopologicalSpace K_1
α : Type u_2
inst_2 : Field α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalDivisionRing α
K : Subfield α
x : α
hx : x ∈ closure (↑K : Set α)
⊢ x⁻¹ ∈ closure (↑K : Set α)
have inl : ∀ (hx : 0 ∈ closure (↑K : Set α)), 0⁻¹ ∈ closure (↑K : Set α)
Tactic: rcases eq_or_ne x 0 with (rfl | h)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
Goal:
K_1 : Type u_1
inst : DivisionRing K_1
inst_1 : TopologicalSpace K_1
α : Type u_2
inst_2 : Field α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalDivisionRing α
K : Subfield α
x : α
hx : x ∈ closure (↑K : Set α)
inl : ∀ (hx : 0 ∈ closure (↑K : Set α)), 0⁻¹ ∈ closure (↑K : Set α)
⊢ x⁻¹ ∈ closure (↑K : Set α)
have inr : ∀ (h : x ≠ 0), x⁻¹ ∈ closure (↑K : Set α)
Tactic: rcases eq_or_ne x 0 with (rfl | h)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
Goal:
K_1 : Type u_1
inst : DivisionRing K_1
inst_1 : TopologicalSpace K_1
α : Type u_2
inst_2 : Field α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalDivisionRing α
K : Subfield α
x : α
hx : x ∈ closure (↑K : Set α)
h : x ≠ 0
⊢ x⁻¹ ∈ closure (↑K : Set α)
have inr : Membership.mem (γ := Set α) (closure ((fun (x : α) ↦ x⁻¹) '' (↑K : Set α))) x⁻¹
Tactic: rw [← inv_coe_set, ← Set.image_inv_eq_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
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
⊢ Continuous (X := { r : R // 0 ≤ r }ˣ)
    (Equiv.toFun (MulEquiv.toEquiv (unitsEquivPos R)) : { r : R // 0 ≤ r }ˣ → { r : R // 0 < r })
have rw : Continuous (X := { r : R // 0 ≤ r }ˣ)
  (Subtype.val (p := fun (r : R) ↦ 0 < r) ∘ Equiv.toFun (MulEquiv.toEquiv (unitsEquivPos R)) : { r : R // 0 ≤ r }ˣ → R)
Tactic: rw [Topology.IsEmbedding.subtypeVal.continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
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
⊢ Continuous (X := { r : R // 0 < r }) (Y := { r : R // 0 ≤ r }ˣ)
    (Equiv.invFun (MulEquiv.toEquiv (unitsEquivPos R)) : { r : R // 0 < r } → { r : R // 0 ≤ r }ˣ)
have rw : 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: rw [Units.continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
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
⊢ 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 })
have 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 })
Tactic: refine ⟨by fun_prop, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
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
⊢ 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 })
have suffices : Continuous (Y := R) fun (x : { r : R // 0 < r }) ↦ (↑x : R)⁻¹
Tactic: suffices Continuous fun (x : { r : R // 0 < r }) ↦ (x⁻¹ : R) by
      simpa [Topology.IsEmbedding.subtypeVal.continuous_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
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
⊢ Continuous (Y := R) fun (x : { r : R // 0 < r }) ↦ (↑x : R)⁻¹
have rw : ∀ (x : { r : R // 0 < r }), ContinuousAt (Y := R) (fun (x : { r : R // 0 < r }) ↦ (↑x : R)⁻¹) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
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 : 𝕜
⊢ (fun (y : 𝕜) ↦ (y - b) / a) ((fun (x : 𝕜) ↦ a * x + b) x) = x
have simp : a * x / a = x
Tactic: simp only [add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
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
⊢ IsLocalMax f⁻¹ a
have 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
Tactic: filter_upwards [h1, h2] with z h3 h4 using (inv_le_inv₀ h4 h2.self_of_nhds).mpr h3
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
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
⊢ IsLocalMax f⁻¹ a
have h₁ : ∀ (a_1 : α), f a ≤ f a_1 → 0 < f a_1 → f⁻¹ a_1 ≤ f⁻¹ a
Tactic: filter_upwards [h1, h2] with z h3 h4 using (inv_le_inv₀ h4 h2.self_of_nhds).mpr h3
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (hypothesis)
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
⊢ EqOn f 1 S ∨ EqOn f (-1) S
have hmaps : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (hypothesis)
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 f g S ∨ EqOn f (-g) S
have hsq₁ : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
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
⊢ f x = g x
have inl : ∀ (h : EqOn f g S), f x = g x
Tactic: rcases hS.eq_or_eq_neg_of_sq_eq hf hg @hsq @hg_ne with (h | h)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
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
⊢ f x = g x
have inr : ∀ (h : EqOn f (-g) S), f x = g x
Tactic: rcases hS.eq_or_eq_neg_of_sq_eq hf hg @hsq @hg_ne with (h | h)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
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
have 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
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' ⊢
Cleared hypotheses: hy', x, hx, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
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
⊢ f x = g x
have rw : ∀ (hy' : Eq.{u_3 + 1} (α := 𝕜) 2 0 ∨ False) (x : α) (hx : x ∈ S) (h : EqOn f (-g) S), x ∈ S
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' ⊢
Cleared hypotheses: hy', x, hx, h