-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
/-- The difference with `NonUnitalAlgebra.adjoin_induction` is that this acts on the subtype. -/
@[elab_as_elim, deprecated adjoin_induction (since := "2024-10-11")]
lemma adjoin_induction_subtype {s : Set A} {p : adjoin R s → Prop} (a : adjoin R s)
    (mem : ∀ x (h : x ∈ s), p ⟨x, subset_adjoin R h⟩)
    (add : ∀ x y, p x → p y → p (x + y)) (zero : p 0)
    (mul : ∀ x y, p x → p y → p (x * y)) (smul : ∀ (r : R) x, p x → p (r • x)) : p a :=
  Subtype.recOn a fun b hb => by
    induction hb using adjoin_induction with
    | mem _ h => exact mem _ h
    | zero => exact zero
    | mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add _ _ h₁ h₂
    | smul _ _ _ h => exact smul _ _ h

Proof state:
case zero
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
p : ↥(adjoin R s) → Prop
a : ↥(adjoin R s)
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
zero : p 0
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
smul : ∀ (r : R) (x : ↥(adjoin R s)), p x → p (r • x)
b : A
⊢ p ⟨0, ⋯⟩

Tactic:
exact zero

Result:
no goals

Proof state:
case add
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
p : ↥(adjoin R s) → Prop
a : ↥(adjoin R s)
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
zero : p 0
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
smul : ∀ (r : R) (x : ↥(adjoin R s)), p x → p (r • x)
b x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p ⟨x✝, hx✝⟩
h₂ : p ⟨y✝, hy✝⟩
⊢ p ⟨x✝ + y✝, ⋯⟩

Tactic:
exact add _ _ h₁ h₂

Result:
no goals

Proof state:
case mem
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
p : ↥(adjoin R s) → Prop
a : ↥(adjoin R s)
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
zero : p 0
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
smul : ∀ (r : R) (x : ↥(adjoin R s)), p x → p (r • x)
b x✝ : A
h : x✝ ∈ s
⊢ p ⟨x✝, ⋯⟩

Tactic:
exact mem _ h

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
p : ↥(adjoin R s) → Prop
a : ↥(adjoin R s)
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
zero : p 0
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
smul : ∀ (r : R) (x : ↥(adjoin R s)), p x → p (r • x)
b : A
hb : b ∈ adjoin R s
⊢ p ⟨b, hb⟩

Tactic:
induction hb using adjoin_induction with
| mem _ h => exact mem _ h
| zero => exact zero
| mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂
| add _ _ _ _ h₁ h₂ => exact add _ _ h₁ h₂
| smul _ _ _ h => exact smul _ _ h

Result:
no goals

Proof state:
case mul
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
p : ↥(adjoin R s) → Prop
a : ↥(adjoin R s)
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
zero : p 0
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
smul : ∀ (r : R) (x : ↥(adjoin R s)), p x → p (r • x)
b x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p ⟨x✝, hx✝⟩
h₂ : p ⟨y✝, hy✝⟩
⊢ p ⟨x✝ * y✝, ⋯⟩

Tactic:
exact mul _ _ h₁ h₂

Result:
no goals

Proof state:
case smul
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
p : ↥(adjoin R s) → Prop
a : ↥(adjoin R s)
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
zero : p 0
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
smul : ∀ (r : R) (x : ↥(adjoin R s)), p x → p (r • x)
b : A
r✝ : R
x✝ : A
hx✝ : x✝ ∈ adjoin R s
h : p ⟨x✝, hx✝⟩
⊢ p ⟨r✝ • x✝, ⋯⟩

Tactic:
exact smul _ _ h

Result:
no goals