-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
/-- An induction principle for `C(s, 𝕜)₀`. -/
@[elab_as_elim]
lemma ContinuousMapZero.induction_on {s : Set 𝕜} [Zero s] (h0 : ((0 : s) : 𝕜) = 0)
    {p : C(s, 𝕜)₀ → Prop} (zero : p 0) (id : p (.id h0)) (star_id : p (star (.id h0)))
    (add : ∀ f g, p f → p g → p (f + g)) (mul : ∀ f g, p f → p g → p (f * g))
    (smul : ∀ (r : 𝕜) f, p f → p (r • f))
    (closure : (∀ f ∈ adjoin 𝕜 {(.id h0 : C(s, 𝕜)₀)}, p f) → ∀ f, p f) (f : C(s, 𝕜)₀) :
    p f

Proof state:
case mem.inl
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Zero ↑s
h0 : ↑0 = 0
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id h0)
star_id : p (star (ContinuousMapZero.id h0))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝ f : C(↑s, 𝕜)₀
⊢ p (ContinuousMapZero.id h0)

case mem.inr
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Zero ↑s
h0 : ↑0 = 0
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id h0)
star_id : p (star (ContinuousMapZero.id h0))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝ f : C(↑s, 𝕜)₀
⊢ p (star (ContinuousMapZero.id h0))

Tactic:
all_goals assumption

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Zero ↑s
h0 : ↑0 = 0
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id h0)
star_id : p (star (ContinuousMapZero.id h0))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝ f : C(↑s, 𝕜)₀
hf : f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}
⊢ p f

Tactic:
induction hf using NonUnitalAlgebra.adjoin_induction with
| mem f hf =>
  simp only [Set.mem_union, Set.mem_singleton_iff, Set.mem_star] at hf
  rw [star_eq_iff_star_eq, eq_comm (b := f)] at hf
  obtain (rfl | rfl) := hf
  all_goals assumption
| zero => exact zero
| add _ _ _ _ hf hg => exact add _ _ hf hg
| mul _ _ _ _ hf hg => exact mul _ _ hf hg
| smul _ _ _ hf => exact smul _ _ hf

Result:
no goals

Proof state:
case zero
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Zero ↑s
h0 : ↑0 = 0
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id h0)
star_id : p (star (ContinuousMapZero.id h0))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝ f : C(↑s, 𝕜)₀
⊢ p 0

Tactic:
exact zero

Result:
no goals

Proof state:
case mem
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Zero ↑s
h0 : ↑0 = 0
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id h0)
star_id : p (star (ContinuousMapZero.id h0))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝¹ f✝ f : C(↑s, 𝕜)₀
hf : f = ContinuousMapZero.id h0 ∨ star f = ContinuousMapZero.id h0
⊢ p f

Tactic:
rw [star_eq_iff_star_eq, eq_comm (b := f)] at hf

Result:
case mem
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Zero ↑s
h0 : ↑0 = 0
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id h0)
star_id : p (star (ContinuousMapZero.id h0))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝¹ f✝ f : C(↑s, 𝕜)₀
hf : f = ContinuousMapZero.id h0 ∨ f = star (ContinuousMapZero.id h0)
⊢ p f

Proof state:
case mem.inr
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Zero ↑s
h0 : ↑0 = 0
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id h0)
star_id : p (star (ContinuousMapZero.id h0))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝ f : C(↑s, 𝕜)₀
⊢ p (star (ContinuousMapZero.id h0))

Tactic:
assumption

Result:
no goals

Proof state:
case add
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Zero ↑s
h0 : ↑0 = 0
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id h0)
star_id : p (star (ContinuousMapZero.id h0))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝ f x✝ y✝ : C(↑s, 𝕜)₀
hx✝ : x✝ ∈ NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id h0} ∪ star {ContinuousMapZero.id h0})
hy✝ : y✝ ∈ NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id h0} ∪ star {ContinuousMapZero.id h0})
hf : p x✝
hg : p y✝
⊢ p (x✝ + y✝)

Tactic:
exact add _ _ hf hg

Result:
no goals

Proof state:
case smul
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Zero ↑s
h0 : ↑0 = 0
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id h0)
star_id : p (star (ContinuousMapZero.id h0))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝ f : C(↑s, 𝕜)₀
r✝ : 𝕜
x✝ : C(↑s, 𝕜)₀
hx✝ : x✝ ∈ NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id h0} ∪ star {ContinuousMapZero.id h0})
hf : p x✝
⊢ p (r✝ • x✝)

Tactic:
exact smul _ _ hf

Result:
no goals

Proof state:
case mem
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Zero ↑s
h0 : ↑0 = 0
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id h0)
star_id : p (star (ContinuousMapZero.id h0))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝¹ f✝ f : C(↑s, 𝕜)₀
hf : f = ContinuousMapZero.id h0 ∨ f = star (ContinuousMapZero.id h0)
⊢ p f

Tactic:
obtain (rfl | rfl) := hf

Result:
case mem.inl
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Zero ↑s
h0 : ↑0 = 0
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id h0)
star_id : p (star (ContinuousMapZero.id h0))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝ f : C(↑s, 𝕜)₀
⊢ p (ContinuousMapZero.id h0)

case mem.inr
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Zero ↑s
h0 : ↑0 = 0
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id h0)
star_id : p (star (ContinuousMapZero.id h0))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝ f : C(↑s, 𝕜)₀
⊢ p (star (ContinuousMapZero.id h0))