-- Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
/-- To show that `l` is a one-sided approximate unit for `A`, it suffices to verify it only for
`m : A` with `0 ≤ m` and `‖m‖ < 1`. -/
lemma tendsto_mul_right_of_forall_nonneg_tendsto {l : Filter A}
    (h : ∀ m, 0 ≤ m → ‖m‖ < 1 → Tendsto (· * m) l (𝓝 m)) (m : A) :
    Tendsto (· * m) l (𝓝 m)

Proof state:
case intro.intro.intro
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x => x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → ↑({x | 0 ≤ x} ∩ ball 0 1)
⊢ Tendsto (fun x_1 => x_1 * ∑ i : Fin n, c i • ↑(x i)) l (𝓝 (∑ i : Fin n, c i • ↑(x i)))

Tactic:
simp_rw [Finset.mul_sum]

Result:
case intro.intro.intro
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x => x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → ↑({x | 0 ≤ x} ∩ ball 0 1)
⊢ Tendsto (fun x_1 => ∑ i : Fin n, x_1 * c i • ↑(x i)) l (𝓝 (∑ i : Fin n, c i • ↑(x i)))

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x => x * m) l (𝓝 m)
m : A
⊢ ?m.175052 ∈ span ?m.174534 ?m.175053

Tactic:
show m ∈ span ℂ ({x | 0 ≤ x} ∩ ball 0 1)

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x => x * m) l (𝓝 m)
m : A
⊢ m ∈ span ℂ ({x | 0 ≤ x} ∩ ball 0 1)

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x => x * m) l (𝓝 m)
m : A
⊢ Tendsto (fun x => x * m) l (𝓝 m)

Tactic:
obtain ⟨n, c, x, rfl⟩ := mem_span_set'.mp <| by
  show m ∈ span ℂ ({x | 0 ≤ x} ∩ ball 0 1)
  simp [span_nonneg_inter_unitBall]

Result:
case intro.intro.intro
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x => x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → ↑({x | 0 ≤ x} ∩ ball 0 1)
⊢ Tendsto (fun x_1 => x_1 * ∑ i : Fin n, c i • ↑(x i)) l (𝓝 (∑ i : Fin n, c i • ↑(x i)))

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x => x * m) l (𝓝 m)
m : A
⊢ m ∈ span ℂ ({x | 0 ≤ x} ∩ ball 0 1)

Tactic:
simp [span_nonneg_inter_unitBall]

Result:
no goals

Proof state:
case intro.intro.intro
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x => x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → ↑({x | 0 ≤ x} ∩ ball 0 1)
i : Fin n
x✝ : i ∈ Finset.univ
⊢ Tendsto (fun x_1 => c i • (x_1 * ↑(x i))) l (𝓝 (c i • ↑(x i)))

Tactic:
exact tendsto_const_nhds.smul <| h (x i) (x i).2.1 <| by simpa using (x i).2.2

Result:
no goals

Proof state:
case intro.intro.intro
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x => x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → ↑({x | 0 ≤ x} ∩ ball 0 1)
i : Fin n
x✝ : i ∈ Finset.univ
⊢ Tendsto (fun x_1 => x_1 * c i • ↑(x i)) l (𝓝 (c i • ↑(x i)))

Tactic:
simp_rw [mul_smul_comm]

Result:
case intro.intro.intro
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x => x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → ↑({x | 0 ≤ x} ∩ ball 0 1)
i : Fin n
x✝ : i ∈ Finset.univ
⊢ Tendsto (fun x_1 => c i • (x_1 * ↑(x i))) l (𝓝 (c i • ↑(x i)))

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x => x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → ↑({x | 0 ≤ x} ∩ ball 0 1)
i : Fin n
x✝ : i ∈ Finset.univ
⊢ ‖↑(x i)‖ < 1

Tactic:
simpa using (x i).2.2

Result:
no goals

Proof state:
case intro.intro.intro
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x => x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → ↑({x | 0 ≤ x} ∩ ball 0 1)
⊢ Tendsto (fun x_1 => ∑ i : Fin n, x_1 * c i • ↑(x i)) l (𝓝 (∑ i : Fin n, c i • ↑(x i)))

Tactic:
refine tendsto_finset_sum _ fun i _ ↦ ?_

Result:
case intro.intro.intro
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x => x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → ↑({x | 0 ≤ x} ∩ ball 0 1)
i : Fin n
x✝ : i ∈ Finset.univ
⊢ Tendsto (fun x_1 => x_1 * c i • ↑(x i)) l (𝓝 (c i • ↑(x i)))