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 s : Set A
x : { x // x ∈ ↑(adjoin R s) }
a : A
ha : a ∈ s
⊢ (fun y => y ∈ adjoin R (Subtype.val ⁻¹' s)) { val := a, property := (_ : a ∈ ↑(adjoin R s)) }

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 s : Set A
x : { x // x ∈ ↑(adjoin R s) }
r : R
⊢ (fun y => y ∈ adjoin R (Subtype.val ⁻¹' s)) (↑(algebraMap R { x // x ∈ adjoin R s }) r)

case refine'_3
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 s : Set A
x : { x // x ∈ ↑(adjoin R s) }
x✝¹ x✝ : { x // x ∈ adjoin R s }
⊢ (fun y => y ∈ adjoin R (Subtype.val ⁻¹' s)) x✝¹ →
    (fun y => y ∈ adjoin R (Subtype.val ⁻¹' s)) x✝ → (fun y => y ∈ adjoin R (Subtype.val ⁻¹' s)) (x✝¹ + x✝)

case refine'_4
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 s : Set A
x : { x // x ∈ ↑(adjoin R s) }
x✝¹ x✝ : { x // x ∈ adjoin R s }
⊢ (fun y => y ∈ adjoin R (Subtype.val ⁻¹' s)) x✝¹ →
    (fun y => y ∈ adjoin R (Subtype.val ⁻¹' s)) x✝ → (fun y => y ∈ adjoin R (Subtype.val ⁻¹' s)) (x✝¹ * x✝)
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 s : Set A
⊢ adjoin R (Subtype.val ⁻¹' s) = ⊤
refine'
  eq_top_iff.2 fun x =>
    adjoin_induction' (p := fun y => y ∈ adjoin R (((↑) : adjoin R s → A) ⁻¹' s))
    (fun a ha => _) (fun r => _) (fun _ _ => _) (fun _ _ => _) x
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 s : Set A
x : { x // x ∈ ↑(adjoin R s) }
a : A
ha : a ∈ s
⊢ (fun y => y ∈ adjoin R (Subtype.val ⁻¹' s)) { val := a, property := (_ : a ∈ ↑(adjoin R s)) }
exact subset_adjoin ha
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 s : Set A
x : { x // x ∈ ↑(adjoin R s) }
r : R
⊢ (fun y => y ∈ adjoin R (Subtype.val ⁻¹' s)) (↑(algebraMap R { x // x ∈ adjoin R s }) r)
exact Subalgebra.algebraMap_mem _ r
no goals
case refine'_3
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 s : Set A
x : { x // x ∈ ↑(adjoin R s) }
x✝¹ x✝ : { x // x ∈ adjoin R s }
⊢ (fun y => y ∈ adjoin R (Subtype.val ⁻¹' s)) x✝¹ →
    (fun y => y ∈ adjoin R (Subtype.val ⁻¹' s)) x✝ → (fun y => y ∈ adjoin R (Subtype.val ⁻¹' s)) (x✝¹ + x✝)
exact Subalgebra.add_mem _
no goals
case refine'_4
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 s : Set A
x : { x // x ∈ ↑(adjoin R s) }
x✝¹ x✝ : { x // x ∈ adjoin R s }
⊢ (fun y => y ∈ adjoin R (Subtype.val ⁻¹' s)) x✝¹ →
    (fun y => y ∈ adjoin R (Subtype.val ⁻¹' s)) x✝ → (fun y => y ∈ adjoin R (Subtype.val ⁻¹' s)) (x✝¹ * x✝)
exact Subalgebra.mul_mem _