R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
p : { x // x ∈ adjoin R s } → Prop
Hs : ∀ (x : A) (h : x ∈ s), p { val := x, property := (_ : x ∈ ↑(adjoin R s)) }
Halg : ∀ (r : R), p (↑(algebraMap R { x // x ∈ adjoin R s }) r)
Hadd : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x + y)
Hmul : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x * y)
x✝ : { x // x ∈ adjoin R s }
x : A
hx : x ∈ adjoin R s
⊢ ∃ x_1, p { val := x, property := x_1 }
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
p : { x // x ∈ adjoin R s } → Prop
Hs : ∀ (x : A) (h : x ∈ s), p { val := x, property := (_ : x ∈ ↑(adjoin R s)) }
Halg : ∀ (r : R), p (↑(algebraMap R { x // x ∈ adjoin R s }) r)
Hadd : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x + y)
Hmul : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x * y)
x✝ : { x // x ∈ adjoin R s }
x : A
hx : x ∈ adjoin R s
⊢ p { val := x, property := hx }
refine' Exists.elim _ fun (hx : x ∈ adjoin R s) (hc : p ⟨x, hx⟩) => hc
no goals
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s t : Set A
p : { x // x ∈ adjoin R s } → Prop
Hs : ∀ (x : A) (h : x ∈ s), p { val := x, property := (_ : x ∈ ↑(adjoin R s)) }
Halg : ∀ (r : R), p (↑(algebraMap R { x // x ∈ adjoin R s }) r)
Hadd : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x + y)
Hmul : ∀ (x y : { x // x ∈ adjoin R s }), p x → p y → p (x * y)
x✝ : { x // x ∈ adjoin R s }
x : A
hx : x ∈ adjoin R s
⊢ ∃ x_1, p { val := x, property := x_1 }
exact adjoin_induction hx (fun x hx => ⟨subset_adjoin hx, Hs x hx⟩)
  (fun r => ⟨Subalgebra.algebraMap_mem _ r, Halg r⟩)
  (fun x y hx hy =>
    Exists.elim hx fun hx' hx =>
      Exists.elim hy fun hy' hy => ⟨Subalgebra.add_mem _ hx' hy', Hadd _ _ hx hy⟩)
  fun x y hx hy =>
    Exists.elim hx fun hx' hx =>
      Exists.elim hy fun hy' hy => ⟨Subalgebra.mul_mem _ hx' hy', Hmul _ _ hx hy⟩