[GOAL]
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
inst✝ : DecidableEq A
α : Type u_1
s : Finset α
f : { x // x ∈ s } → Finset A
⊢ adjoin R ↑(Finset.biUnion (Finset.attach s) f) = ⨆ (x : { x // x ∈ s }), adjoin R ↑(f x)
[PROOFSTEP]
simp [adjoin_iUnion]
[GOAL]
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
[PROOFSTEP]
refine' adjoin_induction hb _ (fun r => _) (Hadd_right a) (Hmul_right a)
[GOAL]
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
[PROOFSTEP]
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)
[GOAL]
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)
[PROOFSTEP]
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)
[GOAL]
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 }
[PROOFSTEP]
refine' Exists.elim _ fun (hx : x ∈ adjoin R s) (hc : p ⟨x, hx⟩) => hc
[GOAL]
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 }
[PROOFSTEP]
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⟩
[GOAL]
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) = ⊤
[PROOFSTEP]
refine'
  eq_top_iff.2
    fun x =>
      -- porting note: Lean could no longer infer the motive
    adjoin_induction' (p := fun y => y ∈ adjoin R (((↑) : adjoin R s → A) ⁻¹' s)) (fun a ha => _) (fun r => _)
      (fun _ _ => _) (fun _ _ => _) x
[GOAL]
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)) }
[PROOFSTEP]
exact subset_adjoin ha
[GOAL]
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)
[PROOFSTEP]
exact Subalgebra.algebraMap_mem _ r
[GOAL]
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✝)
[PROOFSTEP]
exact Subalgebra.add_mem _
[GOAL]
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✝)
[PROOFSTEP]
exact Subalgebra.mul_mem _
[GOAL]
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
⊢ adjoin R ⊥ = ⊥
[PROOFSTEP]
apply GaloisConnection.l_bot
[GOAL]
case gc
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
⊢ GaloisConnection (adjoin R) ?u
case u
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
⊢ Subalgebra R A → Set A
[PROOFSTEP]
exact Algebra.gc
[GOAL]
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
⊢ ↑Subalgebra.toSubmodule (adjoin R s) = span R ↑(Submonoid.closure s)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
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
⊢ ↑Subalgebra.toSubmodule (adjoin R s) ≤ span R ↑(Submonoid.closure s)
[PROOFSTEP]
intro r hr
[GOAL]
case a
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
r : A
hr : r ∈ ↑Subalgebra.toSubmodule (adjoin R s)
⊢ r ∈ span R ↑(Submonoid.closure s)
[PROOFSTEP]
rcases Subsemiring.mem_closure_iff_exists_list.1 hr with ⟨L, HL, rfl⟩
[GOAL]
case a.intro.intro
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
L : List (List A)
HL : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hr : List.sum (List.map List.prod L) ∈ ↑Subalgebra.toSubmodule (adjoin R s)
⊢ List.sum (List.map List.prod L) ∈ span R ↑(Submonoid.closure s)
[PROOFSTEP]
clear hr
[GOAL]
case a.intro.intro
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
L : List (List A)
HL : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.sum (List.map List.prod L) ∈ span R ↑(Submonoid.closure s)
[PROOFSTEP]
induction' L with hd tl ih
[GOAL]
case a.intro.intro.nil
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
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
HL : ∀ (t : List A), t ∈ [] → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.sum (List.map List.prod []) ∈ span R ↑(Submonoid.closure s)
[PROOFSTEP]
exact zero_mem _
[GOAL]
case a.intro.intro.cons
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
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
tl : List (List A)
ih :
  (∀ (t : List A), t ∈ tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s) →
    List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
HL : ∀ (t : List A), t ∈ hd :: tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.sum (List.map List.prod (hd :: tl)) ∈ span R ↑(Submonoid.closure s)
[PROOFSTEP]
rw [List.forall_mem_cons] at HL 
[GOAL]
case a.intro.intro.cons
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
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
tl : List (List A)
ih :
  (∀ (t : List A), t ∈ tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s) →
    List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
HL :
  (∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s) ∧
    ∀ (x : List A), x ∈ tl → ∀ (y : A), y ∈ x → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.sum (List.map List.prod (hd :: tl)) ∈ span R ↑(Submonoid.closure s)
[PROOFSTEP]
rw [List.map_cons, List.sum_cons]
[GOAL]
case a.intro.intro.cons
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
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
tl : List (List A)
ih :
  (∀ (t : List A), t ∈ tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s) →
    List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
HL :
  (∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s) ∧
    ∀ (x : List A), x ∈ tl → ∀ (y : A), y ∈ x → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.prod hd + List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
[PROOFSTEP]
refine' Submodule.add_mem _ _ (ih HL.2)
[GOAL]
case a.intro.intro.cons
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
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
tl : List (List A)
ih :
  (∀ (t : List A), t ∈ tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s) →
    List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
HL :
  (∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s) ∧
    ∀ (x : List A), x ∈ tl → ∀ (y : A), y ∈ x → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.prod hd ∈ span R ↑(Submonoid.closure s)
[PROOFSTEP]
replace HL := HL.1
[GOAL]
case a.intro.intro.cons
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
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
tl : List (List A)
ih :
  (∀ (t : List A), t ∈ tl → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s) →
    List.sum (List.map List.prod tl) ∈ span R ↑(Submonoid.closure s)
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.prod hd ∈ span R ↑(Submonoid.closure s)
[PROOFSTEP]
clear ih tl
[GOAL]
case a.intro.intro.cons
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
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ List.prod hd ∈ span R ↑(Submonoid.closure s)
[PROOFSTEP]
suffices ∃ (z r : _) (_hr : r ∈ Submonoid.closure s), z • r = List.prod hd
  by
  rcases this with ⟨z, r, hr, hzr⟩
  rw [← hzr]
  exact smul_mem _ _ (subset_span hr)
[GOAL]
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
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
this : ∃ z r _hr, z • r = List.prod hd
⊢ List.prod hd ∈ span R ↑(Submonoid.closure s)
[PROOFSTEP]
rcases this with ⟨z, r, hr, hzr⟩
[GOAL]
case intro.intro.intro
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
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
z : ?m.213266
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod hd
⊢ List.prod hd ∈ span R ↑(Submonoid.closure s)
[PROOFSTEP]
rw [← hzr]
[GOAL]
case intro.intro.intro
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
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
z : ?m.213266
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod hd
⊢ z • r ∈ span R ↑(Submonoid.closure s)
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
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ Type ?u.213363
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
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ?m.213266 → (r : A) → r ∈ Submonoid.closure s → HSMul ?m.213266 A A
[PROOFSTEP]
exact smul_mem _ _ (subset_span hr)
[GOAL]
case a.intro.intro.cons
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
L : List (List A)
HL✝ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ∃ z r _hr, z • r = List.prod hd
[PROOFSTEP]
induction' hd with hd tl ih
[GOAL]
case a.intro.intro.cons.nil
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
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : List A
HL✝ : ∀ (y : A), y ∈ hd → y ∈ Set.range ↑(algebraMap R A) ∪ s
HL : ∀ (y : A), y ∈ [] → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ∃ z r _hr, z • r = List.prod []
[PROOFSTEP]
exact ⟨1, 1, (Submonoid.closure s).one_mem', one_smul _ _⟩
[GOAL]
case a.intro.intro.cons.cons
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
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : A
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
HL : ∀ (y : A), y ∈ hd :: tl → y ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ∃ z r _hr, z • r = List.prod (hd :: tl)
[PROOFSTEP]
rw [List.forall_mem_cons] at HL 
[GOAL]
case a.intro.intro.cons.cons
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
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : A
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
HL : hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ∃ z r _hr, z • r = List.prod (hd :: tl)
[PROOFSTEP]
rcases ih HL.2 with ⟨z, r, hr, hzr⟩
[GOAL]
case a.intro.intro.cons.cons.intro.intro.intro
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
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : A
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
HL : hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod tl
⊢ ∃ z r _hr, z • r = List.prod (hd :: tl)
[PROOFSTEP]
rw [List.prod_cons, ← hzr]
[GOAL]
case a.intro.intro.cons.cons.intro.intro.intro
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
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : A
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
HL : hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod tl
⊢ ∃ z_1 r_1 _hr, z_1 • r_1 = hd * z • r
[PROOFSTEP]
rcases HL.1 with (⟨hd, rfl⟩ | hs)
[GOAL]
case a.intro.intro.cons.cons.intro.intro.intro.inl.intro
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
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod tl
hd : R
HL : ↑(algebraMap R A) hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ ∃ z_1 r_1 _hr, z_1 • r_1 = ↑(algebraMap R A) hd * z • r
[PROOFSTEP]
refine' ⟨hd * z, r, hr, _⟩
[GOAL]
case a.intro.intro.cons.cons.intro.intro.intro.inl.intro
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
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod tl
hd : R
HL : ↑(algebraMap R A) hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
⊢ (hd * z) • r = ↑(algebraMap R A) hd * z • r
[PROOFSTEP]
rw [Algebra.smul_def, Algebra.smul_def, (algebraMap _ _).map_mul, _root_.mul_assoc]
[GOAL]
case a.intro.intro.cons.cons.intro.intro.intro.inr
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
L : List (List A)
HL✝¹ : ∀ (t : List A), t ∈ L → ∀ (y : A), y ∈ t → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd✝ : List A
HL✝ : ∀ (y : A), y ∈ hd✝ → y ∈ Set.range ↑(algebraMap R A) ∪ s
hd : A
tl : List A
ih : (∀ (y : A), y ∈ tl → y ∈ Set.range ↑(algebraMap R A) ∪ s) → ∃ z r _hr, z • r = List.prod tl
HL : hd ∈ Set.range ↑(algebraMap R A) ∪ s ∧ ∀ (x : A), x ∈ tl → x ∈ Set.range ↑(algebraMap R A) ∪ s
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = List.prod tl
hs : hd ∈ s
⊢ ∃ z_1 r_1 _hr, z_1 • r_1 = hd * z • r
[PROOFSTEP]
exact ⟨z, hd * r, Submonoid.mul_mem _ (Submonoid.subset_closure hs) hr, (mul_smul_comm _ _ _).symm⟩
[GOAL]
case a
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
⊢ span R ↑(Submonoid.closure s) ≤ ↑Subalgebra.toSubmodule (adjoin R s)
[PROOFSTEP]
refine' span_le.2 _
[GOAL]
case a
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
⊢ ↑(Submonoid.closure s) ⊆ ↑(↑Subalgebra.toSubmodule (adjoin R s))
[PROOFSTEP]
change Submonoid.closure s ≤ (adjoin R s).toSubsemiring.toSubmonoid
[GOAL]
case a
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
⊢ Submonoid.closure s ≤ (adjoin R s).toSubsemiring.toSubmonoid
[PROOFSTEP]
exact Submonoid.closure_le.2 subset_adjoin
[GOAL]
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
t : Submodule R A
⊢ ↑Subalgebra.toSubmodule (adjoin R s) ≤ t ↔ ↑(Submonoid.closure s) ⊆ ↑t
[PROOFSTEP]
rw [adjoin_eq_span, span_le]
[GOAL]
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
f : A →ₐ[R] B
s : Set A
⊢ (fun x => x) '' s ⊆ (Subalgebra.comap f (adjoin R (↑f '' s))).toSubsemiring.toSubmonoid.toSubsemigroup.carrier
[PROOFSTEP]
simp only [Set.image_id', coe_carrier_toSubmonoid, Subalgebra.coe_toSubsemiring, Subalgebra.coe_comap]
[GOAL]
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
f : A →ₐ[R] B
s : Set A
⊢ s ⊆ ↑f ⁻¹' ↑(adjoin R ((fun a => ↑f a) '' s))
[PROOFSTEP]
exact fun x hx => subset_adjoin ⟨x, hx, rfl⟩
[GOAL]
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 : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), ↑f (a₁ * a₂) = ↑f a₁ * ↑f a₂
h : x ∈ adjoin R s
⊢ ↑f x ∈ adjoin R (↑f '' (s ∪ {1}))
[PROOFSTEP]
refine'
  @adjoin_induction R A _ _ _ _ (fun a => f a ∈ adjoin R (f '' (s ∪ {1}))) x h
    (fun a ha => subset_adjoin ⟨a, ⟨Set.subset_union_left _ _ ha, rfl⟩⟩) (fun r => _)
    (fun y z hy hz => by simpa [hy, hz] using Subalgebra.add_mem _ hy hz) fun y z hy hz => by
    simpa [hy, hz, hf y z] using Subalgebra.mul_mem _ hy hz
[GOAL]
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 : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), ↑f (a₁ * a₂) = ↑f a₁ * ↑f a₂
h : x ∈ adjoin R s
y z : A
hy : (fun a => ↑f a ∈ adjoin R (↑f '' (s ∪ {1}))) y
hz : (fun a => ↑f a ∈ adjoin R (↑f '' (s ∪ {1}))) z
⊢ (fun a => ↑f a ∈ adjoin R (↑f '' (s ∪ {1}))) (y + z)
[PROOFSTEP]
simpa [hy, hz] using Subalgebra.add_mem _ hy hz
[GOAL]
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 : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), ↑f (a₁ * a₂) = ↑f a₁ * ↑f a₂
h : x ∈ adjoin R s
y z : A
hy : (fun a => ↑f a ∈ adjoin R (↑f '' (s ∪ {1}))) y
hz : (fun a => ↑f a ∈ adjoin R (↑f '' (s ∪ {1}))) z
⊢ (fun a => ↑f a ∈ adjoin R (↑f '' (s ∪ {1}))) (y * z)
[PROOFSTEP]
simpa [hy, hz, hf y z] using Subalgebra.mul_mem _ hy hz
[GOAL]
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 : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), ↑f (a₁ * a₂) = ↑f a₁ * ↑f a₂
h : x ∈ adjoin R s
r : R
⊢ (fun a => ↑f a ∈ adjoin R (↑f '' (s ∪ {1}))) (↑(algebraMap R A) r)
[PROOFSTEP]
have : f 1 ∈ adjoin R (f '' (s ∪ {1})) := subset_adjoin ⟨1, ⟨Set.subset_union_right _ _ <| Set.mem_singleton 1, rfl⟩⟩
[GOAL]
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 : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), ↑f (a₁ * a₂) = ↑f a₁ * ↑f a₂
h : x ∈ adjoin R s
r : R
this : ↑f 1 ∈ adjoin R (↑f '' (s ∪ {1}))
⊢ (fun a => ↑f a ∈ adjoin R (↑f '' (s ∪ {1}))) (↑(algebraMap R A) r)
[PROOFSTEP]
convert Subalgebra.smul_mem (adjoin R (f '' (s ∪ {1}))) this r
[GOAL]
case h.e'_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 : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), ↑f (a₁ * a₂) = ↑f a₁ * ↑f a₂
h : x ∈ adjoin R s
r : R
this : ↑f 1 ∈ adjoin R (↑f '' (s ∪ {1}))
⊢ ↑f (↑(algebraMap R A) r) = r • ↑f 1
[PROOFSTEP]
rw [algebraMap_eq_smul_one]
[GOAL]
case h.e'_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 : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), ↑f (a₁ * a₂) = ↑f a₁ * ↑f a₂
h : x ∈ adjoin R s
r : R
this : ↑f 1 ∈ adjoin R (↑f '' (s ∪ {1}))
⊢ ↑f (r • 1) = r • ↑f 1
[PROOFSTEP]
exact f.map_smul _ _
[GOAL]
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
t : Set B
⊢ adjoin R (↑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ↑(LinearMap.inr R A B) '' (t ∪ {1})) =
    Subalgebra.prod (adjoin R s) (adjoin R t)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
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
t : Set B
⊢ adjoin R (↑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ↑(LinearMap.inr R A B) '' (t ∪ {1})) ≤
    Subalgebra.prod (adjoin R s) (adjoin R t)
[PROOFSTEP]
simp only [adjoin_le_iff, Set.insert_subset_iff, Subalgebra.zero_mem, Subalgebra.one_mem, subset_adjoin,
  -- the rest comes from `squeeze_simp`Set.union_subset_iff, LinearMap.coe_inl, Set.mk_preimage_prod_right,
  Set.image_subset_iff, SetLike.mem_coe, Set.mk_preimage_prod_left, LinearMap.coe_inr, and_self_iff,
  Set.union_singleton, Subalgebra.coe_prod]
[GOAL]
case a
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
t : Set B
⊢ Subalgebra.prod (adjoin R s) (adjoin R t) ≤
    adjoin R (↑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ↑(LinearMap.inr R A B) '' (t ∪ {1}))
[PROOFSTEP]
rintro ⟨a, b⟩ ⟨ha, hb⟩
[GOAL]
case a.mk.intro
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
t : Set B
a : A
b : B
ha : (a, b).fst ∈ ↑(adjoin R s)
hb : (a, b).snd ∈ ↑(adjoin R t)
⊢ (a, b) ∈ adjoin R (↑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ↑(LinearMap.inr R A B) '' (t ∪ {1}))
[PROOFSTEP]
let P := adjoin R (LinearMap.inl R A B '' (s ∪ {1}) ∪ LinearMap.inr R A B '' (t ∪ {1}))
[GOAL]
case a.mk.intro
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
t : Set B
a : A
b : B
ha : (a, b).fst ∈ ↑(adjoin R s)
hb : (a, b).snd ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (↑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ↑(LinearMap.inr R A B) '' (t ∪ {1}))
⊢ (a, b) ∈ adjoin R (↑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ↑(LinearMap.inr R A B) '' (t ∪ {1}))
[PROOFSTEP]
have Ha : (a, (0 : B)) ∈ adjoin R (LinearMap.inl R A B '' (s ∪ {1})) := mem_adjoin_of_map_mul R LinearMap.inl_map_mul ha
[GOAL]
case a.mk.intro
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
t : Set B
a : A
b : B
ha : (a, b).fst ∈ ↑(adjoin R s)
hb : (a, b).snd ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (↑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ↑(LinearMap.inr R A B) '' (t ∪ {1}))
Ha : (a, 0) ∈ adjoin R (↑(LinearMap.inl R A B) '' (s ∪ {1}))
⊢ (a, b) ∈ adjoin R (↑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ↑(LinearMap.inr R A B) '' (t ∪ {1}))
[PROOFSTEP]
have Hb : ((0 : A), b) ∈ adjoin R (LinearMap.inr R A B '' (t ∪ {1})) := mem_adjoin_of_map_mul R LinearMap.inr_map_mul hb
[GOAL]
case a.mk.intro
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
t : Set B
a : A
b : B
ha : (a, b).fst ∈ ↑(adjoin R s)
hb : (a, b).snd ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (↑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ↑(LinearMap.inr R A B) '' (t ∪ {1}))
Ha : (a, 0) ∈ adjoin R (↑(LinearMap.inl R A B) '' (s ∪ {1}))
Hb : (0, b) ∈ adjoin R (↑(LinearMap.inr R A B) '' (t ∪ {1}))
⊢ (a, b) ∈ adjoin R (↑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ↑(LinearMap.inr R A B) '' (t ∪ {1}))
[PROOFSTEP]
replace Ha : (a, (0 : B)) ∈ P := adjoin_mono (Set.subset_union_left _ _) Ha
[GOAL]
case a.mk.intro
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
t : Set B
a : A
b : B
ha : (a, b).fst ∈ ↑(adjoin R s)
hb : (a, b).snd ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (↑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ↑(LinearMap.inr R A B) '' (t ∪ {1}))
Hb : (0, b) ∈ adjoin R (↑(LinearMap.inr R A B) '' (t ∪ {1}))
Ha : (a, 0) ∈ P
⊢ (a, b) ∈ adjoin R (↑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ↑(LinearMap.inr R A B) '' (t ∪ {1}))
[PROOFSTEP]
replace Hb : ((0 : A), b) ∈ P := adjoin_mono (Set.subset_union_right _ _) Hb
[GOAL]
case a.mk.intro
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
t : Set B
a : A
b : B
ha : (a, b).fst ∈ ↑(adjoin R s)
hb : (a, b).snd ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (↑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ↑(LinearMap.inr R A B) '' (t ∪ {1}))
Ha : (a, 0) ∈ P
Hb : (0, b) ∈ P
⊢ (a, b) ∈ adjoin R (↑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ↑(LinearMap.inr R A B) '' (t ∪ {1}))
[PROOFSTEP]
simpa using Subalgebra.add_mem _ Ha Hb
[GOAL]
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
hcomm : ∀ (a : A), a ∈ s → ∀ (b : A), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ adjoin R s } := Subalgebra.toSemiring (adjoin R s)
x y : { x // x ∈ adjoin R s }
⊢ x * y = y * x
[PROOFSTEP]
ext
[GOAL]
case a
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
hcomm : ∀ (a : A), a ∈ s → ∀ (b : A), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ adjoin R s } := Subalgebra.toSemiring (adjoin R s)
x y : { x // x ∈ adjoin R s }
⊢ ↑(x * y) = ↑(y * x)
[PROOFSTEP]
simp only [Subalgebra.coe_mul]
[GOAL]
case a
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
hcomm : ∀ (a : A), a ∈ s → ∀ (b : A), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ adjoin R s } := Subalgebra.toSemiring (adjoin R s)
x y : { x // x ∈ adjoin R s }
⊢ ↑x * ↑y = ↑y * ↑x
[PROOFSTEP]
exact
  adjoin_induction₂ x.prop y.prop hcomm (fun _ _ => by rw [commutes]) (fun r x _hx => commutes r x)
    (fun r x _hx => (commutes r x).symm) (fun _ _ _ h₁ h₂ => by simp only [add_mul, mul_add, h₁, h₂])
    (fun _ _ _ h₁ h₂ => by simp only [add_mul, mul_add, h₁, h₂])
    (fun x₁ x₂ y₁ h₁ h₂ => by rw [mul_assoc, h₂, ← mul_assoc y₁, ← h₁, mul_assoc x₁]) fun x₁ x₂ y₁ h₁ h₂ => by
    rw [mul_assoc x₂, ← h₂, ← mul_assoc x₂, ← h₁, ← mul_assoc]
[GOAL]
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
hcomm : ∀ (a : A), a ∈ s → ∀ (b : A), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ adjoin R s } := Subalgebra.toSemiring (adjoin R s)
x y : { x // x ∈ adjoin R s }
x✝¹ x✝ : R
⊢ ↑(algebraMap R A) x✝¹ * ↑(algebraMap R A) x✝ = ↑(algebraMap R A) x✝ * ↑(algebraMap R A) x✝¹
[PROOFSTEP]
rw [commutes]
[GOAL]
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
hcomm : ∀ (a : A), a ∈ s → ∀ (b : A), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ adjoin R s } := Subalgebra.toSemiring (adjoin R s)
x y : { x // x ∈ adjoin R s }
x✝² x✝¹ x✝ : A
h₁ : x✝² * x✝ = x✝ * x✝²
h₂ : x✝¹ * x✝ = x✝ * x✝¹
⊢ (x✝² + x✝¹) * x✝ = x✝ * (x✝² + x✝¹)
[PROOFSTEP]
simp only [add_mul, mul_add, h₁, h₂]
[GOAL]
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
hcomm : ∀ (a : A), a ∈ s → ∀ (b : A), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ adjoin R s } := Subalgebra.toSemiring (adjoin R s)
x y : { x // x ∈ adjoin R s }
x✝² x✝¹ x✝ : A
h₁ : x✝² * x✝¹ = x✝¹ * x✝²
h₂ : x✝² * x✝ = x✝ * x✝²
⊢ x✝² * (x✝¹ + x✝) = (x✝¹ + x✝) * x✝²
[PROOFSTEP]
simp only [add_mul, mul_add, h₁, h₂]
[GOAL]
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
hcomm : ∀ (a : A), a ∈ s → ∀ (b : A), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ adjoin R s } := Subalgebra.toSemiring (adjoin R s)
x y : { x // x ∈ adjoin R s }
x₁ x₂ y₁ : A
h₁ : x₁ * y₁ = y₁ * x₁
h₂ : x₂ * y₁ = y₁ * x₂
⊢ x₁ * x₂ * y₁ = y₁ * (x₁ * x₂)
[PROOFSTEP]
rw [mul_assoc, h₂, ← mul_assoc y₁, ← h₁, mul_assoc x₁]
[GOAL]
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
hcomm : ∀ (a : A), a ∈ s → ∀ (b : A), b ∈ s → a * b = b * a
src✝ : Semiring { x // x ∈ adjoin R s } := Subalgebra.toSemiring (adjoin R s)
x y : { x // x ∈ adjoin R s }
x₁ x₂ y₁ : A
h₁ : x₁ * x₂ = x₂ * x₁
h₂ : x₁ * y₁ = y₁ * x₁
⊢ x₁ * (x₂ * y₁) = x₂ * y₁ * x₁
[PROOFSTEP]
rw [mul_assoc x₂, ← h₂, ← mul_assoc x₂, ← h₁, ← mul_assoc]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
⊢ ↑Subalgebra.toSubmodule (adjoin R (s ∪ t)) =
    ↑Subalgebra.toSubmodule (adjoin R s) * ↑Subalgebra.toSubmodule (adjoin R t)
[PROOFSTEP]
rw [adjoin_eq_span, adjoin_eq_span, adjoin_eq_span, span_mul_span]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
⊢ span R ↑(Submonoid.closure (s ∪ t)) = span R (↑(Submonoid.closure s) * ↑(Submonoid.closure t))
[PROOFSTEP]
congr 1 with z
[GOAL]
case e_s.h
R : Type u
A : Type v
B : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
z : A
⊢ z ∈ ↑(Submonoid.closure (s ∪ t)) ↔ z ∈ ↑(Submonoid.closure s) * ↑(Submonoid.closure t)
[PROOFSTEP]
simp [Submonoid.closure_union, Submonoid.mem_sup, Set.mem_mul]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
⊢ adjoin A ↑(adjoin R s) = adjoin A s
[PROOFSTEP]
apply le_antisymm (adjoin_le _)
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
⊢ adjoin A s ≤ adjoin A ↑(adjoin R s)
[PROOFSTEP]
exact adjoin_mono subset_adjoin
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
⊢ ↑(adjoin R s) ⊆ ↑(adjoin A s)
[PROOFSTEP]
change adjoin R s ≤ (adjoin A s).restrictScalars R
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
⊢ adjoin R s ≤ Subalgebra.restrictScalars R (adjoin A s)
[PROOFSTEP]
refine'
  adjoin_le
    _
      -- porting note: unclear why this was broken
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
⊢ s ⊆ ↑(Subalgebra.restrictScalars R (adjoin A s))
[PROOFSTEP]
have : (Subalgebra.restrictScalars R (adjoin A s) : Set B) = adjoin A s := rfl
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
this : ↑(Subalgebra.restrictScalars R (adjoin A s)) = ↑(adjoin A s)
⊢ s ⊆ ↑(Subalgebra.restrictScalars R (adjoin A s))
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set B
this : ↑(Subalgebra.restrictScalars R (adjoin A s)) = ↑(adjoin A s)
⊢ s ⊆ ↑(adjoin A s)
[PROOFSTEP]
exact subset_adjoin
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
x : B
hx : x ∈ adjoin R s
hr : ↑(algebraMap A B) r ∈ B'
⊢ ∃ n₀, ∀ (n : ℕ), n ≥ n₀ → r ^ n • x ∈ B'
[PROOFSTEP]
replace hx : x ∈ Subalgebra.toSubmodule (adjoin R s) := hx
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
x : B
hr : ↑(algebraMap A B) r ∈ B'
hx : x ∈ ↑Subalgebra.toSubmodule (adjoin R s)
⊢ ∃ n₀, ∀ (n : ℕ), n ≥ n₀ → r ^ n • x ∈ B'
[PROOFSTEP]
rw [adjoin_eq_span, Finsupp.mem_span_iff_total] at hx 
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
x : B
hr : ↑(algebraMap A B) r ∈ B'
hx : ∃ l, ↑(Finsupp.total (↑↑(Submonoid.closure s)) B R Subtype.val) l = x
⊢ ∃ n₀, ∀ (n : ℕ), n ≥ n₀ → r ^ n • x ∈ B'
[PROOFSTEP]
rcases hx with ⟨l, rfl : (l.sum fun (i : Submonoid.closure s) (c : R) => c • (i : B)) = x⟩
[GOAL]
case intro
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : ↑(algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
⊢ ∃ n₀, ∀ (n : ℕ), n ≥ n₀ → (r ^ n • Finsupp.sum l fun i c => c • ↑i) ∈ B'
[PROOFSTEP]
choose n₁ n₂ using fun x : Submonoid.closure s => Submonoid.pow_smul_mem_closure_smul r s x.prop
[GOAL]
case intro
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : ↑(algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : { x // x ∈ Submonoid.closure s } → ℕ
n₂ : ∀ (x : { x // x ∈ Submonoid.closure s }), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
⊢ ∃ n₀, ∀ (n : ℕ), n ≥ n₀ → (r ^ n • Finsupp.sum l fun i c => c • ↑i) ∈ B'
[PROOFSTEP]
use l.support.sup n₁
[GOAL]
case h
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : ↑(algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : { x // x ∈ Submonoid.closure s } → ℕ
n₂ : ∀ (x : { x // x ∈ Submonoid.closure s }), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
⊢ ∀ (n : ℕ), n ≥ Finset.sup l.support n₁ → (r ^ n • Finsupp.sum l fun i c => c • ↑i) ∈ B'
[PROOFSTEP]
intro n hn
[GOAL]
case h
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : ↑(algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : { x // x ∈ Submonoid.closure s } → ℕ
n₂ : ∀ (x : { x // x ∈ Submonoid.closure s }), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ Finset.sup l.support n₁
⊢ (r ^ n • Finsupp.sum l fun i c => c • ↑i) ∈ B'
[PROOFSTEP]
rw [Finsupp.smul_sum]
[GOAL]
case h
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : ↑(algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : { x // x ∈ Submonoid.closure s } → ℕ
n₂ : ∀ (x : { x // x ∈ Submonoid.closure s }), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ Finset.sup l.support n₁
⊢ (Finsupp.sum l fun a b => r ^ n • b • ↑a) ∈ B'
[PROOFSTEP]
refine' B'.toSubmodule.sum_mem _
[GOAL]
case h
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : ↑(algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : { x // x ∈ Submonoid.closure s } → ℕ
n₂ : ∀ (x : { x // x ∈ Submonoid.closure s }), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ Finset.sup l.support n₁
⊢ ∀ (c : ↑↑(Submonoid.closure s)), c ∈ l.support → (fun a b => r ^ n • b • ↑a) c (↑l c) ∈ ↑Subalgebra.toSubmodule B'
[PROOFSTEP]
intro a ha
[GOAL]
case h
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : ↑(algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : { x // x ∈ Submonoid.closure s } → ℕ
n₂ : ∀ (x : { x // x ∈ Submonoid.closure s }), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ Finset.sup l.support n₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
⊢ (fun a b => r ^ n • b • ↑a) a (↑l a) ∈ ↑Subalgebra.toSubmodule B'
[PROOFSTEP]
have : n ≥ n₁ a := le_trans (Finset.le_sup ha) hn
[GOAL]
case h
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : ↑(algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : { x // x ∈ Submonoid.closure s } → ℕ
n₂ : ∀ (x : { x // x ∈ Submonoid.closure s }), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ Finset.sup l.support n₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ (fun a b => r ^ n • b • ↑a) a (↑l a) ∈ ↑Subalgebra.toSubmodule B'
[PROOFSTEP]
dsimp only
[GOAL]
case h
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : ↑(algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : { x // x ∈ Submonoid.closure s } → ℕ
n₂ : ∀ (x : { x // x ∈ Submonoid.closure s }), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ Finset.sup l.support n₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ r ^ n • ↑l a • ↑a ∈ ↑Subalgebra.toSubmodule B'
[PROOFSTEP]
rw [← tsub_add_cancel_of_le this, pow_add, ← smul_smul, ← IsScalarTower.algebraMap_smul A (l a) (a : B),
  smul_smul (r ^ n₁ a), mul_comm, ← smul_smul, smul_def, map_pow, IsScalarTower.algebraMap_smul]
[GOAL]
case h
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : ↑(algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : { x // x ∈ Submonoid.closure s } → ℕ
n₂ : ∀ (x : { x // x ∈ Submonoid.closure s }), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ Finset.sup l.support n₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ ↑(algebraMap A B) r ^ (n - n₁ a) * ↑l a • r ^ n₁ a • ↑a ∈ ↑Subalgebra.toSubmodule B'
[PROOFSTEP]
apply Subalgebra.mul_mem _ (Subalgebra.pow_mem _ hr _) _
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : ↑(algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : { x // x ∈ Submonoid.closure s } → ℕ
n₂ : ∀ (x : { x // x ∈ Submonoid.closure s }), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ Finset.sup l.support n₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ ↑l a • r ^ n₁ a • ↑a ∈ B'
[PROOFSTEP]
refine' Subalgebra.smul_mem _ _ _
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : ↑(algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : { x // x ∈ Submonoid.closure s } → ℕ
n₂ : ∀ (x : { x // x ∈ Submonoid.closure s }), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ Finset.sup l.support n₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ r ^ n₁ a • ↑a ∈ B'
[PROOFSTEP]
change _ ∈ B'.toSubmonoid
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : ↑(algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : { x // x ∈ Submonoid.closure s } → ℕ
n₂ : ∀ (x : { x // x ∈ Submonoid.closure s }), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ Finset.sup l.support n₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ r ^ n₁ a • ↑a ∈ B'.toSubmonoid
[PROOFSTEP]
rw [← Submonoid.closure_eq B'.toSubmonoid]
[GOAL]
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
s✝ t : Set A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : ↑(algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : { x // x ∈ Submonoid.closure s } → ℕ
n₂ : ∀ (x : { x // x ∈ Submonoid.closure s }), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ Finset.sup l.support n₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ r ^ n₁ a • ↑a ∈ Submonoid.closure ↑B'.toSubmonoid
[PROOFSTEP]
apply Submonoid.closure_mono hs (n₂ a)
