-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
lemma ContinuousMapZero.mul_nonUnitalStarAlgHom_apply_eq_zero {𝕜 A : Type*}
    [RCLike 𝕜] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [IsTopologicalSemiring A]
    [T2Space A] [Module 𝕜 A] [SMulCommClass 𝕜 A A] {s : Set 𝕜} [Zero s] [CompactSpace s]
    (h0 : (0 : s) = (0 : 𝕜)) (φ : C(s, 𝕜)₀ →⋆ₙₐ[𝕜] A) (a : A) (hmul_id : a * φ (.id h0) = 0)
    (hmul_star_id : a * φ (star (.id h0)) = 0) (hφ : Continuous φ) (f : C(s, 𝕜)₀) :
    a * φ f = 0

Proof state:
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalSemiring A
inst✝⁴ : T2Space A
inst✝³ : Module 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : a * φ (ContinuousMapZero.id h0) = 0
hmul_star_id : a * φ (star (ContinuousMapZero.id h0)) = 0
hφ : Continuous ⇑φ
f : C(↑s, 𝕜)₀
h : ∃ᶠ (g : C(↑s, 𝕜)₀) in nhds f, a * φ g = 0
⊢ Continuous fun g => a * φ g

Tactic:
fun_prop

Result:
no goals

Proof state:
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalSemiring A
inst✝⁴ : T2Space A
inst✝³ : Module 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : a * φ (ContinuousMapZero.id h0) = 0
hmul_star_id : a * φ (star (ContinuousMapZero.id h0)) = 0
hφ : Continuous ⇑φ
f : C(↑s, 𝕜)₀
⊢ a * φ f = 0

Tactic:
induction f using ContinuousMapZero.induction_on_of_compact h0 with
| zero => simp [map_zero]
| id => exact hmul_id
| star_id => exact hmul_star_id
| add _ _ h₁ h₂ => simp only [map_add, mul_add, h₁, h₂, zero_add]
| mul _ _ h _ => simp only [map_mul, ← mul_assoc, h, zero_mul]
| smul _ _ h => rw [map_smul, mul_smul_comm, h, smul_zero]
| frequently f h => exact h.mem_of_closed <| isClosed_eq (by fun_prop) continuous_zero

Result:
no goals

Proof state:
case mul
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalSemiring A
inst✝⁴ : T2Space A
inst✝³ : Module 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : a * φ (ContinuousMapZero.id h0) = 0
hmul_star_id : a * φ (star (ContinuousMapZero.id h0)) = 0
hφ : Continuous ⇑φ
f✝ g✝ : C(↑s, 𝕜)₀
h : a * φ f✝ = 0
a✝ : a * φ g✝ = 0
⊢ a * φ (f✝ * g✝) = 0

Tactic:
simp only [map_mul, ← mul_assoc, h, zero_mul]

Result:
no goals

Proof state:
case id
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalSemiring A
inst✝⁴ : T2Space A
inst✝³ : Module 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : a * φ (ContinuousMapZero.id h0) = 0
hmul_star_id : a * φ (star (ContinuousMapZero.id h0)) = 0
hφ : Continuous ⇑φ
⊢ a * φ (ContinuousMapZero.id h0) = 0

Tactic:
exact hmul_id

Result:
no goals

Proof state:
case add
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalSemiring A
inst✝⁴ : T2Space A
inst✝³ : Module 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : a * φ (ContinuousMapZero.id h0) = 0
hmul_star_id : a * φ (star (ContinuousMapZero.id h0)) = 0
hφ : Continuous ⇑φ
f✝ g✝ : C(↑s, 𝕜)₀
h₁ : a * φ f✝ = 0
h₂ : a * φ g✝ = 0
⊢ a * φ (f✝ + g✝) = 0

Tactic:
simp only [map_add, mul_add, h₁, h₂, zero_add]

Result:
no goals

Proof state:
case smul
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalSemiring A
inst✝⁴ : T2Space A
inst✝³ : Module 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : a * φ (ContinuousMapZero.id h0) = 0
hmul_star_id : a * φ (star (ContinuousMapZero.id h0)) = 0
hφ : Continuous ⇑φ
r✝ : 𝕜
f✝ : C(↑s, 𝕜)₀
h : a * φ f✝ = 0
⊢ a * φ (r✝ • f✝) = 0

Tactic:
rw [map_smul, mul_smul_comm, h, smul_zero]

Result:
no goals

Proof state:
case star_id
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalSemiring A
inst✝⁴ : T2Space A
inst✝³ : Module 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : a * φ (ContinuousMapZero.id h0) = 0
hmul_star_id : a * φ (star (ContinuousMapZero.id h0)) = 0
hφ : Continuous ⇑φ
⊢ a * φ (star (ContinuousMapZero.id h0)) = 0

Tactic:
exact hmul_star_id

Result:
no goals

Proof state:
case frequently
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalSemiring A
inst✝⁴ : T2Space A
inst✝³ : Module 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : a * φ (ContinuousMapZero.id h0) = 0
hmul_star_id : a * φ (star (ContinuousMapZero.id h0)) = 0
hφ : Continuous ⇑φ
f : C(↑s, 𝕜)₀
h : ∃ᶠ (g : C(↑s, 𝕜)₀) in nhds f, a * φ g = 0
⊢ a * φ f = 0

Tactic:
exact h.mem_of_closed <| isClosed_eq (by fun_prop) continuous_zero

Result:
no goals

Proof state:
case zero
𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalSemiring A
inst✝⁴ : T2Space A
inst✝³ : Module 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : a * φ (ContinuousMapZero.id h0) = 0
hmul_star_id : a * φ (star (ContinuousMapZero.id h0)) = 0
hφ : Continuous ⇑φ
⊢ a * φ 0 = 0

Tactic:
simp [map_zero]

Result:
no goals