awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.UniformConvergence (hypothesis)
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this : IsTopologicalAddGroup H
hb :
  HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
c : 𝕜
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ ∃ (j : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) j ∧
      Set.MapsTo (β := H) (fun (x : H) ↦ c • x)
        {u : H | ∀ (x : α), Membership.mem (α := E) j ((φ : (a : H) → α → E) u x : E)}
        {u : H | ∀ (x : α), Membership.mem (α := E) U ((φ : (a : H) → α → E) u x : E)}
have this₁ : Tendsto (β := E) (fun (x : E) ↦ c • x) (𝓝 0) (𝓝 0)
Tactic: have : Tendsto (c • · : E → E) (𝓝 0) (𝓝 0) :=
      (continuous_const_smul c).tendsto' _ _ (smul_zero _)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.UniformConvergence (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this_1 : IsTopologicalAddGroup H
hb :
  HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
c : 𝕜
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
this : Tendsto (β := E) (fun (x : E) ↦ c • x) (𝓝 0) (𝓝 0)
⊢ ∃ (j : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) j ∧
      Set.MapsTo (β := H) (fun (x : H) ↦ c • x)
        {u : H | ∀ (x : α), Membership.mem (α := E) j ((φ : (a : H) → α → E) u x : E)}
        {u : H | ∀ (x : α), Membership.mem (α := E) U ((φ : (a : H) → α → E) u x : E)}
have hsmul_left : ∀ (u : H)
  (hu :
    Membership.mem (γ := Set H)
      {u : H |
        ∀ (x : α), Membership.mem (α := E) (γ := Set E) ((fun (x : E) ↦ c • x) ⁻¹' U) ((φ : (a : H) → α → E) u x : E)}
      u)
  (x : α), Membership.mem (α := E) U ((φ : (a : H) → α → E) ((fun (x : H) ↦ c • x) u) x : E)
Tactic: refine ⟨_, this hU, fun u hu x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.UniformConvergence (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ E) (Function.comp (β := α → E) (⇑ofFun : (a : α → E) → α →ᵤ E) (⇑φ : (a : H) → α → E))
h :
  ∀ (u : H), Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Set.range.{u_3, u_2 + 1} (ι := α) ((φ : (a : H) → α → E) u))
this : IsTopologicalAddGroup H
hb :
  HasBasis.{u_4, u_3 + 1} (α := H) (𝓝 0) (fun (x : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) x) fun (V : Set E) ↦
    {u : H | ∀ (x : α), Membership.mem (α := E) V ((φ : (a : H) → α → E) u x : E)}
u : H
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0,
    Membership.mem (γ := Set H) {u : H | ∀ (x : α), Membership.mem (α := E) U ((φ : (a : H) → α → E) u x : E)} (x • u)
have hsmul_right : ∀ᶠ (x : 𝕜) in 𝓝 0, ∀ (x_1 : α), HSMul.hSMul (β := E) x ((φ : (a : H) → α → E) u x_1 : E) ∈ U
Tactic: simp only [Set.mem_setOf_eq, map_smul, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.UniformConvergence (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace H
inst_6 : UniformSpace E
inst_7 : IsUniformAddGroup E
inst_8 : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst_9 : FunLike hom H (α → E)
inst_10 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ :
  IsInducing (X := H) (Y := α →ᵤ[𝔖] E)
    (Function.comp (β := α → E) (⇑(ofFun 𝔖) : (a : α → E) → α →ᵤ[𝔖] E) (⇑φ : (a : H) → α → E))
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ((φ : (a : H) → α → E) u '' s)
⊢ ContinuousSMul 𝕜 H
have obtain : ∀
  (hφ :
    IsInducing (X := H) (Y := α →ᵤ[𝔖] E)
      (Function.comp (β := α → E) (⇑(ofFun 𝔖) : (a : α → E) → α →ᵤ[𝔖] E) (⇑φ : (a : H) → α → E))),
  ContinuousSMul 𝕜 H
Tactic: obtain rfl := hφ.eq_induced
Cleared hypotheses: inst_5, hφ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.UniformConvergence (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : UniformSpace E
inst_6 : IsUniformAddGroup E
inst_7 : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst_8 : FunLike hom H (α → E)
inst_9 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ((φ : (a : H) → α → E) u '' s)
⊢ ContinuousSMul 𝕜 H
have simp : ContinuousSMul 𝕜 H
Tactic: simp +instances only [induced_iInf, UniformOnFun.topologicalSpace_eq, induced_compose]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.UniformConvergence (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : UniformSpace E
inst_6 : IsUniformAddGroup E
inst_7 : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst_8 : FunLike hom H (α → E)
inst_9 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ((φ : (a : H) → α → E) u '' s)
⊢ ContinuousSMul 𝕜 H
have refine : ∀ (s : Set α) (hs : s ∈ 𝔖), ContinuousSMul 𝕜 H
Tactic: refine continuousSMul_iInf fun s ↦ continuousSMul_iInf fun hs ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.UniformConvergence (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup H
inst_2 : Module 𝕜 H
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : UniformSpace E
inst_6 : IsUniformAddGroup E
inst_7 : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst_8 : FunLike hom H (α → E)
inst_9 : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ((φ : (a : H) → α → E) u '' s)
s : Set α
hs : s ∈ 𝔖
this : TopologicalSpace H :=
  TopologicalSpace.induced (Y := UniformFun.{u_2, u_3} (↑s : Type u_2) E)
    (Function.comp (β := (↑s : Type u_2) → E)
      ((⇑UniformFun.ofFun : (a : (↑s : Type u_2) → E) → UniformFun.{u_2, u_3} (↑s : Type u_2) E) :
        (a : (↑s : Type u_2) → E) → UniformFun.{u_2, u_3} (↑s : Type u_2) E)
      (Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E) : H → (↑s : Type u_2) → E))
    (UniformFun.topologicalSpace (↑s : Type u_2) E)
φ' : H →ₗ[𝕜] (↑s : Type u_2) → E :=
  { toFun := Function.comp (β := α → E) (s.restrict (π := fun (a : α) ↦ E)) (⇑φ : (a : H) → α → E), map_add' := ⋯,
    map_smul' := ⋯ }
⊢ ContinuousSMul 𝕜 H
have refine : ∀ (u : H),
  Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E)
    (Set.range.{u_3, u_2 + 1} (ι := (↑s : Type u_2)) ((φ' : (a : H) → (↑s : Type u_2) → E) u))
Tactic: refine UniformFun.continuousSMul_induced_of_range_bounded 𝕜 s E H φ' ⟨rfl⟩ fun u ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid.AddChar (goal)
Goal:
A : Type u_1
M : Type u_2
inst : TopologicalSpace A
inst_1 : AddMonoidWithOne A
inst_2 : Monoid M
inst_3 : TopologicalSpace M
inst_4 : T2Space M
hdr : DenseRange.{u_1, 0} (X := A) Nat.cast
κ₁ κ₂ : AddChar A M
hκ₁ : Continuous.{u_1, u_2} (X := A) (Y := M) (⇑κ₁ : (a : A) → M)
hκ₂ : Continuous.{u_1, u_2} (X := A) (Y := M) (⇑κ₂ : (a : A) → M)
h : Eq.{u_2 + 1} (α := M) ((κ₁ : (a : A) → M) 1 : M) ((κ₂ : (a : A) → M) 1 : M)
⊢ κ₁ = κ₂
have refine : ∀ (n : ℕ),
  Eq.{u_2 + 1} (α := M)
    (Function.comp.{1, u_1 + 1, u_2 + 1} (β := A) ((fun (f : AddChar A M) ↦ ((⇑f : (a : A) → M) : (a : A) → M)) κ₁)
      Nat.cast n)
    (Function.comp.{1, u_1 + 1, u_2 + 1} (β := A) ((fun (f : AddChar A M) ↦ ((⇑f : (a : A) → M) : (a : A) → M)) κ₂)
      Nat.cast n)
Tactic: refine DFunLike.coe_injective <| hdr.equalizer hκ₁ hκ₂ (funext fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid.FunOnFinite (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
X : Type u_2
Y : Type u_3
inst_3 : Finite X
inst_4 : Finite Y
f : X → Y
⊢ Continuous (X := X → M) (map f)
have have : ∀ (this : Fintype X), Continuous (X := X → M) (map f)
Tactic: have := Fintype.ofFinite X
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid.FunOnFinite (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
X : Type u_2
Y : Type u_3
inst_3 : Finite X
inst_4 : Finite Y
f : X → Y
this : Fintype X
⊢ Continuous (X := X → M) (map f)
have refine : ∀ (y : Y), Continuous (Y := M) fun (a : X → M) ↦ map f a y
Tactic: refine continuous_pi (fun y ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid.FunOnFinite (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
X : Type u_2
Y : Type u_3
inst_3 : Finite X
inst_4 : Finite Y
f : X → Y
this : Fintype X
y : Y
⊢ Continuous (Y := M) fun (a : X → M) ↦ map f a y
have simp : Continuous (Y := M) fun (a : X → M) ↦ ∑ x : X with f x = y, a x
Tactic: simp only [FunOnFinite.map_apply_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid.FunOnFinite (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
X : Type u_2
Y : Type u_3
inst_3 : Finite X
inst_4 : Finite Y
f : X → Y
⊢ Continuous (X := X → M) (map f)
have have : ∀ (this : Fintype X), Continuous (X := X → M) (map f)
Tactic: classical
  have := Fintype.ofFinite X
  refine continuous_pi (fun y ↦ ?_)
  simp only [FunOnFinite.map_apply_apply]
  exact continuous_finsetSum _ (fun _ _ ↦ continuous_apply _)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid.FunOnFinite (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
X : Type u_2
Y : Type u_3
inst_3 : Finite X
inst_4 : Finite Y
f : X → Y
have have₁ have₂ : ∀ (this : Fintype X), Continuous (X := X → M) (map f)
⊢ Continuous (X := X → M) (map f)
have have₃ : ∀ (this : Fintype X) (y : Y), Continuous (Y := M) fun (a : X → M) ↦ map f a y
Tactic: classical
  have := Fintype.ofFinite X
  refine continuous_pi (fun y ↦ ?_)
  simp only [FunOnFinite.map_apply_apply]
  exact continuous_finsetSum _ (fun _ _ ↦ continuous_apply _)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid.FunOnFinite (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
X : Type u_2
Y : Type u_3
inst_3 : Finite X
inst_4 : Finite Y
f : X → Y
have have₁ have₂ : ∀ (this : Fintype X), Continuous (X := X → M) (map f)
have₃ : ∀ (this : Fintype X) (y : Y), Continuous (Y := M) fun (a : X → M) ↦ map f a y
⊢ Continuous (X := X → M) (map f)
have have₄ : ∀ (this : Fintype X) (y : Y), Continuous (Y := M) fun (a : X → M) ↦ ∑ x : X with f x = y, a x
Tactic: classical
  have := Fintype.ofFinite X
  refine continuous_pi (fun y ↦ ?_)
  simp only [FunOnFinite.map_apply_apply]
  exact continuous_finsetSum _ (fun _ _ ↦ continuous_apply _)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
α : Type u_6
β : Type u_7
F : Type u_8
inst : FunLike F α β
inst_1 : Mul α
inst_2 : Mul β
inst_3 : MulHomClass F α β
tβ : TopologicalSpace β
inst_4 : ContinuousMul β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
⊢ ContinuousMul α
have refine : Continuous[instTopologicalSpaceProd, tβ] (Function.comp (β := α) (⇑f : (a : α) → β) fun (p : α × α) ↦ p.1 * p.2)
Tactic: refine ⟨continuous_induced_rng.2 ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
α : Type u_6
β : Type u_7
F : Type u_8
inst : FunLike F α β
inst_1 : Mul α
inst_2 : Mul β
inst_3 : MulHomClass F α β
tβ : TopologicalSpace β
inst_4 : ContinuousMul β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
⊢ Continuous[instTopologicalSpaceProd, tβ] (Function.comp (β := α) (⇑f : (a : α) → β) fun (p : α × α) ↦ p.1 * p.2)
have simp : Continuous[instTopologicalSpaceProd, tβ] fun (x : α × α) ↦
  HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x.1 : β) ((f : (a : α) → β) x.2 : β)
Tactic: simp only [Function.comp_def, map_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Mul M
inst_2 : ContinuousMul M
a b : M
⊢ 𝓝 a * 𝓝 b ≤ 𝓝 (a * b)
have rw : map (Function.uncurry fun (x1 x2 : M) ↦ x1 * x2) (𝓝 (a, b)) ≤ 𝓝 (a * b)
Tactic: rw [← map₂_mul, ← map_uncurry_prod, ← nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
α : Type u_2
𝕜 : Type u_6
inst : Preorder 𝕜
inst_1 : Zero 𝕜
inst_2 : Mul 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst_5 : PosMulStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x : α
h_1 : f x ∈ Ioi c
⊢ b * f x ∈ Ioi (b * c)
have rw : c < f x → b * c < b * f x
Tactic: rw [Set.mem_Ioi] at *
Cleared hypotheses: h_1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
α : Type u_2
𝕜 : Type u_6
inst : Preorder 𝕜
inst_1 : Zero 𝕜
inst_2 : Mul 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst_5 : PosMulStrictMono 𝕜
h : Tendsto f l (𝓝[<] c)
x : α
h_1 : f x ∈ Iio c
⊢ b * f x ∈ Iio (b * c)
have rw : f x < c → b * f x < b * c
Tactic: rw [Set.mem_Iio] at *
Cleared hypotheses: h_1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
α : Type u_2
𝕜 : Type u_6
inst : Preorder 𝕜
inst_1 : Zero 𝕜
inst_2 : Mul 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst_5 : MulPosStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x : α
h_1 : f x ∈ Ioi c
⊢ f x * b ∈ Ioi (c * b)
have rw : c < f x → c * b < f x * b
Tactic: rw [Set.mem_Ioi] at *
Cleared hypotheses: h_1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
α : Type u_2
𝕜 : Type u_6
inst : Preorder 𝕜
inst_1 : Zero 𝕜
inst_2 : Mul 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst_5 : MulPosStrictMono 𝕜
h : Tendsto f l (𝓝[<] c)
x : α
h_1 : f x ∈ Iio c
⊢ f x * b ∈ Iio (c * b)
have rw : f x < c → f x * b < c * b
Tactic: rw [Set.mem_Iio] at *
Cleared hypotheses: h_1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Mul M
inst_3 : ContinuousMul M
inst_4 : TopologicalSpace N
inst_5 : Monoid N
inst_6 : ContinuousMul N
inst_7 : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst_8 : l.NeBot
h₁ : Tendsto (fun (x : ι) ↦ (↑(f x) : N)) l (𝓝 r₁)
h₂ : Tendsto (fun (x : ι) ↦ (↑(f x)⁻¹ : N)) l (𝓝 r₂)
⊢ r₁ * r₂ = 1
have symm : 1 = r₁ * r₂
Tactic: symm
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Mul M
inst_3 : ContinuousMul M
inst_4 : TopologicalSpace N
inst_5 : Monoid N
inst_6 : ContinuousMul N
inst_7 : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst_8 : l.NeBot
h₁ : Tendsto (fun (x : ι) ↦ (↑(f x) : N)) l (𝓝 r₁)
h₂ : Tendsto (fun (x : ι) ↦ (↑(f x)⁻¹ : N)) l (𝓝 r₂)
⊢ r₂ * r₁ = 1
have symm : 1 = r₂ * r₁
Tactic: symm
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Mul M
inst_3 : ContinuousMul M
inst_4 : TopologicalSpace N
inst_5 : Mul N
inst_6 : ContinuousMul N
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : (M × N) × M × N) ↦ p.1 * p.2
have hf : Continuous[instTopologicalSpaceProd, inst_1] fun (x : (M × N) × M × N) ↦ x.1.1 * x.2.1
Tactic: apply Continuous.prodMk
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Mul M
inst_3 : ContinuousMul M
inst_4 : TopologicalSpace N
inst_5 : Mul N
inst_6 : ContinuousMul N
hf : Continuous[instTopologicalSpaceProd, inst_1] fun (x : (M × N) × M × N) ↦ x.1.1 * x.2.1
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (p : (M × N) × M × N) ↦ p.1 * p.2
have hg : Continuous[instTopologicalSpaceProd, inst_4] fun (x : (M × N) × M × N) ↦ x.1.2 * x.2.2
Tactic: apply Continuous.prodMk
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
α : Type u_2
M_1 : Type u_3
N_1 : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M_1
inst_2 : Mul M_1
inst_3 : ContinuousMul M_1
M : Type u_6
N : Type u_7
inst_4 : TopologicalSpace M
inst_5 : Mul M
inst_6 : SeparatelyContinuousMul M
inst_7 : TopologicalSpace N
inst_8 : Mul N
inst_9 : SeparatelyContinuousMul N
x : M × N
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (x_1 : M × N) ↦ x * x_1
have hf : Continuous[instTopologicalSpaceProd, inst_4] fun (x_1 : M × N) ↦ x.1 * x_1.1
Tactic: apply Continuous.prodMk
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
α : Type u_2
M_1 : Type u_3
N_1 : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M_1
inst_2 : Mul M_1
inst_3 : ContinuousMul M_1
M : Type u_6
N : Type u_7
inst_4 : TopologicalSpace M
inst_5 : Mul M
inst_6 : SeparatelyContinuousMul M
inst_7 : TopologicalSpace N
inst_8 : Mul N
inst_9 : SeparatelyContinuousMul N
x : M × N
hf : Continuous[instTopologicalSpaceProd, inst_4] fun (x_1 : M × N) ↦ x.1 * x_1.1
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (x_1 : M × N) ↦ x * x_1
have hg : Continuous[instTopologicalSpaceProd, inst_7] fun (x_1 : M × N) ↦ x.2 * x_1.2
Tactic: apply Continuous.prodMk
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
α : Type u_2
M_1 : Type u_3
N_1 : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M_1
inst_2 : Mul M_1
inst_3 : ContinuousMul M_1
M : Type u_6
N : Type u_7
inst_4 : TopologicalSpace M
inst_5 : Mul M
inst_6 : SeparatelyContinuousMul M
inst_7 : TopologicalSpace N
inst_8 : Mul N
inst_9 : SeparatelyContinuousMul N
x : M × N
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (x_1 : M × N) ↦ x_1 * x
have hf : Continuous[instTopologicalSpaceProd, inst_4] fun (x_1 : M × N) ↦ x_1.1 * x.1
Tactic: apply Continuous.prodMk
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
ι : Type u_1
α : Type u_2
M_1 : Type u_3
N_1 : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M_1
inst_2 : Mul M_1
inst_3 : ContinuousMul M_1
M : Type u_6
N : Type u_7
inst_4 : TopologicalSpace M
inst_5 : Mul M
inst_6 : SeparatelyContinuousMul M
inst_7 : TopologicalSpace N
inst_8 : Mul N
inst_9 : SeparatelyContinuousMul N
x : M × N
hf : Continuous[instTopologicalSpaceProd, inst_4] fun (x_1 : M × N) ↦ x_1.1 * x.1
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (x_1 : M × N) ↦ x_1 * x
have hg : Continuous[instTopologicalSpaceProd, inst_7] fun (x_1 : M × N) ↦ x_1.2 * x.2
Tactic: apply Continuous.prodMk
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u
inst : Monoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x * x₀) (𝓝 1)
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : M × M) ↦ p.1 * p.2
have rw : ∀ (x : M × M), ContinuousAt (Y := M) (fun (p : M × M) ↦ p.1 * p.2) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u
inst : Monoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
⊢ Eq.{u + 1} (α := (p : M × M) → M) (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀))
    (comp (β := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (uncurry fun (x1 x2 : M) ↦ x1 * x2))
have h : ∀ (p : M × M),
  x₀ * p.1 * (p.2 * y₀) =
    comp (β := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (uncurry fun (x1 x2 : M) ↦ x1 * x2) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
Goal:
M : Type u
inst : Monoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
⊢ ContinuousAt (Y := M) (fun (p : M × M) ↦ p.1 * p.2) (x₀, y₀)
have key : Eq.{u + 1} (α := (p : M × M) → M) (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀))
  (comp (β := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (uncurry fun (x1 x2 : M) ↦ x1 * x2))
Tactic: have key : (fun p : M × M => x₀ * p.1 * (p.2 * y₀)) =
        ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry (· * ·) := by
      ext p
      simp [uncurry, mul_assoc]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
M : Type u
inst : Monoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key :
  Eq.{u + 1} (α := (p : M × M) → M) (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀))
    (comp (β := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (uncurry fun (x1 x2 : M) ↦ x1 * x2))
⊢ Eq.{u + 1} (α := M → M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) fun (x : M) ↦ x₀ * y₀ * x
have h : ∀ (x : M), ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) x = x₀ * y₀ * x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (hypothesis)
Goal:
M : Type u
inst : Monoid M
inst_1 : TopologicalSpace M
hmul :
  Tendsto (β := M) (uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun (x : M) ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key :
  Eq.{u + 1} (α := (p : M × M) → M) (fun (p : M × M) ↦ x₀ * p.1 * (p.2 * y₀))
    (comp (β := M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ x * y₀) (uncurry fun (x1 x2 : M) ↦ x1 * x2))
⊢ ContinuousAt (Y := M) (fun (p : M × M) ↦ p.1 * p.2) (x₀, y₀)
have key₂ : Eq.{u + 1} (α := M → M) ((fun (x : M) ↦ x₀ * x) ∘ fun (x : M) ↦ y₀ * x) fun (x : M) ↦ x₀ * y₀ * x
Tactic: have key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x := by
      ext x
      simp [mul_assoc]