-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem adjoin_induction {p : (x : A) → x ∈ adjoin R s → Prop}
    (mem : ∀ (x) (hx : x ∈ s), p x (subset_adjoin hx))
    (algebraMap : ∀ r, p (algebraMap R A r) (algebraMap_mem _ r))
    (add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (add_mem hx hy))
    (mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy))
    {x : A} (hx : x ∈ adjoin R s) : p x hx :=
  let S : Subalgebra R A :=
    { carrier := { x | ∃ hx, p x hx }
      mul_mem'

Proof state:
case intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((_root_.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
x : A
hx : x ∈ adjoin R s
a✝ b✝ : A
w✝¹ : a✝ ∈ adjoin R s
hpx : p a✝ w✝¹
w✝ : b✝ ∈ adjoin R s
hpy : p b✝ w✝
⊢ a✝ + b✝ ∈ { carrier := {x | ∃ (hx : x ∈ adjoin R s), p x hx}, mul_mem' := ⋯, one_mem' := ⋯ }.carrier

Tactic:
exact ⟨_, add _ _ _ _ hpx hpy⟩

Result:
no goals

Proof state:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((_root_.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
x : A
hx : x ∈ adjoin R s
⊢ ∀ {a b : A},
    a ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx} →
      b ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx} → a * b ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx}

Tactic:
rintro _ _ ⟨_, hpx⟩ ⟨_, hpy⟩

Result:
case intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((_root_.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
x : A
hx : x ∈ adjoin R s
a✝ b✝ : A
w✝¹ : a✝ ∈ adjoin R s
hpx : p a✝ w✝¹
w✝ : b✝ ∈ adjoin R s
hpy : p b✝ w✝
⊢ a✝ * b✝ ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx}

Proof state:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((_root_.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
x : A
hx : x ∈ adjoin R s
⊢ ∀ {a b : A},
    a ∈ { carrier := {x | ∃ (hx : x ∈ adjoin R s), p x hx}, mul_mem' := ⋯, one_mem' := ⋯ }.carrier →
      b ∈ { carrier := {x | ∃ (hx : x ∈ adjoin R s), p x hx}, mul_mem' := ⋯, one_mem' := ⋯ }.carrier →
        a + b ∈ { carrier := {x | ∃ (hx : x ∈ adjoin R s), p x hx}, mul_mem' := ⋯, one_mem' := ⋯ }.carrier

Tactic:
rintro _ _ ⟨_, hpx⟩ ⟨_, hpy⟩

Result:
case intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((_root_.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
x : A
hx : x ∈ adjoin R s
a✝ b✝ : A
w✝¹ : a✝ ∈ adjoin R s
hpx : p a✝ w✝¹
w✝ : b✝ ∈ adjoin R s
hpy : p b✝ w✝
⊢ a✝ + b✝ ∈ { carrier := {x | ∃ (hx : x ∈ adjoin R s), p x hx}, mul_mem' := ⋯, one_mem' := ⋯ }.carrier

Proof state:
case intro.intro
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((_root_.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
x : A
hx : x ∈ adjoin R s
a✝ b✝ : A
w✝¹ : a✝ ∈ adjoin R s
hpx : p a✝ w✝¹
w✝ : b✝ ∈ adjoin R s
hpy : p b✝ w✝
⊢ a✝ * b✝ ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx}

Tactic:
exact ⟨_, mul _ _ _ _ hpx hpy⟩

Result:
no goals