awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α)
rw₄ 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 α)
⊢ HSMul.hSMul (β := Completion α) (a + 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]

Premises used: UniformSpace.Completion.coe_smul, add_smul, UniformSpace.Completion.coe_add
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 : β)
rw₂ rw₃ : Eq.{u_4 + 1} (α := β) 0 0
⊢ Eq.{u_4 + 1} (α := β) (Completion.extension.{u_3, u_4} (α := α) (⇑f : (a : α) → β) 0) 0

Tactic:
rw [← coe_zero, extension_coe hf, f.map_zero]

Premises used: AddMonoidHom.map_zero, UniformSpace.Completion.extension_coe, UniformSpace.Completion.coe_zero
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 b : Completion α
⊢ Continuous.{u_3, u_4} (Y := β) fun (x : Completion α × Completion α) ↦
    Completion.extension (⇑f : (a : α) → β) (x.1 + x.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 b : Completion α
⊢ Continuous.{u_3, u_4} (Y := β) fun (x : Completion α × Completion α) ↦
    HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) x.1) (Completion.extension (⇑f : (a : α) → β) x.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α) : β)
rw_mod_cast₈ :
  (f : (a : α) → β) (a + b) = HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (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 α))

Tactic:
rw_mod_cast [extension_coe hf, extension_coe hf, extension_coe hf, f.map_add]

Premises used: UniformSpace.Completion.extension_coe, AddMonoidHom.map_add
-- Module: Mathlib.Topology.Algebra.GroupCompletion
Goal:
α : 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 : Continuous.{u_3, u_4} (X := α) (Y := β) (⇑f : (a : α) → β)
a : α
⊢ Eq.{u_4 + 1} (α := β) ((f.extension hf : (a : Completion α) → β) (↑a : Completion α) : β) ((f : (a : α) → β) a : β)

Tactic:
UniformSpace.Completion.extension_coe (uniformContinuous_addMonoidHom_of_continuous hf) a

Premises used: UniformSpace.Completion.extension_coe, UniformSpace.Completion.extension, uniformContinuous_addMonoidHom_of_continuous, AbstractCompletion.extend, ite
-- Module: Mathlib.Topology.Algebra.GroupCompletion
Goal:
α : 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 : Continuous.{u_3, u_4} (X := α) (Y := β) (⇑f : (a : α) → β)
⊢ Continuous.{u_3, u_4} (X := Completion α) (Y := β) (⇑(f.extension hf) : (a : Completion α) → β)

Tactic:
UniformSpace.Completion.continuous_extension

Premises used: UniformSpace.Completion.extension, UniformSpace.Completion.continuous_extension, AbstractCompletion.extend, ite
-- Module: Mathlib.Topology.Algebra.GroupCompletion
Goal:
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
inst_3 : UniformSpace β
inst_4 : AddGroup β
inst_5 : IsUniformAddGroup β
f : α →+ β
hf : Continuous.{u_3, u_4} (X := α) (Y := β) (⇑f : (a : α) → β)
⊢ Continuous.{u_3, u_4} (X := Completion α) (Y := Completion β) (⇑(f.completion hf) : (a : Completion α) → Completion β)

Tactic:
continuous_map

Premises used: UniformSpace.Completion.map, UniformSpace.Completion.coe', Quotient, SeparationQuotient, SeparationQuotient.mk, UniformSpace.Completion.extension, UniformSpace.Completion.continuous_map, AbstractCompletion.map, AbstractCompletion.extend, UniformSpace.Completion, ite
-- Module: Mathlib.Topology.Algebra.GroupCompletion
Goal:
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
inst_3 : UniformSpace β
inst_4 : AddGroup β
inst_5 : IsUniformAddGroup β
f : α →+ β
hf : Continuous.{u_3, u_4} (X := α) (Y := β) (⇑f : (a : α) → β)
a : α
⊢ Eq.{u_4 + 1} (α := Completion β)
    (((f.completion hf : AddMonoidHom.{u_3, u_4} (Completion α) (Completion β)) : (a : Completion α) → Completion β)
        (↑a : Completion α) :
      Completion β)
    ((↑((f : (a : α) → β) a) : Completion β) : Completion β)

Tactic:
map_coe (uniformContinuous_addMonoidHom_of_continuous hf) a

Premises used: UniformSpace.Completion.map, UniformSpace.Completion.coe', UniformSpace.Completion.map_coe, Quotient, SeparationQuotient, SeparationQuotient.mk, UniformSpace.Completion.extension, uniformContinuous_addMonoidHom_of_continuous, AbstractCompletion.map, AbstractCompletion.extend, UniformSpace.Completion, ite
-- Module: Mathlib.Topology.Algebra.GroupCompletion
Goal:
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
inst_3 : UniformSpace β
inst_4 : AddGroup β
inst_5 : IsUniformAddGroup β
h :
  ∀ (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 β)
⊢ Eq (α := AddMonoidHom.{u_3, u_4} (Completion α) (Completion β)) (completion 0 ⋯) 0

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 β)

Tactic:
Completion.induction_on x ?_ ?_

Premises used: UniformSpace.Completion.induction_on
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 β)}
h₁ :
  ∀ (a : α),
    Eq.{u_4 + 1} (α := Completion β)
      ((completion 0 ⋯ : (a : Completion α) → Completion β) (↑a : Completion α) : Completion β)
      (((0 : AddMonoidHom.{u_3, u_4} (Completion α) (Completion β)) : (a : Completion α) → Completion β)
          (↑a : Completion α) :
        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 β)

Tactic:
refine Completion.induction_on x ?_ ?_
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 : Continuous.{u_3, u_4} (X := Completion α) (Y := Completion β) (⇑0 : (a : Completion α) → 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 β)}

Tactic:
apply isClosed_eq (AddMonoidHom.continuous_completion (0 : α →+ β) continuous_const)

Premises used: continuous_const, AddMonoidHom.continuous_completion, isClosed_eq, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α
⊢ Continuous.{u_3, u_4} (X := Completion α) (Y := Completion β) (⇑0 : (a : Completion α) → Completion β)

Tactic:
continuous_const

Premises used: UniformSpace.Completion.coe', continuous_const, SeparationQuotient.mk
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α
⊢ Continuous.{u_3, u_4} (X := Completion α) (Y := Completion β) (⇑0 : (a : Completion α) → Completion β)

Tactic:
exact continuous_const

Premises used: continuous_const
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α
⊢ ∀ (a : α),
    Eq.{u_4 + 1} (α := Completion β)
      ((completion 0 ⋯ : (a : Completion α) → Completion β) (↑a : Completion α) : Completion β)
      (((0 : AddMonoidHom.{u_3, u_4} (Completion α) (Completion β)) : (a : Completion α) → Completion β)
          (↑a : Completion α) :
        Completion β)

Tactic:
simp [(0 : α →+ β).completion_coe continuous_const, coe_zero]

Premises used: AddMonoidHom.completion_coe, continuous_const, UniformSpace.Completion.coe_zero, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 : α) → γ)
⊢ Continuous (HAdd.hAdd (α := α → γ) (⇑f : (a : α) → γ) (⇑g : (a : α) → γ))

Tactic:
have hfg := hf.add hg
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 : α) → γ))
h :
  ∀ (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 γ)
⊢ (f + g).completion ⋯ =
    HAdd.hAdd (α := AddMonoidHom.{u_3, u_5} (Completion α) (Completion γ)) (f.completion hf) (g.completion hg)

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 γ)

Tactic:
Completion.induction_on x ?_ ?_

Premises used: UniformSpace.Completion.induction_on
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 γ)}
h₁ :
  ∀ (a : α),
    Eq.{u_5 + 1} (α := Completion γ)
      ((((f + g).completion ⋯ : 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 γ)
⊢ 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 γ)

Tactic:
refine Completion.induction_on x ?_ ?_
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α
⊢ 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 γ)}

Tactic:
isClosed_eq ((f + g).continuous_completion hfg)
      ((f.continuous_completion hf).add (g.continuous_completion hg))

Premises used: AddMonoidHom.continuous_completion, isClosed_eq, HAdd.hAdd, Continuous.add
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α
⊢ 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 γ)}

Tactic:
exact isClosed_eq ((f + g).continuous_completion hfg)
      ((f.continuous_completion hf).add (g.continuous_completion hg))

Premises used: AddMonoidHom.continuous_completion, isClosed_eq, HAdd.hAdd, Continuous.add
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α
⊢ ∀ (a : α),
    Eq.{u_5 + 1} (α := Completion γ)
      ((((f + g).completion ⋯ : 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:
simp [(f + g).completion_coe hfg, coe_add, f.completion_coe hf, g.completion_coe hg]

Premises used: AddMonoidHom.completion_coe, HAdd.hAdd, UniformSpace.Completion.coe_add
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : DivInvMonoid G₀
inst_1 : TopologicalSpace G₀
inst_2 : SeparatelyContinuousMul G₀
f : α → G₀
l : Filter α
x : G₀
hf : Tendsto f l (𝓝 x)
y : G₀
⊢ Tendsto (fun (a : α) ↦ f a / y) l (𝓝 (x / y))

Tactic:
simpa only [div_eq_mul_inv] using hf.mul_const _

Premises used: Filter.Tendsto.mul_const, div_eq_mul_inv
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : DivInvMonoid G₀
inst_1 : TopologicalSpace G₀
inst_2 : SeparatelyContinuousMul G₀
f : α → G₀
inst_3 : TopologicalSpace α
a : α
hf : ContinuousAt f a
y : G₀
⊢ ContinuousAt.{u_1, u_3} (Y := G₀) (fun (x : α) ↦ f x / y) a

Tactic:
hf.div_const y

Premises used: ContinuousAt, Filter.Tendsto.div_const
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : DivInvMonoid G₀
inst_1 : TopologicalSpace G₀
inst_2 : SeparatelyContinuousMul G₀
f : α → G₀
s : Set α
inst_3 : TopologicalSpace α
a : α
hf : ContinuousWithinAt f s a
y : G₀
⊢ ContinuousWithinAt.{u_1, u_3} (Y := G₀) (fun (x : α) ↦ f x / y) s a

Tactic:
hf.div_const _

Premises used: ContinuousWithinAt, Filter.Tendsto.div_const
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : DivInvMonoid G₀
inst_1 : TopologicalSpace G₀
inst_2 : SeparatelyContinuousMul G₀
f : α → G₀
s : Set α
inst_3 : TopologicalSpace α
hf : ContinuousOn f s
y : G₀
⊢ ContinuousOn.{u_1, u_3} (Y := G₀) (fun (x : α) ↦ f x / y) s

Tactic:
simpa only [div_eq_mul_inv] using hf.mul_const _

Premises used: ContinuousOn.mul_const, div_eq_mul_inv
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : DivInvMonoid G₀
inst_1 : TopologicalSpace G₀
inst_2 : SeparatelyContinuousMul G₀
f : α → G₀
inst_3 : TopologicalSpace α
hf : Continuous[inst_3, inst_1] f
y : G₀
⊢ Continuous[inst_3, inst_1] fun (x : α) ↦ f x / y

Tactic:
simpa only [div_eq_mul_inv] using hf.mul_const _

Premises used: div_eq_mul_inv, Continuous.mul_const
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : Zero G₀
inst_1 : Inv G₀
inst_2 : TopologicalSpace G₀
inst_3 : ContinuousInv₀ G₀
x : G₀
hx : x ≠ 0
⊢ Tendsto Inv.inv (𝓝 x) (𝓝 x⁻¹)

Tactic:
continuousAt_inv₀ hx

Premises used: ContinuousInv₀.continuousAt_inv₀, ContinuousAt
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : Zero G₀
inst_1 : Inv G₀
inst_2 : TopologicalSpace G₀
inst_3 : ContinuousInv₀ G₀
⊢ ContinuousOn (X := G₀) Inv.inv {0}ᶜ

Tactic:
fun _x hx =>
  (continuousAt_inv₀ hx).continuousWithinAt

Premises used: ContinuousInv₀.continuousAt_inv₀, ContinuousAt.continuousWithinAt, ContinuousOn
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
α : Type u_1
G₀ : Type u_3
inst : Zero G₀
inst_1 : Inv G₀
inst_2 : TopologicalSpace G₀
inst_3 : ContinuousInv₀ G₀
l : Filter α
f : α → G₀
a : G₀
hf : Tendsto f l (𝓝 a)
ha : a ≠ 0
⊢ Tendsto (fun (x : α) ↦ (f x)⁻¹) l (𝓝 a⁻¹)

Tactic:
(tendsto_inv₀ ha).comp hf

Premises used: tendsto_inv₀, Filter.Tendsto.comp