-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem ext_continuousAddMonoidHom
    {F : Type*} [AddCommMonoid F] [TopologicalSpace F] [T2Space F]
    [Fact (1 ≤ p)] (hp : p ≠ ⊤) ⦃f g : ContinuousAddMonoidHom (lp E p) F⦄
    (h : ∀ i,
      f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)) :
    f = g

Proof state:
case h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E i)
inst✝⁴ : DecidableEq α
F : Type u_5
inst✝³ : AddCommMonoid F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
f g : ContinuousAddMonoidHom (↥(lp E p)) F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
⊢ f x = g x

Tactic:
have := lp.hasSum_single hp x

Result:
case h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E i)
inst✝⁴ : DecidableEq α
F : Type u_5
inst✝³ : AddCommMonoid F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
f g : ContinuousAddMonoidHom (↥(lp E p)) F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
this : HasSum (fun i => lp.single p i (↑x i)) x
⊢ f x = g x

Proof state:
case h.h.e'_5.h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E i)
inst✝⁴ : DecidableEq α
F : Type u_5
inst✝³ : AddCommMonoid F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
f g : ContinuousAddMonoidHom (↥(lp E p)) F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
this : HasSum (fun i => lp.single p i (↑x i)) x
i : α
⊢ (⇑f ∘ fun i => lp.single p i (↑x i)) i = (⇑g ∘ fun i => lp.single p i (↑x i)) i

Tactic:
exact DFunLike.congr_fun (h i) (x i)

Result:
no goals

Proof state:
case h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E i)
inst✝⁴ : DecidableEq α
F : Type u_5
inst✝³ : AddCommMonoid F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
f g : ContinuousAddMonoidHom (↥(lp E p)) F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
this : HasSum (fun i => lp.single p i (↑x i)) x
⊢ f x = g x

Tactic:
rw [← (this.map f f.continuous).tsum_eq, ← (this.map g g.continuous).tsum_eq]

Result:
case h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E i)
inst✝⁴ : DecidableEq α
F : Type u_5
inst✝³ : AddCommMonoid F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
f g : ContinuousAddMonoidHom (↥(lp E p)) F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
this : HasSum (fun i => lp.single p i (↑x i)) x
⊢ ∑' (b : α), (⇑f ∘ fun i => lp.single p i (↑x i)) b = ∑' (b : α), (⇑g ∘ fun i => lp.single p i (↑x i)) b

Proof state:
case h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E i)
inst✝⁴ : DecidableEq α
F : Type u_5
inst✝³ : AddCommMonoid F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
f g : ContinuousAddMonoidHom (↥(lp E p)) F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
⊢ f x = g x

Tactic:
classical
have := lp.hasSum_single hp x
rw [← (this.map f f.continuous).tsum_eq, ← (this.map g g.continuous).tsum_eq]
congr! 2 with i
exact DFunLike.congr_fun (h i) (x i)

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E i)
inst✝⁴ : DecidableEq α
F : Type u_5
inst✝³ : AddCommMonoid F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
f g : ContinuousAddMonoidHom (↥(lp E p)) F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
⊢ f = g

Tactic:
ext x

Result:
case h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E i)
inst✝⁴ : DecidableEq α
F : Type u_5
inst✝³ : AddCommMonoid F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
f g : ContinuousAddMonoidHom (↥(lp E p)) F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
⊢ f x = g x

Proof state:
case h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E i)
inst✝⁴ : DecidableEq α
F : Type u_5
inst✝³ : AddCommMonoid F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
f g : ContinuousAddMonoidHom (↥(lp E p)) F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
this : HasSum (fun i => lp.single p i (↑x i)) x
⊢ ∑' (b : α), (⇑f ∘ fun i => lp.single p i (↑x i)) b = ∑' (b : α), (⇑g ∘ fun i => lp.single p i (↑x i)) b

Tactic:
congr! 2 with i

Result:
case h.h.e'_5.h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E i)
inst✝⁴ : DecidableEq α
F : Type u_5
inst✝³ : AddCommMonoid F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
f g : ContinuousAddMonoidHom (↥(lp E p)) F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
this : HasSum (fun i => lp.single p i (↑x i)) x
i : α
⊢ (⇑f ∘ fun i => lp.single p i (↑x i)) i = (⇑g ∘ fun i => lp.single p i (↑x i)) i