case refine'_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 : A → A → Prop
a b : A
ha : a ∈ adjoin R s
hb : b ∈ adjoin R s
Hs : ∀ (x : A), x ∈ s → ∀ (y : A), y ∈ s → p x y
Halg : ∀ (r₁ r₂ : R), p (↑(algebraMap R A) r₁) (↑(algebraMap R A) r₂)
Halg_left : ∀ (r : R) (x : A), x ∈ s → p (↑(algebraMap R A) r) x
Halg_right : ∀ (r : R) (x : A), x ∈ s → p x (↑(algebraMap R A) r)
Hadd_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x : A), x ∈ s → p a x

case refine'_2
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 : A → A → Prop
a b : A
ha : a ∈ adjoin R s
hb : b ∈ adjoin R s
Hs : ∀ (x : A), x ∈ s → ∀ (y : A), y ∈ s → p x y
Halg : ∀ (r₁ r₂ : R), p (↑(algebraMap R A) r₁) (↑(algebraMap R A) r₂)
Halg_left : ∀ (r : R) (x : A), x ∈ s → p (↑(algebraMap R A) r) x
Halg_right : ∀ (r : R) (x : A), x ∈ s → p x (↑(algebraMap R A) r)
Hadd_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ * y₂)
r : R
⊢ p a (↑(algebraMap R A) r)
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 : A → A → Prop
a b : A
ha : a ∈ adjoin R s
hb : b ∈ adjoin R s
Hs : ∀ (x : A), x ∈ s → ∀ (y : A), y ∈ s → p x y
Halg : ∀ (r₁ r₂ : R), p (↑(algebraMap R A) r₁) (↑(algebraMap R A) r₂)
Halg_left : ∀ (r : R) (x : A), x ∈ s → p (↑(algebraMap R A) r) x
Halg_right : ∀ (r : R) (x : A), x ∈ s → p x (↑(algebraMap R A) r)
Hadd_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ p a b
refine' adjoin_induction hb _ (fun r => _) (Hadd_right a) (Hmul_right a)
no goals
case refine'_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 : A → A → Prop
a b : A
ha : a ∈ adjoin R s
hb : b ∈ adjoin R s
Hs : ∀ (x : A), x ∈ s → ∀ (y : A), y ∈ s → p x y
Halg : ∀ (r₁ r₂ : R), p (↑(algebraMap R A) r₁) (↑(algebraMap R A) r₂)
Halg_left : ∀ (r : R) (x : A), x ∈ s → p (↑(algebraMap R A) r) x
Halg_right : ∀ (r : R) (x : A), x ∈ s → p x (↑(algebraMap R A) r)
Hadd_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x : A), x ∈ s → p a x
exact adjoin_induction ha Hs Halg_left
  (fun x y Hx Hy z hz => Hadd_left x y z (Hx z hz) (Hy z hz))
  fun x y Hx Hy z hz => Hmul_left x y z (Hx z hz) (Hy z hz)
no goals
case refine'_2
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 : A → A → Prop
a b : A
ha : a ∈ adjoin R s
hb : b ∈ adjoin R s
Hs : ∀ (x : A), x ∈ s → ∀ (y : A), y ∈ s → p x y
Halg : ∀ (r₁ r₂ : R), p (↑(algebraMap R A) r₁) (↑(algebraMap R A) r₂)
Halg_left : ∀ (r : R) (x : A), x ∈ s → p (↑(algebraMap R A) r) x
Halg_right : ∀ (r : R) (x : A), x ∈ s → p x (↑(algebraMap R A) r)
Hadd_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ * y₂)
r : R
⊢ p a (↑(algebraMap R A) r)
exact adjoin_induction ha (Halg_right r) (fun r' => Halg r' r)
  (fun x y => Hadd_left x y ((algebraMap R A) r))
  fun x y => Hmul_left x y ((algebraMap R A) r)