-- Mathlib/Topology/Algebra/GroupCompletion.lean
theorem AddMonoidHom.completion_add {γ : Type*} [AddCommGroup γ] [UniformSpace γ]
    [UniformAddGroup γ] (f g : α →+ γ) (hf : Continuous f) (hg : Continuous g) :
    AddMonoidHom.completion (f + g) (hf.add hg) =
    AddMonoidHom.completion f hf + AddMonoidHom.completion g hg

Proof state:
case h.refine_2
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous fun x => f x + g x
x : Completion α
⊢ ∀ (a : α), ((f + g).completion ⋯) ↑a = (f.completion hf + g.completion hg) ↑a

Tactic:
intro a

Result:
case h.refine_2
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous fun x => f x + g x
x : Completion α
a : α
⊢ ((f + g).completion ⋯) ↑a = (f.completion hf + g.completion hg) ↑a

Proof state:
case h
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous fun x => f x + g x
x : Completion α
⊢ ((f + g).completion ⋯) x = (f.completion hf + g.completion hg) x

Tactic:
refine Completion.induction_on x ?_ ?_

Result:
case h.refine_1
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous fun x => f x + g x
x : Completion α
⊢ IsClosed {a | ((f + g).completion ⋯) a = (f.completion hf + g.completion hg) a}

case h.refine_2
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous fun x => f x + g x
x : Completion α
⊢ ∀ (a : α), ((f + g).completion ⋯) ↑a = (f.completion hf + g.completion hg) ↑a

Proof state:
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
⊢ (f + g).completion ⋯ = f.completion hf + g.completion hg

Tactic:
have hfg := hf.add hg

Result:
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous fun x => f x + g x
⊢ (f + g).completion ⋯ = f.completion hf + g.completion hg

Proof state:
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous fun x => f x + g x
⊢ (f + g).completion ⋯ = f.completion hf + g.completion hg

Tactic:
ext x

Result:
case h
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous fun x => f x + g x
x : Completion α
⊢ ((f + g).completion ⋯) x = (f.completion hf + g.completion hg) x

Proof state:
case h.refine_2
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous fun x => f x + g x
x : Completion α
a : α
⊢ ((f + g).completion ⋯) ↑a = (f.completion hf + g.completion hg) ↑a

Tactic:
simp [(f + g).completion_coe hfg, coe_add, f.completion_coe hf, g.completion_coe hg]

Result:
no goals

Proof state:
case h.refine_1
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous fun x => f x + g x
x : Completion α
⊢ IsClosed {a | ((f + g).completion ⋯) a = (f.completion hf + g.completion hg) a}

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

Result:
no goals