awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddCommGroup α
inst_2 : IsUniformAddGroup α
inst_3 : Semiring R
inst_4 : Module R α
inst_5 : UniformContinuousConstSMul R α
a b : R
x : α
rw :
  (↑((a + b) • x) : Completion α) =
    HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
rw₁ :
  (↑(a • x + b • x) : Completion α) =
    HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
rw₂ :
  HAdd.hAdd (α := Completion α) (↑(a • x) : Completion α) (↑(b • x) : Completion α) =
    HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
rw₃ :
  HSMul.hSMul (β := Completion α) a (↑x : Completion α) + (↑(b • x) : Completion α) =
    HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
⊢ HSMul.hSMul (β := Completion α) (a + b) (↑x : Completion α) =
    HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
have rw₄ : HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α) =
  HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
Tactic: rw [← coe_smul, add_smul, coe_add, coe_smul, coe_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
inst_3 : UniformSpace β
inst_4 : AddGroup β
inst_5 : IsUniformAddGroup β
inst_6 : CompleteSpace β
inst_7 : T0Space β
f : α →+ β
hf_1 : Continuous.{u_3, u_4} (X := α) (Y := β) (⇑f : (a : α) → β)
hf : UniformContinuous.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ Eq.{u_4 + 1} (α := β) (Completion.extension.{u_3, u_4} (α := α) (⇑f : (a : α) → β) 0) 0
have rw : Eq.{u_4 + 1} (α := β) (Completion.extension.{u_3, u_4} (α := α) (⇑f : (a : α) → β) (↑0 : Completion α)) 0
Tactic: rw [← coe_zero, extension_coe hf, f.map_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
inst_3 : UniformSpace β
inst_4 : AddGroup β
inst_5 : IsUniformAddGroup β
inst_6 : CompleteSpace β
inst_7 : T0Space β
f : α →+ β
hf_1 : Continuous.{u_3, u_4} (X := α) (Y := β) (⇑f : (a : α) → β)
hf : UniformContinuous.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
rw : Eq.{u_4 + 1} (α := β) (Completion.extension.{u_3, u_4} (α := α) (⇑f : (a : α) → β) (↑0 : Completion α)) 0
⊢ Eq.{u_4 + 1} (α := β) (Completion.extension.{u_3, u_4} (α := α) (⇑f : (a : α) → β) 0) 0
have rw₁ : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)
Tactic: rw [← coe_zero, extension_coe hf, f.map_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
inst_3 : UniformSpace β
inst_4 : AddGroup β
inst_5 : IsUniformAddGroup β
inst_6 : CompleteSpace β
inst_7 : T0Space β
f : α →+ β
hf_1 : Continuous.{u_3, u_4} (X := α) (Y := β) (⇑f : (a : α) → β)
hf : UniformContinuous.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
rw : Eq.{u_4 + 1} (α := β) (Completion.extension.{u_3, u_4} (α := α) (⇑f : (a : α) → β) (↑0 : Completion α)) 0
rw₁ : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)
⊢ Eq.{u_4 + 1} (α := β) (Completion.extension.{u_3, u_4} (α := α) (⇑f : (a : α) → β) 0) 0
have rw₂ : Eq.{u_4 + 1} (α := β) 0 0
Tactic: rw [← coe_zero, extension_coe hf, f.map_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
inst_3 : UniformSpace β
inst_4 : AddGroup β
inst_5 : IsUniformAddGroup β
inst_6 : CompleteSpace β
inst_7 : T0Space β
f : α →+ β
hf_1 : Continuous.{u_3, u_4} (X := α) (Y := β) (⇑f : (a : α) → β)
hf : UniformContinuous.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
a_1 b_1 : Completion α
a b : α
⊢ Completion.extension (⇑f : (a : α) → β) (HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α)) =
    HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
have rw_mod_cast : Completion.extension (⇑f : (a : α) → β) (↑(a + b) : Completion α) =
  HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
    (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
Tactic: rw_mod_cast [extension_coe hf, extension_coe hf, extension_coe hf, f.map_add]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
inst_3 : UniformSpace β
inst_4 : AddGroup β
inst_5 : IsUniformAddGroup β
inst_6 : CompleteSpace β
inst_7 : T0Space β
f : α →+ β
hf_1 : Continuous.{u_3, u_4} (X := α) (Y := β) (⇑f : (a : α) → β)
hf : UniformContinuous.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
a_1 b_1 : Completion α
a b : α
rw_mod_cast rw_mod_cast₁ rw_mod_cast₂ rw_mod_cast₃ rw_mod_cast₄ rw_mod_cast₅ :
  Completion.extension (⇑f : (a : α) → β) (↑(a + b) : Completion α) =
    HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
⊢ Completion.extension (⇑f : (a : α) → β) (HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α)) =
    HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
have rw_mod_cast₆ : (f : (a : α) → β) (a + b) =
  HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
    (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
Tactic: rw_mod_cast [extension_coe hf, extension_coe hf, extension_coe hf, f.map_add]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
inst_3 : UniformSpace β
inst_4 : AddGroup β
inst_5 : IsUniformAddGroup β
inst_6 : CompleteSpace β
inst_7 : T0Space β
f : α →+ β
hf_1 : Continuous.{u_3, u_4} (X := α) (Y := β) (⇑f : (a : α) → β)
hf : UniformContinuous.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
a_1 b_1 : Completion α
a b : α
rw_mod_cast rw_mod_cast₁ rw_mod_cast₂ rw_mod_cast₃ rw_mod_cast₄ rw_mod_cast₅ :
  Completion.extension (⇑f : (a : α) → β) (↑(a + b) : Completion α) =
    HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
rw_mod_cast₆ :
  (f : (a : α) → β) (a + b) =
    HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
⊢ Completion.extension (⇑f : (a : α) → β) (HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α)) =
    HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
have rw_mod_cast₇ : (f : (a : α) → β) (a + b) =
  HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β)
    (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α) : β)
Tactic: rw_mod_cast [extension_coe hf, extension_coe hf, extension_coe hf, f.map_add]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
inst_3 : UniformSpace β
inst_4 : AddGroup β
inst_5 : IsUniformAddGroup β
inst_6 : CompleteSpace β
inst_7 : T0Space β
f : α →+ β
hf_1 : Continuous.{u_3, u_4} (X := α) (Y := β) (⇑f : (a : α) → β)
hf : UniformContinuous.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
a_1 b_1 : Completion α
a b : α
rw_mod_cast rw_mod_cast₁ rw_mod_cast₂ rw_mod_cast₃ rw_mod_cast₄ rw_mod_cast₅ :
  Completion.extension (⇑f : (a : α) → β) (↑(a + b) : Completion α) =
    HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
rw_mod_cast₆ :
  (f : (a : α) → β) (a + b) =
    HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
rw_mod_cast₇ :
  (f : (a : α) → β) (a + b) =
    HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β)
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α) : β)
⊢ Completion.extension (⇑f : (a : α) → β) (HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α)) =
    HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
have rw_mod_cast₈ : (f : (a : α) → β) (a + b) = HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
Tactic: rw_mod_cast [extension_coe hf, extension_coe hf, extension_coe hf, f.map_add]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
inst_3 : UniformSpace β
inst_4 : AddGroup β
inst_5 : IsUniformAddGroup β
⊢ Eq (α := AddMonoidHom.{u_3, u_4} (Completion α) (Completion β)) (completion 0 ⋯) 0
have h : ∀ (x : Completion α),
  Eq.{u_4 + 1} (α := Completion β) ((completion 0 sorry : (a : Completion α) → Completion β) x : Completion β)
    (((0 : AddMonoidHom.{u_3, u_4} (Completion α) (Completion β)) : (a : Completion α) → Completion β) x : Completion β)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
inst_3 : UniformSpace β
inst_4 : AddGroup β
inst_5 : IsUniformAddGroup β
x : Completion α
⊢ Eq.{u_4 + 1} (α := Completion β) ((completion 0 ⋯ : (a : Completion α) → Completion β) x : Completion β)
    (((0 : AddMonoidHom.{u_3, u_4} (Completion α) (Completion β)) : (a : Completion α) → Completion β) x : Completion β)
have h : IsClosed.{u_3} (X := Completion α)
  {a : Completion α |
    Eq.{u_4 + 1} (α := Completion β) ((completion 0 sorry : (a : Completion α) → Completion β) a : Completion β)
      (((0 : AddMonoidHom.{u_3, u_4} (Completion α) (Completion β)) : (a : Completion α) → Completion β) a :
        Completion β)}
Tactic: refine Completion.induction_on x ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
inst_3 : UniformSpace β
inst_4 : AddGroup β
inst_5 : IsUniformAddGroup β
x : Completion α
h :
  IsClosed.{u_3} (X := Completion α)
    {a : Completion α |
      Eq.{u_4 + 1} (α := Completion β) ((completion 0 ⋯ : (a : Completion α) → Completion β) a : Completion β)
        (((0 : AddMonoidHom.{u_3, u_4} (Completion α) (Completion β)) : (a : Completion α) → Completion β) a :
          Completion β)}
⊢ Eq.{u_4 + 1} (α := Completion β) ((completion 0 ⋯ : (a : Completion α) → Completion β) x : Completion β)
    (((0 : AddMonoidHom.{u_3, u_4} (Completion α) (Completion β)) : (a : Completion α) → Completion β) x : Completion β)
have h₁ : ∀ (a : α),
  Eq.{u_4 + 1} (α := Completion β)
    ((completion 0 sorry : (a : Completion α) → Completion β) (↑a : Completion α) : Completion β)
    (((0 : AddMonoidHom.{u_3, u_4} (Completion α) (Completion β)) : (a : Completion α) → Completion β)
        (↑a : Completion α) :
      Completion β)
Tactic: refine Completion.induction_on x ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
inst_3 : UniformSpace β
inst_4 : AddGroup β
inst_5 : IsUniformAddGroup β
x : Completion α
⊢ IsClosed.{u_3} (X := Completion α)
    {a : Completion α |
      Eq.{u_4 + 1} (α := Completion β) ((completion 0 ⋯ : (a : Completion α) → Completion β) a : Completion β)
        (((0 : AddMonoidHom.{u_3, u_4} (Completion α) (Completion β)) : (a : Completion α) → Completion β) a :
          Completion β)}
have h : Continuous.{u_3, u_4} (X := Completion α) (Y := Completion β) (⇑0 : (a : Completion α) → Completion β)
Tactic: apply isClosed_eq (AddMonoidHom.continuous_completion (0 : α →+ β) continuous_const)
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (hypothesis)
Goal:
α : Type u_3
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
γ : Type u_5
inst_3 : AddCommGroup γ
inst_4 : UniformSpace γ
inst_5 : IsUniformAddGroup γ
f g : α →+ γ
hf : Continuous.{u_3, u_5} (X := α) (Y := γ) (⇑f : (a : α) → γ)
hg : Continuous.{u_3, u_5} (X := α) (Y := γ) (⇑g : (a : α) → γ)
⊢ (f + g).completion ⋯ =
    HAdd.hAdd (α := AddMonoidHom.{u_3, u_5} (Completion α) (Completion γ)) (f.completion hf) (g.completion hg)
have hfg : Continuous (HAdd.hAdd (α := α → γ) (⇑f : (a : α) → γ) (⇑g : (a : α) → γ))
Tactic: have hfg := hf.add hg
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
α : Type u_3
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
γ : Type u_5
inst_3 : AddCommGroup γ
inst_4 : UniformSpace γ
inst_5 : IsUniformAddGroup γ
f g : α →+ γ
hf : Continuous.{u_3, u_5} (X := α) (Y := γ) (⇑f : (a : α) → γ)
hg : Continuous.{u_3, u_5} (X := α) (Y := γ) (⇑g : (a : α) → γ)
hfg : Continuous (HAdd.hAdd (α := α → γ) (⇑f : (a : α) → γ) (⇑g : (a : α) → γ))
⊢ (f + g).completion ⋯ =
    HAdd.hAdd (α := AddMonoidHom.{u_3, u_5} (Completion α) (Completion γ)) (f.completion hf) (g.completion hg)
have h : ∀ (x : Completion α),
  Eq.{u_5 + 1} (α := Completion γ)
    ((((f + g).completion sorry : AddMonoidHom.{u_3, u_5} (Completion α) (Completion γ)) :
          (a : Completion α) → Completion γ)
        x :
      Completion γ)
    ((HAdd.hAdd (α := AddMonoidHom.{u_3, u_5} (Completion α) (Completion γ)) (f.completion hf) (g.completion hg) :
          (a : Completion α) → Completion γ)
        x :
      Completion γ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
α : Type u_3
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
γ : Type u_5
inst_3 : AddCommGroup γ
inst_4 : UniformSpace γ
inst_5 : IsUniformAddGroup γ
f g : α →+ γ
hf : Continuous.{u_3, u_5} (X := α) (Y := γ) (⇑f : (a : α) → γ)
hg : Continuous.{u_3, u_5} (X := α) (Y := γ) (⇑g : (a : α) → γ)
hfg : Continuous (HAdd.hAdd (α := α → γ) (⇑f : (a : α) → γ) (⇑g : (a : α) → γ))
x : Completion α
⊢ Eq.{u_5 + 1} (α := Completion γ)
    ((((f + g).completion ⋯ : AddMonoidHom.{u_3, u_5} (Completion α) (Completion γ)) :
          (a : Completion α) → Completion γ)
        x :
      Completion γ)
    ((HAdd.hAdd (α := AddMonoidHom.{u_3, u_5} (Completion α) (Completion γ)) (f.completion hf) (g.completion hg) :
          (a : Completion α) → Completion γ)
        x :
      Completion γ)
have h : IsClosed.{u_3} (X := Completion α)
  {a : Completion α |
    Eq.{u_5 + 1} (α := Completion γ)
      ((((f + g).completion sorry : AddMonoidHom.{u_3, u_5} (Completion α) (Completion γ)) :
            (a : Completion α) → Completion γ)
          a :
        Completion γ)
      ((HAdd.hAdd (α := AddMonoidHom.{u_3, u_5} (Completion α) (Completion γ)) (f.completion hf) (g.completion hg) :
            (a : Completion α) → Completion γ)
          a :
        Completion γ)}
Tactic: refine Completion.induction_on x ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
α : Type u_3
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
γ : Type u_5
inst_3 : AddCommGroup γ
inst_4 : UniformSpace γ
inst_5 : IsUniformAddGroup γ
f g : α →+ γ
hf : Continuous.{u_3, u_5} (X := α) (Y := γ) (⇑f : (a : α) → γ)
hg : Continuous.{u_3, u_5} (X := α) (Y := γ) (⇑g : (a : α) → γ)
hfg : Continuous (HAdd.hAdd (α := α → γ) (⇑f : (a : α) → γ) (⇑g : (a : α) → γ))
x : Completion α
h :
  IsClosed.{u_3} (X := Completion α)
    {a : Completion α |
      Eq.{u_5 + 1} (α := Completion γ)
        ((((f + g).completion ⋯ : AddMonoidHom.{u_3, u_5} (Completion α) (Completion γ)) :
              (a : Completion α) → Completion γ)
            a :
          Completion γ)
        ((HAdd.hAdd (α := AddMonoidHom.{u_3, u_5} (Completion α) (Completion γ)) (f.completion hf) (g.completion hg) :
              (a : Completion α) → Completion γ)
            a :
          Completion γ)}
⊢ Eq.{u_5 + 1} (α := Completion γ)
    ((((f + g).completion ⋯ : AddMonoidHom.{u_3, u_5} (Completion α) (Completion γ)) :
          (a : Completion α) → Completion γ)
        x :
      Completion γ)
    ((HAdd.hAdd (α := AddMonoidHom.{u_3, u_5} (Completion α) (Completion γ)) (f.completion hf) (g.completion hg) :
          (a : Completion α) → Completion γ)
        x :
      Completion γ)
have h₁ : ∀ (a : α),
  Eq.{u_5 + 1} (α := Completion γ)
    ((((f + g).completion sorry : AddMonoidHom.{u_3, u_5} (Completion α) (Completion γ)) :
          (a : Completion α) → Completion γ)
        (↑a : Completion α) :
      Completion γ)
    ((HAdd.hAdd (α := AddMonoidHom.{u_3, u_5} (Completion α) (Completion γ)) (f.completion hf) (g.completion hg) :
          (a : Completion α) → Completion γ)
        (↑a : Completion α) :
      Completion γ)
Tactic: refine Completion.induction_on x ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
x : G₀
hx : x ≠ 0
⊢ 𝓝 x⁻¹ = (𝓝 x)⁻¹
have refine : (𝓝 x⁻¹)⁻¹ ≤ 𝓝 x
Tactic: refine le_antisymm (inv_le_iff_le_inv.1 ?_) (tendsto_inv₀ hx)
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (goal)
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
⊢ Tendsto (fun (n : α) ↦ f n * g n) l (𝓝 (x * y)) ↔ Tendsto f l (𝓝 x)
have refine : ∀ (hfg : Tendsto (fun (n : α) ↦ f n * g n) l (𝓝 (x * y))), Tendsto f l (𝓝 x)
Tactic: refine ⟨fun hfg => ?_, fun hf => hf.mul hg⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (goal)
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun (n : α) ↦ f n * g n) l (𝓝 (x * y))
⊢ Tendsto f l (𝓝 x)
have rw : Tendsto f l (𝓝 (x * y / y))
Tactic: rw [← mul_div_cancel_right₀ x hy]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (goal)
Goal:
α : Type u_1
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun (n : α) ↦ f n * g n) l (𝓝 (x * y))
⊢ Tendsto f l (𝓝 (x * y / y))
have refine : (fun (n : α) ↦ f n * g n) / g =ᶠ[l] f
Tactic: refine Tendsto.congr' ?_ (hfg.div hg hy)
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (goal)
Goal:
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : TopologicalSpace α
inst_5 : TopologicalSpace β
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (SProd.sprod (β := Filter G₀) (𝓝 a) ⊤) (𝓝 (h a 0))
⊢ ContinuousAt.{u_1, u_2} (Y := β) (fun (x : α) ↦ h x (f x / g x)) a
have change : ContinuousAt (↿h ∘ fun (x : α) ↦ (x, f x / g x)) a
Tactic: change ContinuousAt (↿h ∘ fun x => (x, f x / g x)) a
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (goal)
Goal:
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : TopologicalSpace α
inst_5 : TopologicalSpace β
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (SProd.sprod (β := Filter G₀) (𝓝 a) ⊤) (𝓝 (h a 0))
⊢ ContinuousAt (↿h ∘ fun (x : α) ↦ (x, f x / g x)) a
have pos : ∀ (hga : g a = 0), ContinuousAt (↿h ∘ fun (x : α) ↦ (x, f x / g x)) a
Tactic: by_cases hga : g a = 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (goal)
Goal:
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : TopologicalSpace α
inst_5 : TopologicalSpace β
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (SProd.sprod (β := Filter G₀) (𝓝 a) ⊤) (𝓝 (h a 0))
pos : ∀ (hga : g a = 0), ContinuousAt (↿h ∘ fun (x : α) ↦ (x, f x / g x)) a
⊢ ContinuousAt (↿h ∘ fun (x : α) ↦ (x, f x / g x)) a
have neg : ∀ (hga : ¬g a = 0), ContinuousAt (↿h ∘ fun (x : α) ↦ (x, f x / g x)) a
Tactic: by_cases hga : g a = 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (goal)
Goal:
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : TopologicalSpace α
inst_5 : TopologicalSpace β
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (SProd.sprod (β := Filter G₀) (𝓝 a) ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ Tendsto (↿h ∘ fun (x : α) ↦ (x, f x / g x)) (𝓝 a) (𝓝 ((↿h ∘ fun (x : α) ↦ (x, f x / g x)) a))
have pos : Tendsto (↿h ∘ fun (x : α) ↦ (x, f x / g x)) (𝓝 a) (𝓝 (↿h (a, 0)))
Tactic: simp_rw [comp_apply, hga, div_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (goal)
Goal:
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
inst_4 : TopologicalSpace α
inst_5 : TopologicalSpace β
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (SProd.sprod (β := Filter G₀) (𝓝 a) ⊤) (𝓝 (h a 0))
hga : ¬g a = 0
⊢ ContinuousAt (↿h ∘ fun (x : α) ↦ (x, f x / g x)) a
have funProp : g a ≠ 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (goal)
Goal:
G₀ : Type u_3
inst : TopologicalSpace G₀
inst_1 : GroupWithZero G₀
inst_2 : SeparatelyContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ map (fun (x : G₀) ↦ a * x) (𝓝 1) = 𝓝 a
have rw : 𝓝 (a * 1) = 𝓝 a
Tactic: rw [map_mul_left_nhds₀ ha, mul_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (goal)
Goal:
G₀ : Type u_3
inst : TopologicalSpace G₀
inst_1 : GroupWithZero G₀
inst_2 : SeparatelyContinuousMul G₀
a : G₀
ha : a ≠ 0
rw : 𝓝 (a * 1) = 𝓝 a
⊢ map (fun (x : G₀) ↦ a * x) (𝓝 1) = 𝓝 a
have rw₁ : 𝓝 a = 𝓝 a
Tactic: rw [map_mul_left_nhds₀ ha, mul_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (goal)
Goal:
G₀ : Type u_3
inst : TopologicalSpace G₀
inst_1 : GroupWithZero G₀
inst_2 : SeparatelyContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ map (fun (x : G₀) ↦ x * a) (𝓝 1) = 𝓝 a
have rw : 𝓝 (1 * a) = 𝓝 a
Tactic: rw [map_mul_right_nhds₀ ha, one_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupWithZero (goal)
Goal:
G₀ : Type u_3
inst : TopologicalSpace G₀
inst_1 : GroupWithZero G₀
inst_2 : SeparatelyContinuousMul G₀
a : G₀
ha : a ≠ 0
rw : 𝓝 (1 * a) = 𝓝 a
⊢ map (fun (x : G₀) ↦ x * a) (𝓝 1) = 𝓝 a
have rw₁ : 𝓝 a = 𝓝 a
Tactic: rw [map_mul_right_nhds₀ ha, one_mul]