[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)


[GOAL]
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
⊢ Basis (Fin (natDegree (minpoly K x))) K { x_1 // x_1 ∈ adjoin K {x} }
[PROOFSTEP]
have hST : Function.Injective (algebraMap (adjoin K ({ x } : Set S)) S) := Subtype.coe_injective
[GOAL]
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
⊢ Basis (Fin (natDegree (minpoly K x))) K { x_1 // x_1 ∈ adjoin K {x} }
[PROOFSTEP]
have hx' : IsIntegral K (⟨x, subset_adjoin (Set.mem_singleton x)⟩ : adjoin K ({ x } : Set S)) :=
  by
  apply (isIntegral_algebraMap_iff hST).mp
  convert hx
[GOAL]
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
⊢ IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
[PROOFSTEP]
apply (isIntegral_algebraMap_iff hST).mp
[GOAL]
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
⊢ IsIntegral K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
[PROOFSTEP]
convert hx
[GOAL]
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
⊢ Basis (Fin (natDegree (minpoly K x))) K { x_1 // x_1 ∈ adjoin K {x} }
[PROOFSTEP]
have minpoly_eq := minpoly.eq_of_algebraMap_eq hST hx' rfl
[GOAL]
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
⊢ Basis (Fin (natDegree (minpoly K x))) K { x_1 // x_1 ∈ adjoin K {x} }
[PROOFSTEP]
apply
  @Basis.mk (Fin (minpoly K x).natDegree) _ (adjoin K { x }) fun i => ⟨x, subset_adjoin (Set.mem_singleton x)⟩ ^ (i : ℕ)
[GOAL]
case hli
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
⊢ LinearIndependent K fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i
[PROOFSTEP]
have : LinearIndependent K _ := linearIndependent_pow (⟨x, self_mem_adjoin_singleton _ _⟩ : adjoin K { x })
[GOAL]
case hli
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
this : LinearIndependent K fun i => { val := x, property := (_ : x ∈ adjoin K {x}) } ^ ↑i
⊢ LinearIndependent K fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i
[PROOFSTEP]
rwa [minpoly_eq] at this
[GOAL]
case hsp
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
⊢ ⊤ ≤ Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
[PROOFSTEP]
rintro ⟨y, hy⟩ _
[GOAL]
case hsp.mk
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
y : S
hy : y ∈ adjoin K {x}
a✝ : { val := y, property := hy } ∈ ⊤
⊢ { val := y, property := hy } ∈
    Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
[PROOFSTEP]
have := hx'.mem_span_pow (y := ⟨y, hy⟩)
[GOAL]
case hsp.mk
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
y : S
hy : y ∈ adjoin K {x}
a✝ : { val := y, property := hy } ∈ ⊤
this :
  (∃ f, { val := y, property := hy } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f) →
    { val := y, property := hy } ∈
      Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
⊢ { val := y, property := hy } ∈
    Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
[PROOFSTEP]
rw [minpoly_eq] at this
[GOAL]
case hsp.mk
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
y : S
hy : y ∈ adjoin K {x}
a✝ : { val := y, property := hy } ∈ ⊤
this :
  (∃ f, { val := y, property := hy } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f) →
    { val := y, property := hy } ∈
      Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
⊢ { val := y, property := hy } ∈
    Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
[PROOFSTEP]
apply this
[GOAL]
case hsp.mk
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
y : S
hy : y ∈ adjoin K {x}
a✝ : { val := y, property := hy } ∈ ⊤
this :
  (∃ f, { val := y, property := hy } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f) →
    { val := y, property := hy } ∈
      Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
⊢ ∃ f, { val := y, property := hy } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f
[PROOFSTEP]
rw [adjoin_singleton_eq_range_aeval] at hy
[GOAL]
case hsp.mk
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
y : S
hy✝ : y ∈ adjoin K {x}
hy : y ∈ AlgHom.range (aeval x)
a✝ : { val := y, property := hy✝ } ∈ ⊤
this :
  (∃ f, { val := y, property := hy✝ } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f) →
    { val := y, property := hy✝ } ∈
      Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
⊢ ∃ f, { val := y, property := hy✝ } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f
[PROOFSTEP]
obtain ⟨f, rfl⟩ := (aeval x).mem_range.mp hy
[GOAL]
case hsp.mk.intro
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
f : K[X]
hy✝ : ↑(aeval x) f ∈ adjoin K {x}
hy : ↑(aeval x) f ∈ AlgHom.range (aeval x)
a✝ : { val := ↑(aeval x) f, property := hy✝ } ∈ ⊤
this :
  (∃ f_1, { val := ↑(aeval x) f, property := hy✝ } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f_1) →
    { val := ↑(aeval x) f, property := hy✝ } ∈
      Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
⊢ ∃ f_1, { val := ↑(aeval x) f, property := hy✝ } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f_1
[PROOFSTEP]
use f
[GOAL]
case h
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
f : K[X]
hy✝ : ↑(aeval x) f ∈ adjoin K {x}
hy : ↑(aeval x) f ∈ AlgHom.range (aeval x)
a✝ : { val := ↑(aeval x) f, property := hy✝ } ∈ ⊤
this :
  (∃ f_1, { val := ↑(aeval x) f, property := hy✝ } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f_1) →
    { val := ↑(aeval x) f, property := hy✝ } ∈
      Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
⊢ { val := ↑(aeval x) f, property := hy✝ } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f
[PROOFSTEP]
ext
[GOAL]
case h.a
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S)
hx' : IsIntegral K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }
minpoly_eq :
  minpoly K { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } =
    minpoly K (↑(algebraMap { x_1 // x_1 ∈ adjoin K {x} } S) { val := x, property := (_ : x ∈ ↑(adjoin K {x})) })
f : K[X]
hy✝ : ↑(aeval x) f ∈ adjoin K {x}
hy : ↑(aeval x) f ∈ AlgHom.range (aeval x)
a✝ : { val := ↑(aeval x) f, property := hy✝ } ∈ ⊤
this :
  (∃ f_1, { val := ↑(aeval x) f, property := hy✝ } = ↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f_1) →
    { val := ↑(aeval x) f, property := hy✝ } ∈
      Submodule.span K (Set.range fun i => { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i)
⊢ ↑{ val := ↑(aeval x) f, property := hy✝ } = ↑(↑(aeval { val := x, property := (_ : x ∈ ↑(adjoin K {x})) }) f)
[PROOFSTEP]
exact aeval_algebraMap_apply S (⟨x, _⟩ : adjoin K { x }) _
[GOAL]
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
i : Fin (natDegree (minpoly K x))
⊢ ↑(powerBasisAux hx) i = { val := x, property := (_ : x ∈ ↑(adjoin K {x})) } ^ ↑i
[PROOFSTEP]
rw [adjoin.powerBasisAux, Basis.mk_apply]
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
⊢ ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (B.gen ^ n)) i)
[PROOFSTEP]
intro i
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
⊢ IsIntegral R (↑(↑B.basis.repr (B.gen ^ n)) i)
[PROOFSTEP]
let Q := X ^ n %ₘ minpoly R B.gen
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
⊢ IsIntegral R (↑(↑B.basis.repr (B.gen ^ n)) i)
[PROOFSTEP]
have : B.gen ^ n = aeval B.gen Q :=
  by
  rw [← @aeval_X_pow R _ _ _ _ B.gen, ← modByMonic_add_div (X ^ n) (minpoly.monic hB)]
  simp
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
⊢ B.gen ^ n = ↑(aeval B.gen) Q
[PROOFSTEP]
rw [← @aeval_X_pow R _ _ _ _ B.gen, ← modByMonic_add_div (X ^ n) (minpoly.monic hB)]
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
⊢ ↑(aeval B.gen) (X ^ n %ₘ minpoly R B.gen + minpoly R B.gen * (X ^ n /ₘ minpoly R B.gen)) = ↑(aeval B.gen) Q
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
⊢ IsIntegral R (↑(↑B.basis.repr (B.gen ^ n)) i)
[PROOFSTEP]
by_cases hQ : Q = 0
[GOAL]
case pos
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : Q = 0
⊢ IsIntegral R (↑(↑B.basis.repr (B.gen ^ n)) i)
[PROOFSTEP]
simp [this, hQ, isIntegral_zero]
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
⊢ IsIntegral R (↑(↑B.basis.repr (B.gen ^ n)) i)
[PROOFSTEP]
have hlt : Q.natDegree < B.dim :=
  by
  rw [← B.natDegree_minpoly, hmin, (minpoly.monic hB).natDegree_map, natDegree_lt_natDegree_iff hQ]
  letI : Nontrivial R := Nontrivial.of_polynomial_ne hQ
  exact degree_modByMonic_lt _ (minpoly.monic hB)
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
⊢ natDegree Q < B.dim
[PROOFSTEP]
rw [← B.natDegree_minpoly, hmin, (minpoly.monic hB).natDegree_map, natDegree_lt_natDegree_iff hQ]
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
⊢ degree Q < degree (minpoly R B.gen)
[PROOFSTEP]
letI : Nontrivial R := Nontrivial.of_polynomial_ne hQ
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this✝ : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
this : Nontrivial R := Nontrivial.of_polynomial_ne hQ
⊢ degree Q < degree (minpoly R B.gen)
[PROOFSTEP]
exact degree_modByMonic_lt _ (minpoly.monic hB)
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
⊢ IsIntegral R (↑(↑B.basis.repr (B.gen ^ n)) i)
[PROOFSTEP]
rw [this, aeval_eq_sum_range' hlt]
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
⊢ IsIntegral R (↑(↑B.basis.repr (Finset.sum (Finset.range B.dim) fun i => coeff Q i • B.gen ^ i)) i)
[PROOFSTEP]
simp only [LinearEquiv.map_sum, LinearEquiv.map_smulₛₗ, RingHom.id_apply, Finset.sum_apply']
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
⊢ IsIntegral R
    (Finset.sum (Finset.range B.dim) fun x => ↑(↑B.basis.repr (coeff (X ^ n %ₘ minpoly R B.gen) x • B.gen ^ x)) i)
[PROOFSTEP]
refine' IsIntegral.sum _ fun j hj => _
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
j : ℕ
hj : j ∈ Finset.range B.dim
⊢ IsIntegral R (↑(↑B.basis.repr (coeff (X ^ n %ₘ minpoly R B.gen) j • B.gen ^ j)) i)
[PROOFSTEP]
replace hj := Finset.mem_range.1 hj
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
j : ℕ
hj : j < B.dim
⊢ IsIntegral R (↑(↑B.basis.repr (coeff (X ^ n %ₘ minpoly R B.gen) j • B.gen ^ j)) i)
[PROOFSTEP]
rw [← Fin.val_mk hj, ← B.basis_eq_pow, Algebra.smul_def, IsScalarTower.algebraMap_apply R S A, ← Algebra.smul_def,
  LinearEquiv.map_smul]
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
j : ℕ
hj : j < B.dim
⊢ IsIntegral R
    (↑(↑(algebraMap R S) (coeff (X ^ n %ₘ minpoly R B.gen) ↑{ val := j, isLt := hj }) •
          ↑B.basis.repr (↑B.basis { val := j, isLt := hj }))
      i)
[PROOFSTEP]
simp only [algebraMap_smul, Finsupp.coe_smul, Pi.smul_apply, B.basis.repr_self_apply]
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
j : ℕ
hj : j < B.dim
⊢ IsIntegral R (coeff (X ^ n %ₘ minpoly R B.gen) j • if { val := j, isLt := hj } = i then 1 else 0)
[PROOFSTEP]
by_cases hij : (⟨j, hj⟩ : Fin _) = i
[GOAL]
case pos
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
j : ℕ
hj : j < B.dim
hij : { val := j, isLt := hj } = i
⊢ IsIntegral R (coeff (X ^ n %ₘ minpoly R B.gen) j • if { val := j, isLt := hj } = i then 1 else 0)
[PROOFSTEP]
simp only [hij, eq_self_iff_true, if_true]
[GOAL]
case pos
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
j : ℕ
hj : j < B.dim
hij : { val := j, isLt := hj } = i
⊢ IsIntegral R (coeff (X ^ n %ₘ minpoly R B.gen) j • 1)
[PROOFSTEP]
rw [Algebra.smul_def, mul_one]
[GOAL]
case pos
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
j : ℕ
hj : j < B.dim
hij : { val := j, isLt := hj } = i
⊢ IsIntegral R (↑(algebraMap R S) (coeff (X ^ n %ₘ minpoly R B.gen) j))
[PROOFSTEP]
exact isIntegral_algebraMap
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = ↑(aeval B.gen) Q
hQ : ¬Q = 0
hlt : natDegree Q < B.dim
j : ℕ
hj : j < B.dim
hij : ¬{ val := j, isLt := hj } = i
⊢ IsIntegral R (coeff (X ^ n %ₘ minpoly R B.gen) j • if { val := j, isLt := hj } = i then 1 else 0)
[PROOFSTEP]
simp [hij, isIntegral_zero]
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x y : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
⊢ ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x * y)) i)
[PROOFSTEP]
intro i
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x y : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
i : Fin B.dim
⊢ IsIntegral R (↑(↑B.basis.repr (x * y)) i)
[PROOFSTEP]
rw [← B.basis.sum_repr x, ← B.basis.sum_repr y, Finset.sum_mul_sum, LinearEquiv.map_sum, Finset.sum_apply']
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x y : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
i : Fin B.dim
⊢ IsIntegral R
    (Finset.sum (Finset.univ ×ˢ Finset.univ) fun k =>
      ↑(↑B.basis.repr (↑(↑B.basis.repr x) k.fst • ↑B.basis k.fst * ↑(↑B.basis.repr y) k.snd • ↑B.basis k.snd)) i)
[PROOFSTEP]
refine' IsIntegral.sum _ fun I _ => _
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x y : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
i : Fin B.dim
I : Fin B.dim × Fin B.dim
x✝ : I ∈ Finset.univ ×ˢ Finset.univ
⊢ IsIntegral R
    (↑(↑B.basis.repr (↑(↑B.basis.repr x) I.fst • ↑B.basis I.fst * ↑(↑B.basis.repr y) I.snd • ↑B.basis I.snd)) i)
[PROOFSTEP]
simp only [Algebra.smul_mul_assoc, Algebra.mul_smul_comm, LinearEquiv.map_smulₛₗ, RingHom.id_apply, Finsupp.coe_smul,
  Pi.smul_apply, id.smul_eq_mul]
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x y : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
i : Fin B.dim
I : Fin B.dim × Fin B.dim
x✝ : I ∈ Finset.univ ×ˢ Finset.univ
⊢ IsIntegral R
    ((↑(↑B.basis.repr y) I.snd • ↑(↑B.basis.repr x) I.fst • ↑(↑B.basis.repr (↑B.basis I.fst * ↑B.basis I.snd))) i)
[PROOFSTEP]
refine' isIntegral_mul (hy _) (isIntegral_mul (hx _) _)
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x y : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
i : Fin B.dim
I : Fin B.dim × Fin B.dim
x✝ : I ∈ Finset.univ ×ˢ Finset.univ
⊢ IsIntegral R (↑(↑B.basis.repr (↑B.basis I.fst * ↑B.basis I.snd)) i)
[PROOFSTEP]
simp only [coe_basis, ← pow_add]
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x y : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
i : Fin B.dim
I : Fin B.dim × Fin B.dim
x✝ : I ∈ Finset.univ ×ˢ Finset.univ
⊢ IsIntegral R (↑(↑B.basis.repr (B.gen ^ (↑I.fst + ↑I.snd))) i)
[PROOFSTEP]
refine' repr_gen_pow_isIntegral hB hmin _ _
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
⊢ ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ n)) i)
[PROOFSTEP]
nontriviality A using Subsingleton.elim (x ^ n) 0, isIntegral_zero
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
✝ : Nontrivial A
⊢ ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ n)) i)
[PROOFSTEP]
revert hx
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
✝ : Nontrivial A
⊢ (∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)) →
    ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ n)) i)
[PROOFSTEP]
refine'
  Nat.case_strong_induction_on (p := fun n ↦ _ → ∀ (i : Fin B.dim), IsIntegral R (B.basis.repr (x ^ n) i)) n _
    fun n hn => _
[GOAL]
case refine'_1
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
✝ : Nontrivial A
⊢ (fun n =>
      (∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)) →
        ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ n)) i))
    0
[PROOFSTEP]
intro _ i
[GOAL]
case refine'_1
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
✝ : Nontrivial A
a✝ : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
i : Fin B.dim
⊢ IsIntegral R (↑(↑B.basis.repr (x ^ 0)) i)
[PROOFSTEP]
rw [pow_zero, ← pow_zero B.gen, ← Fin.val_mk B.dim_pos, ← B.basis_eq_pow, B.basis.repr_self_apply]
[GOAL]
case refine'_1
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
✝ : Nontrivial A
a✝ : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
i : Fin B.dim
⊢ IsIntegral R (if { val := 0, isLt := (_ : 0 < B.dim) } = i then 1 else 0)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
✝ : Nontrivial A
a✝ : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
i : Fin B.dim
h✝ : { val := 0, isLt := (_ : 0 < B.dim) } = i
⊢ IsIntegral R 1
[PROOFSTEP]
exact isIntegral_one
[GOAL]
case neg
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
✝ : Nontrivial A
a✝ : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
i : Fin B.dim
h✝ : ¬{ val := 0, isLt := (_ : 0 < B.dim) } = i
⊢ IsIntegral R 0
[PROOFSTEP]
exact isIntegral_zero
[GOAL]
case refine'_2
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n✝ : ℕ
✝ : Nontrivial A
n : ℕ
hn :
  ∀ (m : ℕ),
    m ≤ n →
      (fun n =>
          (∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)) →
            ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ n)) i))
        m
⊢ (fun n =>
      (∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)) →
        ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ n)) i))
    (Nat.succ n)
[PROOFSTEP]
intro hx
[GOAL]
case refine'_2
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n✝ : ℕ
✝ : Nontrivial A
n : ℕ
hn :
  ∀ (m : ℕ),
    m ≤ n →
      (fun n =>
          (∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)) →
            ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ n)) i))
        m
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
⊢ ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ Nat.succ n)) i)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case refine'_2
K : Type u_1
S : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra K S
R : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R K
inst✝⁵ : IsScalarTower R K S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n✝ : ℕ
✝ : Nontrivial A
n : ℕ
hn :
  ∀ (m : ℕ),
    m ≤ n →
      (fun n =>
          (∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)) →
            ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x ^ n)) i))
        m
hx : ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr x) i)
⊢ ∀ (i : Fin B.dim), IsIntegral R (↑(↑B.basis.repr (x * x ^ n)) i)
[PROOFSTEP]
exact repr_mul_isIntegral hB hx (fun _ => hn _ le_rfl (fun _ => hx _) _) hmin
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : CommRing S
inst✝⁸ : Algebra K S
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B✝ : PowerBasis S A
hB✝ : IsIntegral R B✝.gen
B B' : PowerBasis K S
P : R[X]
h : ↑(aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
⊢ ∀ (i : Fin B.dim) (j : Fin B'.dim), IsIntegral R (Basis.toMatrix B.basis (↑B'.basis) i j)
[PROOFSTEP]
intro i j
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : CommRing S
inst✝⁸ : Algebra K S
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B✝ : PowerBasis S A
hB✝ : IsIntegral R B✝.gen
B B' : PowerBasis K S
P : R[X]
h : ↑(aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i : Fin B.dim
j : Fin B'.dim
⊢ IsIntegral R (Basis.toMatrix B.basis (↑B'.basis) i j)
[PROOFSTEP]
rw [B.basis.toMatrix_apply, B'.coe_basis]
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : CommRing S
inst✝⁸ : Algebra K S
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B✝ : PowerBasis S A
hB✝ : IsIntegral R B✝.gen
B B' : PowerBasis K S
P : R[X]
h : ↑(aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i : Fin B.dim
j : Fin B'.dim
⊢ IsIntegral R (↑(↑B.basis.repr ((fun i => B'.gen ^ ↑i) j)) i)
[PROOFSTEP]
refine' repr_pow_isIntegral hB (fun i => _) hmin _ _
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : CommRing S
inst✝⁸ : Algebra K S
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B✝ : PowerBasis S A
hB✝ : IsIntegral R B✝.gen
B B' : PowerBasis K S
P : R[X]
h : ↑(aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i✝ : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
⊢ IsIntegral R (↑(↑B.basis.repr B'.gen) i)
[PROOFSTEP]
rw [← h, aeval_eq_sum_range, LinearEquiv.map_sum, Finset.sum_apply']
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : CommRing S
inst✝⁸ : Algebra K S
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B✝ : PowerBasis S A
hB✝ : IsIntegral R B✝.gen
B B' : PowerBasis K S
P : R[X]
h : ↑(aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i✝ : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
⊢ IsIntegral R (Finset.sum (Finset.range (natDegree P + 1)) fun k => ↑(↑B.basis.repr (coeff P k • B.gen ^ k)) i)
[PROOFSTEP]
refine' IsIntegral.sum _ fun n _ => _
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : CommRing S
inst✝⁸ : Algebra K S
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B✝ : PowerBasis S A
hB✝ : IsIntegral R B✝.gen
B B' : PowerBasis K S
P : R[X]
h : ↑(aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i✝ : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
n : ℕ
x✝ : n ∈ Finset.range (natDegree P + 1)
⊢ IsIntegral R (↑(↑B.basis.repr (coeff P n • B.gen ^ n)) i)
[PROOFSTEP]
rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R K S, ← Algebra.smul_def, LinearEquiv.map_smul, algebraMap_smul]
[GOAL]
K : Type u_1
S : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : CommRing S
inst✝⁸ : Algebra K S
R : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R K
inst✝⁴ : IsScalarTower R K S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B✝ : PowerBasis S A
hB✝ : IsIntegral R B✝.gen
B B' : PowerBasis K S
P : R[X]
h : ↑(aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i✝ : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
n : ℕ
x✝ : n ∈ Finset.range (natDegree P + 1)
⊢ IsIntegral R (↑(coeff P n • ↑B.basis.repr (B.gen ^ n)) i)
[PROOFSTEP]
exact isIntegral_smul _ (repr_gen_pow_isIntegral hB hmin _ _)