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

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✝² : IsScalarTower 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : φ (ContinuousMapZero.id h0) * a = 0
hmul_star_id : φ (star (ContinuousMapZero.id h0)) * a = 0
hφ : Continuous ⇑φ
⊢ φ 0 * a = 0

Tactic:
simp [map_zero]

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✝² : IsScalarTower 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : φ (ContinuousMapZero.id h0) * a = 0
hmul_star_id : φ (star (ContinuousMapZero.id h0)) * a = 0
hφ : Continuous ⇑φ
f : C(↑s, 𝕜)₀
⊢ φ f * a = 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, add_mul, h₁, h₂, zero_add]
| mul _ _ _ h => simp only [map_mul, mul_assoc, h, mul_zero]
| smul _ _ h => rw [map_smul, smul_mul_assoc, h, smul_zero]
| frequently f h => exact h.mem_of_closed <| isClosed_eq (by fun_prop) continuous_zero

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✝² : IsScalarTower 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : φ (ContinuousMapZero.id h0) * a = 0
hmul_star_id : φ (star (ContinuousMapZero.id h0)) * a = 0
hφ : Continuous ⇑φ
r✝ : 𝕜
f✝ : C(↑s, 𝕜)₀
h : φ f✝ * a = 0
⊢ φ (r✝ • f✝) * a = 0

Tactic:
rw [map_smul, smul_mul_assoc, h, smul_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✝² : IsScalarTower 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : φ (ContinuousMapZero.id h0) * a = 0
hmul_star_id : φ (star (ContinuousMapZero.id h0)) * a = 0
hφ : Continuous ⇑φ
f✝ g✝ : C(↑s, 𝕜)₀
a✝ : φ f✝ * a = 0
h : φ g✝ * a = 0
⊢ φ (f✝ * g✝) * a = 0

Tactic:
simp only [map_mul, mul_assoc, h, mul_zero]

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✝² : IsScalarTower 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : φ (ContinuousMapZero.id h0) * a = 0
hmul_star_id : φ (star (ContinuousMapZero.id h0)) * a = 0
hφ : Continuous ⇑φ
f : C(↑s, 𝕜)₀
h : ∃ᶠ (g : C(↑s, 𝕜)₀) in nhds f, φ g * a = 0
⊢ φ f * a = 0

Tactic:
exact h.mem_of_closed <| isClosed_eq (by fun_prop) continuous_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✝² : IsScalarTower 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : φ (ContinuousMapZero.id h0) * a = 0
hmul_star_id : φ (star (ContinuousMapZero.id h0)) * a = 0
hφ : Continuous ⇑φ
⊢ φ (star (ContinuousMapZero.id h0)) * a = 0

Tactic:
exact hmul_star_id

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✝² : IsScalarTower 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : φ (ContinuousMapZero.id h0) * a = 0
hmul_star_id : φ (star (ContinuousMapZero.id h0)) * a = 0
hφ : Continuous ⇑φ
⊢ φ (ContinuousMapZero.id h0) * a = 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✝² : IsScalarTower 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : φ (ContinuousMapZero.id h0) * a = 0
hmul_star_id : φ (star (ContinuousMapZero.id h0)) * a = 0
hφ : Continuous ⇑φ
f✝ g✝ : C(↑s, 𝕜)₀
h₁ : φ f✝ * a = 0
h₂ : φ g✝ * a = 0
⊢ φ (f✝ + g✝) * a = 0

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

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✝² : IsScalarTower 𝕜 A A
s : Set 𝕜
inst✝¹ : Zero ↑s
inst✝ : CompactSpace ↑s
h0 : ↑0 = 0
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : φ (ContinuousMapZero.id h0) * a = 0
hmul_star_id : φ (star (ContinuousMapZero.id h0)) * a = 0
hφ : Continuous ⇑φ
f : C(↑s, 𝕜)₀
h : ∃ᶠ (g : C(↑s, 𝕜)₀) in nhds f, φ g * a = 0
⊢ Continuous fun g => φ g * a

Tactic:
fun_prop

Result:
no goals