[GOAL]
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
f : F[X]
hf✝ : HasSeparableContraction q f
g : F[X]
hf : IsSeparableContraction q f g
⊢ ∃ m, natDegree g * q ^ m = natDegree f
[PROOFSTEP]
obtain ⟨m, rfl⟩ := hf.2
[GOAL]
case intro
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf✝ : HasSeparableContraction q (↑(expand F (q ^ m)) g)
hf : IsSeparableContraction q (↑(expand F (q ^ m)) g) g
⊢ ∃ m_1, natDegree g * q ^ m_1 = natDegree (↑(expand F (q ^ m)) g)
[PROOFSTEP]
use m
[GOAL]
case h
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf✝ : HasSeparableContraction q (↑(expand F (q ^ m)) g)
hf : IsSeparableContraction q (↑(expand F (q ^ m)) g) g
⊢ natDegree g * q ^ m = natDegree (↑(expand F (q ^ m)) g)
[PROOFSTEP]
rw [natDegree_expand]
[GOAL]
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
f✝ : F[X]
hf✝ : HasSeparableContraction q f✝
f : F[X]
hf : HasSeparableContraction 1 f
⊢ degree hf = natDegree f
[PROOFSTEP]
let ⟨a, ha⟩ := hf.dvd_degree'
[GOAL]
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
f✝ : F[X]
hf✝ : HasSeparableContraction q f✝
f : F[X]
hf : HasSeparableContraction 1 f
a : ℕ
ha : degree hf * 1 ^ a = natDegree f
⊢ degree hf = natDegree f
[PROOFSTEP]
rw [← ha, one_pow a, mul_one]
[GOAL]
F : Type u_1
inst✝ : Field F
q✝ : ℕ
f✝ : F[X]
hf : HasSeparableContraction q✝ f✝
q : ℕ
hF : ExpChar F q
f : F[X]
irred : Irreducible f
⊢ HasSeparableContraction q f
[PROOFSTEP]
cases hF
[GOAL]
case zero
F : Type u_1
inst✝¹ : Field F
q : ℕ
f✝ : F[X]
hf : HasSeparableContraction q f✝
f : F[X]
irred : Irreducible f
inst✝ : CharZero F
⊢ HasSeparableContraction 1 f
[PROOFSTEP]
exact ⟨f, irred.separable, ⟨0, by rw [pow_zero, expand_one]⟩⟩
[GOAL]
F : Type u_1
inst✝¹ : Field F
q : ℕ
f✝ : F[X]
hf : HasSeparableContraction q f✝
f : F[X]
irred : Irreducible f
inst✝ : CharZero F
⊢ ↑(expand F (1 ^ 0)) f = f
[PROOFSTEP]
rw [pow_zero, expand_one]
[GOAL]
case prime
F : Type u_1
inst✝ : Field F
q✝ : ℕ
f✝ : F[X]
hf : HasSeparableContraction q✝ f✝
q : ℕ
f : F[X]
irred : Irreducible f
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
⊢ HasSeparableContraction q f
[PROOFSTEP]
rcases exists_separable_of_irreducible q irred ‹q.Prime›.ne_zero with ⟨n, g, hgs, hge⟩
[GOAL]
case prime.intro.intro.intro
F : Type u_1
inst✝ : Field F
q✝ : ℕ
f✝ : F[X]
hf : HasSeparableContraction q✝ f✝
q : ℕ
f : F[X]
irred : Irreducible f
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
n : ℕ
g : F[X]
hgs : Separable g
hge : ↑(expand F (q ^ n)) g = f
⊢ HasSeparableContraction q f
[PROOFSTEP]
exact ⟨g, hgs, n, hge⟩
[GOAL]
F : Type u_1
inst✝¹ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m m' : ℕ
h_expand : ↑(expand F (q ^ m)) g = ↑(expand F (q ^ m')) g'
hg : Separable g
hg' : Separable g'
⊢ natDegree g = natDegree g'
[PROOFSTEP]
wlog hm : m ≤ m'
[GOAL]
case inr
F : Type u_1
inst✝¹ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m m' : ℕ
h_expand : ↑(expand F (q ^ m)) g = ↑(expand F (q ^ m')) g'
hg : Separable g
hg' : Separable g'
this :
  ∀ {F : Type u_1} [inst : Field F] (q : ℕ) {f : F[X]},
    HasSeparableContraction q f →
      ∀ [hq : NeZero q] [inst_1 : CharP F q] (g g' : F[X]) (m m' : ℕ),
        ↑(expand F (q ^ m)) g = ↑(expand F (q ^ m')) g' →
          Separable g → Separable g' → m ≤ m' → natDegree g = natDegree g'
hm : ¬m ≤ m'
⊢ natDegree g = natDegree g'
[PROOFSTEP]
exact (this q hf g' g m' m h_expand.symm hg' hg (le_of_not_le hm)).symm
[GOAL]
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m m' : ℕ
h_expand : ↑(expand F (q ^ m)) g = ↑(expand F (q ^ m')) g'
hg : Separable g
hg' : Separable g'
hm : m ≤ m'
⊢ natDegree g = natDegree g'
[PROOFSTEP]
obtain ⟨s, rfl⟩ := exists_add_of_le hm
[GOAL]
case intro
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m : ℕ
hg : Separable g
hg' : Separable g'
s : ℕ
h_expand : ↑(expand F (q ^ m)) g = ↑(expand F (q ^ (m + s))) g'
hm : m ≤ m + s
⊢ natDegree g = natDegree g'
[PROOFSTEP]
rw [pow_add, expand_mul, expand_inj (pow_pos (NeZero.pos q) m)] at h_expand
[GOAL]
case intro
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m : ℕ
hg : Separable g
hg' : Separable g'
s : ℕ
h_expand : g = ↑(expand F (q ^ s)) g'
hm : m ≤ m + s
⊢ natDegree g = natDegree g'
[PROOFSTEP]
subst h_expand
[GOAL]
case intro
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : Separable g'
s : ℕ
hm : m ≤ m + s
hg : Separable (↑(expand F (q ^ s)) g')
⊢ natDegree (↑(expand F (q ^ s)) g') = natDegree g'
[PROOFSTEP]
rcases isUnit_or_eq_zero_of_separable_expand q s (NeZero.pos q) hg with (h | rfl)
[GOAL]
case intro.inl
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : Separable g'
s : ℕ
hm : m ≤ m + s
hg : Separable (↑(expand F (q ^ s)) g')
h : IsUnit g'
⊢ natDegree (↑(expand F (q ^ s)) g') = natDegree g'
[PROOFSTEP]
rw [natDegree_expand, natDegree_eq_zero_of_isUnit h, zero_mul]
[GOAL]
case intro.inr
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hq : NeZero q
inst✝ : CharP F q
g' : F[X]
m : ℕ
hg' : Separable g'
hm : m ≤ m + 0
hg : Separable (↑(expand F (q ^ 0)) g')
⊢ natDegree (↑(expand F (q ^ 0)) g') = natDegree g'
[PROOFSTEP]
rw [natDegree_expand, pow_zero, mul_one]
[GOAL]
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hF : ExpChar F q
g : F[X]
hg : IsSeparableContraction q f g
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
cases hF
[GOAL]
case zero
F : Type u_1
inst✝¹ : Field F
f g : F[X]
inst✝ : CharZero F
hf : HasSeparableContraction 1 f
hg : IsSeparableContraction 1 f g
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
rcases hg with ⟨_, m, hm⟩
[GOAL]
case zero.intro.intro
F : Type u_1
inst✝¹ : Field F
f g : F[X]
inst✝ : CharZero F
hf : HasSeparableContraction 1 f
left✝ : Separable g
m : ℕ
hm : ↑(expand F (1 ^ m)) g = f
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
rw [one_pow, expand_one] at hm
[GOAL]
case zero.intro.intro
F : Type u_1
inst✝¹ : Field F
f g : F[X]
inst✝ : CharZero F
hf : HasSeparableContraction 1 f
left✝ : Separable g
m : ℕ
hm : g = f
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
rw [hf.eq_degree, hm]
[GOAL]
case prime
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hg : IsSeparableContraction q f g
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
rcases hg with ⟨hg, m, hm⟩
[GOAL]
case prime.intro.intro
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
let g' := Classical.choose hf
[GOAL]
case prime.intro.intro
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
cases' (Classical.choose_spec hf).2 with m' hm'
[GOAL]
case prime.intro.intro.intro
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
haveI : Fact q.Prime := ⟨by assumption⟩
[GOAL]
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
⊢ Nat.Prime q
[PROOFSTEP]
assumption
[GOAL]
case prime.intro.intro.intro
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
this : Fact (Nat.Prime q)
⊢ natDegree g = HasSeparableContraction.degree hf
[PROOFSTEP]
apply contraction_degree_eq_or_insep q g g' m m'
[GOAL]
case prime.intro.intro.intro.h_expand
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
this : Fact (Nat.Prime q)
⊢ ↑(expand F (q ^ m)) g = ↑(expand F (q ^ m')) g'
case prime.intro.intro.intro.hg
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
this : Fact (Nat.Prime q)
⊢ Separable g
case prime.intro.intro.intro.hg'
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
this : Fact (Nat.Prime q)
⊢ Separable g'
[PROOFSTEP]
rw [hm, hm']
[GOAL]
case prime.intro.intro.intro.hg
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
this : Fact (Nat.Prime q)
⊢ Separable g
case prime.intro.intro.intro.hg'
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
this : Fact (Nat.Prime q)
⊢ Separable g'
[PROOFSTEP]
exact hg
[GOAL]
case prime.intro.intro.intro.hg'
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : Separable g
m : ℕ
hm : ↑(expand F (q ^ m)) g = f
g' : F[X] := choose hf
m' : ℕ
hm' : ↑(expand F (q ^ m')) (choose hf) = f
this : Fact (Nat.Prime q)
⊢ Separable g'
[PROOFSTEP]
exact (Classical.choose_spec hf).1


[GOAL]
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
⊢ Function.Injective ↑(RingHom.comp (Ideal.Quotient.mk I) C)
[PROOFSTEP]
refine' (injective_iff_map_eq_zero _).2 fun x hx => _
[GOAL]
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : ↑(RingHom.comp (Ideal.Quotient.mk I) C) x = 0
⊢ x = 0
[PROOFSTEP]
rw [RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem] at hx
[GOAL]
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : ↑C x ∈ I
⊢ x = 0
[PROOFSTEP]
refine' _root_.by_contradiction fun hx0 => absurd (I.eq_top_iff_one.2 _) hI
[GOAL]
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : ↑C x ∈ I
hx0 : ¬x = 0
⊢ 1 ∈ I
[PROOFSTEP]
have := I.mul_mem_left (MvPolynomial.C x⁻¹) hx
[GOAL]
σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
x : K
hx : ↑C x ∈ I
hx0 : ¬x = 0
this : ↑C x⁻¹ * ↑C x ∈ I
⊢ 1 ∈ I
[PROOFSTEP]
rwa [← MvPolynomial.C.map_mul, inv_mul_cancel hx0, MvPolynomial.C_1] at this
[GOAL]
σ K : Type u
inst✝ : Field K
⊢ Module.rank K (MvPolynomial σ K) = Cardinal.mk (σ →₀ ℕ)
[PROOFSTEP]
rw [← Cardinal.lift_inj, ← (basisMonomials σ K).mk_eq_rank]


[GOAL]
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
⊢ Surjective fun v i => ↑(MvPolynomial.eval v) (ps i)
[PROOFSTEP]
have is_int : ∀ x : R, IsIntegral K x := fun x => isAlgebraic_iff_isIntegral.1 (alg x)
[GOAL]
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
⊢ Surjective fun v i => ↑(MvPolynomial.eval v) (ps i)
[PROOFSTEP]
classical
intro v
cases nonempty_fintype ι
let s : Finset R :=
  (Finset.biUnion (univ : Finset ι) fun i => (ps i).support.image fun x => coeff x (ps i)) ∪ (univ : Finset ι).image v
have hv : ∀ i, v i ∈ Algebra.adjoin K (s : Set R) := fun j =>
  Algebra.subset_adjoin (mem_union_right _ (mem_image.2 ⟨j, mem_univ _, rfl⟩))
have hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ (ps i).support → coeff k (ps i) ∈ Algebra.adjoin K (s : Set R) := fun i k hk =>
  Algebra.subset_adjoin (mem_union_left _ (mem_biUnion.2 ⟨i, mem_univ _, mem_image_of_mem _ hk⟩))
letI := isNoetherian_adjoin_finset s fun x _ => is_int x
letI := Module.IsNoetherian.finite K (Algebra.adjoin K (s : Set R))
letI : Finite (Algebra.adjoin K (s : Set R)) :=
  FiniteDimensional.finite_of_finite K
    (Algebra.adjoin K (s : Set R))
      -- The restriction of the polynomial map, `ps`, to the subalgebra generated by `s`
let res : (ι → Algebra.adjoin K (s : Set R)) → ι → Algebra.adjoin K (s : Set R) := fun x i =>
  ⟨eval (fun j : ι => (x j : R)) (ps i), eval_mem (hs₁ _) fun i => (x i).2⟩
have hres_inj : Injective res := by
  intro x y hxy
  ext i
  simp only [Subtype.ext_iff, funext_iff] at hxy
  exact congr_fun (hinj (funext hxy)) i
have hres_surj : Surjective res := Finite.injective_iff_surjective.1 hres_inj
cases' hres_surj fun i => ⟨v i, hv i⟩ with w hw
use fun i => w i
simpa only [Subtype.ext_iff, funext_iff] using hw
[GOAL]
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
⊢ Surjective fun v i => ↑(MvPolynomial.eval v) (ps i)
[PROOFSTEP]
intro v
[GOAL]
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
let s : Finset R :=
  (Finset.biUnion (univ : Finset ι) fun i => (ps i).support.image fun x => coeff x (ps i)) ∪ (univ : Finset ι).image v
[GOAL]
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
have hv : ∀ i, v i ∈ Algebra.adjoin K (s : Set R) := fun j =>
  Algebra.subset_adjoin (mem_union_right _ (mem_image.2 ⟨j, mem_univ _, rfl⟩))
[GOAL]
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
have hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ (ps i).support → coeff k (ps i) ∈ Algebra.adjoin K (s : Set R) := fun i k hk =>
  Algebra.subset_adjoin (mem_union_left _ (mem_biUnion.2 ⟨i, mem_univ _, mem_image_of_mem _ hk⟩))
[GOAL]
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
letI := isNoetherian_adjoin_finset s fun x _ => is_int x
[GOAL]
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
letI := Module.IsNoetherian.finite K (Algebra.adjoin K (s : Set R))
[GOAL]
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } := Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
letI : Finite (Algebra.adjoin K (s : Set R)) :=
  FiniteDimensional.finite_of_finite K
    (Algebra.adjoin K (s : Set R))
      -- The restriction of the polynomial map, `ps`, to the subalgebra generated by `s`
[GOAL]
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
let res : (ι → Algebra.adjoin K (s : Set R)) → ι → Algebra.adjoin K (s : Set R) := fun x i =>
  ⟨eval (fun j : ι => (x j : R)) (ps i), eval_mem (hs₁ _) fun i => (x i).2⟩
[GOAL]
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
have hres_inj : Injective res := by
  intro x y hxy
  ext i
  simp only [Subtype.ext_iff, funext_iff] at hxy
  exact congr_fun (hinj (funext hxy)) i
[GOAL]
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
⊢ Injective res
[PROOFSTEP]
intro x y hxy
[GOAL]
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
x y : ι → { x // x ∈ Algebra.adjoin K ↑s }
hxy : res x = res y
⊢ x = y
[PROOFSTEP]
ext i
[GOAL]
case h.a
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
x y : ι → { x // x ∈ Algebra.adjoin K ↑s }
hxy : res x = res y
i : ι
⊢ ↑(x i) = ↑(y i)
[PROOFSTEP]
simp only [Subtype.ext_iff, funext_iff] at hxy
[GOAL]
case h.a
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
x y : ι → { x // x ∈ Algebra.adjoin K ↑s }
i : ι
hxy : ∀ (a : ι), ↑(MvPolynomial.eval fun j => ↑(x j)) (ps a) = ↑(MvPolynomial.eval fun j => ↑(y j)) (ps a)
⊢ ↑(x i) = ↑(y i)
[PROOFSTEP]
exact congr_fun (hinj (funext hxy)) i
[GOAL]
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
hres_inj : Injective res
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
have hres_surj : Surjective res := Finite.injective_iff_surjective.1 hres_inj
[GOAL]
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
hres_inj : Injective res
hres_surj : Surjective res
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
cases' hres_surj fun i => ⟨v i, hv i⟩ with w hw
[GOAL]
case intro.intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
hres_inj : Injective res
hres_surj : Surjective res
w : ι → { x // x ∈ Algebra.adjoin K ↑s }
hw : res w = fun i => { val := v i, property := (_ : v i ∈ Algebra.adjoin K ↑s) }
⊢ ∃ a, (fun v i => ↑(MvPolynomial.eval v) (ps i)) a = v
[PROOFSTEP]
use fun i => w i
[GOAL]
case h
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
hinj : Injective fun v i => ↑(MvPolynomial.eval v) (ps i)
is_int : ∀ (x : R), IsIntegral K x
v : (i : ι) → (fun x => R) (ps i)
val✝ : Fintype ι
s : Finset R :=
  (Finset.biUnion univ fun i => image (fun x => coeff x (ps i)) (MvPolynomial.support (ps i))) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ MvPolynomial.support (ps i) → coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝¹ : IsNoetherian K { x // x ∈ Algebra.adjoin K ↑s } := isNoetherian_adjoin_finset s fun x x_1 => is_int x
this✝ : Module.Finite K { x // x ∈ Algebra.adjoin K ↑s } :=
  Module.IsNoetherian.finite K { x // x ∈ Algebra.adjoin K ↑s }
this : Finite { x // x ∈ Algebra.adjoin K ↑s } := FiniteDimensional.finite_of_finite K { x // x ∈ Algebra.adjoin K ↑s }
res : (ι → { x // x ∈ Algebra.adjoin K ↑s }) → ι → { x // x ∈ Algebra.adjoin K ↑s } :=
  fun x i =>
    { val := ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i),
      property := (_ : ↑(MvPolynomial.eval fun j => ↑(x j)) (ps i) ∈ Algebra.adjoin K ↑s) }
hres_inj : Injective res
hres_surj : Surjective res
w : ι → { x // x ∈ Algebra.adjoin K ↑s }
hw : res w = fun i => { val := v i, property := (_ : v i ∈ Algebra.adjoin K ↑s) }
⊢ ((fun v i => ↑(MvPolynomial.eval v) (ps i)) fun i => ↑(w i)) = v
[PROOFSTEP]
simpa only [Subtype.ext_iff, funext_iff] using hw


[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
⊢ restrictScalars F (normalClosure F K L) = ⨆ (x : K), adjoin F (rootSet (minpoly F x) L)
[PROOFSTEP]
classical
have hi : ∀ x : K, IsIntegral F x := fun x ↦ (isIntegral_algebraMap_iff (algebraMap K L).injective).mp (h.isIntegral _)
refine' le_antisymm (iSup_le _) (iSup_le fun x => adjoin_le_iff.mpr fun y hy => _)
· rintro f _ ⟨x, rfl⟩
  refine' le_iSup (fun x => adjoin F ((minpoly F x).rootSet L)) x (subset_adjoin F ((minpoly F x).rootSet L) _)
  rw [mem_rootSet_of_ne (minpoly.ne_zero (hi x)), AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom,
    Polynomial.aeval_algHom_apply, minpoly.aeval, map_zero]
· rw [Polynomial.rootSet, Finset.mem_coe, Multiset.mem_toFinset] at hy
  let g := (algHomAdjoinIntegralEquiv F (hi x)).symm ⟨y, hy⟩
  refine'
    le_iSup (fun f : K →ₐ[F] L => f.fieldRange) ((g.liftNormal L).comp (toAlgHom F K L))
      ⟨x, (g.liftNormal_commutes L (AdjoinSimple.gen F x)).trans _⟩
  rw [Algebra.id.map_eq_id, RingHom.id_apply]
    -- Porting note: in mathlib3 this next `apply` closed the goal.
        -- Now it can't find a proof by unification, so we have to do it ourselves.
  apply PowerBasis.lift_gen
  change aeval y (minpoly F (AdjoinSimple.gen F x)) = 0
  exact minpoly_gen (hi x) ▸ aeval_eq_zero_of_mem_rootSet (Multiset.mem_toFinset.mpr hy)
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
⊢ restrictScalars F (normalClosure F K L) = ⨆ (x : K), adjoin F (rootSet (minpoly F x) L)
[PROOFSTEP]
have hi : ∀ x : K, IsIntegral F x := fun x ↦ (isIntegral_algebraMap_iff (algebraMap K L).injective).mp (h.isIntegral _)
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
⊢ restrictScalars F (normalClosure F K L) = ⨆ (x : K), adjoin F (rootSet (minpoly F x) L)
[PROOFSTEP]
refine' le_antisymm (iSup_le _) (iSup_le fun x => adjoin_le_iff.mpr fun y hy => _)
[GOAL]
case refine'_1
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
⊢ ∀ (i : K →ₐ[F] L), AlgHom.fieldRange i ≤ ⨆ (x : K), adjoin F (rootSet (minpoly F x) L)
[PROOFSTEP]
rintro f _ ⟨x, rfl⟩
[GOAL]
case refine'_1.intro
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
f : K →ₐ[F] L
x : K
⊢ ↑↑f x ∈ ⨆ (x : K), adjoin F (rootSet (minpoly F x) L)
[PROOFSTEP]
refine' le_iSup (fun x => adjoin F ((minpoly F x).rootSet L)) x (subset_adjoin F ((minpoly F x).rootSet L) _)
[GOAL]
case refine'_1.intro
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
f : K →ₐ[F] L
x : K
⊢ ↑↑f x ∈ rootSet (minpoly F x) L
[PROOFSTEP]
rw [mem_rootSet_of_ne (minpoly.ne_zero (hi x)), AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom,
  Polynomial.aeval_algHom_apply, minpoly.aeval, map_zero]
[GOAL]
case refine'_2
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
x : K
y : L
hy : y ∈ rootSet (minpoly F x) L
⊢ y ∈ ↑(restrictScalars F (normalClosure F K L))
[PROOFSTEP]
rw [Polynomial.rootSet, Finset.mem_coe, Multiset.mem_toFinset] at hy
[GOAL]
case refine'_2
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
x : K
y : L
hy : y ∈ roots (Polynomial.map (algebraMap F L) (minpoly F x))
⊢ y ∈ ↑(restrictScalars F (normalClosure F K L))
[PROOFSTEP]
let g := (algHomAdjoinIntegralEquiv F (hi x)).symm ⟨y, hy⟩
[GOAL]
case refine'_2
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
x : K
y : L
hy : y ∈ roots (Polynomial.map (algebraMap F L) (minpoly F x))
g : (fun x_1 => { x_2 // x_2 ∈ F⟮x⟯ } →ₐ[F] L) { val := y, property := hy } :=
  ↑(algHomAdjoinIntegralEquiv F (_ : IsIntegral F x)).symm { val := y, property := hy }
⊢ y ∈ ↑(restrictScalars F (normalClosure F K L))
[PROOFSTEP]
refine'
  le_iSup (fun f : K →ₐ[F] L => f.fieldRange) ((g.liftNormal L).comp (toAlgHom F K L))
    ⟨x, (g.liftNormal_commutes L (AdjoinSimple.gen F x)).trans _⟩
[GOAL]
case refine'_2
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
x : K
y : L
hy : y ∈ roots (Polynomial.map (algebraMap F L) (minpoly F x))
g : (fun x_1 => { x_2 // x_2 ∈ F⟮x⟯ } →ₐ[F] L) { val := y, property := hy } :=
  ↑(algHomAdjoinIntegralEquiv F (_ : IsIntegral F x)).symm { val := y, property := hy }
⊢ ↑(algebraMap L L) (↑g (AdjoinSimple.gen F x)) = y
[PROOFSTEP]
rw [Algebra.id.map_eq_id, RingHom.id_apply]
  -- Porting note: in mathlib3 this next `apply` closed the goal.
      -- Now it can't find a proof by unification, so we have to do it ourselves.
[GOAL]
case refine'_2
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
x : K
y : L
hy : y ∈ roots (Polynomial.map (algebraMap F L) (minpoly F x))
g : (fun x_1 => { x_2 // x_2 ∈ F⟮x⟯ } →ₐ[F] L) { val := y, property := hy } :=
  ↑(algHomAdjoinIntegralEquiv F (_ : IsIntegral F x)).symm { val := y, property := hy }
⊢ ↑g (AdjoinSimple.gen F x) = y
[PROOFSTEP]
apply PowerBasis.lift_gen
[GOAL]
case refine'_2.hy
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
x : K
y : L
hy : y ∈ roots (Polynomial.map (algebraMap F L) (minpoly F x))
g : (fun x_1 => { x_2 // x_2 ∈ F⟮x⟯ } →ₐ[F] L) { val := y, property := hy } :=
  ↑(algHomAdjoinIntegralEquiv F (_ : IsIntegral F x)).symm { val := y, property := hy }
⊢ ↑(aeval
          ↑(↑(Equiv.subtypeEquiv (Equiv.refl L)
                    (_ :
                      ∀ (x_1 : L),
                        ↑(aeval x_1) (minpoly F (adjoin.powerBasis (_ : IsIntegral F x)).gen) = 0 ↔
                          ↑(Equiv.refl L) x_1 ∈
                            roots
                              (Polynomial.map (algebraMap F L)
                                (minpoly F (adjoin.powerBasis (_ : IsIntegral F x)).gen)))).symm
              (↑(Equiv.subtypeEquiv (Equiv.refl L)
                      (_ :
                        ∀ (x_1 : L),
                          x_1 ∈
                              roots
                                (Polynomial.map (algebraMap F L)
                                  (minpoly F (adjoin.powerBasis (_ : IsIntegral F x)).gen)) ↔
                            ↑(Equiv.refl L) x_1 ∈ roots (Polynomial.map (algebraMap F L) (minpoly F x)))).symm
                { val := y, property := hy })))
      (minpoly F (adjoin.powerBasis (_ : IsIntegral F x)).gen) =
    0
[PROOFSTEP]
change aeval y (minpoly F (AdjoinSimple.gen F x)) = 0
[GOAL]
case refine'_2.hy
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
x : K
y : L
hy : y ∈ roots (Polynomial.map (algebraMap F L) (minpoly F x))
g : (fun x_1 => { x_2 // x_2 ∈ F⟮x⟯ } →ₐ[F] L) { val := y, property := hy } :=
  ↑(algHomAdjoinIntegralEquiv F (_ : IsIntegral F x)).symm { val := y, property := hy }
⊢ ↑(aeval y) (minpoly F (AdjoinSimple.gen F x)) = 0
[PROOFSTEP]
exact minpoly_gen (hi x) ▸ aeval_eq_zero_of_mem_rootSet (Multiset.mem_toFinset.mpr hy)
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
⊢ Normal F { x // x ∈ normalClosure F K L }
[PROOFSTEP]
let ϕ := algebraMap K L
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
ϕ : K →+* L := algebraMap K L
⊢ Normal F { x // x ∈ normalClosure F K L }
[PROOFSTEP]
rw [← IntermediateField.restrictScalars_normal, restrictScalars_eq_iSup_adjoin]
  -- Porting note: use the `(_)` trick to obtain an instance by unification.
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
ϕ : K →+* L := algebraMap K L
⊢ Normal F { x // x ∈ ⨆ (x : K), adjoin F (rootSet (minpoly F x) L) }
[PROOFSTEP]
apply IntermediateField.normal_iSup (h := _)
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
ϕ : K →+* L := algebraMap K L
⊢ ∀ (i : K), Normal F { x // x ∈ adjoin F (rootSet (minpoly F i) L) }
[PROOFSTEP]
intro x
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
ϕ : K →+* L := algebraMap K L
x : K
⊢ Normal F { x_1 // x_1 ∈ adjoin F (rootSet (minpoly F x) L) }
[PROOFSTEP]
apply Normal.of_isSplittingField (p := minpoly F x) (hFEp := _)
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
ϕ : K →+* L := algebraMap K L
x : K
⊢ IsSplittingField F { x_1 // x_1 ∈ adjoin F (rootSet (minpoly F x) L) } (minpoly F x)
[PROOFSTEP]
exact
  adjoin_rootSet_isSplittingField
    ((minpoly.eq_of_algebraMap_eq ϕ.injective ((isIntegral_algebraMap_iff ϕ.injective).mp (h.isIntegral (ϕ x)))
          rfl).symm ▸
      h.splits _)
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower F K L
inst✝ : FiniteDimensional F K
⊢ FiniteDimensional F { x // x ∈ normalClosure F K L }
[PROOFSTEP]
haveI : ∀ f : K →ₐ[F] L, FiniteDimensional F f.fieldRange := fun f => f.toLinearMap.finiteDimensional_range
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower F K L
inst✝ : FiniteDimensional F K
this : ∀ (f : K →ₐ[F] L), FiniteDimensional F { x // x ∈ AlgHom.fieldRange f }
⊢ FiniteDimensional F { x // x ∈ normalClosure F K L }
[PROOFSTEP]
apply IntermediateField.finiteDimensional_iSup_of_finite


[GOAL]
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
⊢ ⁅x, x⁆ = 0
[PROOFSTEP]
simp only [bracket_def]
[GOAL]
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) x = 0
[PROOFSTEP]
refine' x.induction_on _ _ _
[GOAL]
case refine'_1
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) 0) 0 = 0
[PROOFSTEP]
simp only [LinearMap.map_zero, eq_self_iff_true, LinearMap.zero_apply]
[GOAL]
case refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
⊢ ∀ (x : A) (y : L), ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x ⊗ₜ[R] y)) (x ⊗ₜ[R] y) = 0
[PROOFSTEP]
intro a l
[GOAL]
case refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
a : A
l : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a ⊗ₜ[R] l)) (a ⊗ₜ[R] l) = 0
[PROOFSTEP]
simp only [bracket'_tmul, TensorProduct.tmul_zero, eq_self_iff_true, lie_self]
[GOAL]
case refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
⊢ ∀ (x y : A ⊗[R] L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) x = 0 →
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) y = 0 →
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x + y)) (x + y) = 0
[PROOFSTEP]
intro z₁ z₂ h₁ h₂
[GOAL]
case refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (z₁ + z₂)) (z₁ + z₂) = 0
[PROOFSTEP]
suffices bracket' R A L z₁ z₂ + bracket' R A L z₂ z₁ = 0 by
  rw [LinearMap.map_add, LinearMap.map_add, LinearMap.add_apply, LinearMap.add_apply, h₁, h₂, zero_add, add_zero,
    add_comm, this]
[GOAL]
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
this : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₂ + ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₁ = 0
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (z₁ + z₂)) (z₁ + z₂) = 0
[PROOFSTEP]
rw [LinearMap.map_add, LinearMap.map_add, LinearMap.add_apply, LinearMap.add_apply, h₁, h₂, zero_add, add_zero,
  add_comm, this]
[GOAL]
case refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₂ + ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₁ = 0
[PROOFSTEP]
refine' z₁.induction_on _ _ _
[GOAL]
case refine'_3.refine'_1
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) 0) z₂ + ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) 0 = 0
[PROOFSTEP]
simp only [LinearMap.map_zero, add_zero, LinearMap.zero_apply]
[GOAL]
case refine'_3.refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
⊢ ∀ (x : A) (y : L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x ⊗ₜ[R] y)) z₂ +
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) (x ⊗ₜ[R] y) =
      0
[PROOFSTEP]
intro a₁ l₁
[GOAL]
case refine'_3.refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z₂ +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) (a₁ ⊗ₜ[R] l₁) =
    0
[PROOFSTEP]
refine' z₂.induction_on _ _ _
[GOAL]
case refine'_3.refine'_2.refine'_1
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) 0 +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) 0) (a₁ ⊗ₜ[R] l₁) =
    0
[PROOFSTEP]
simp only [LinearMap.map_zero, add_zero, LinearMap.zero_apply]
[GOAL]
case refine'_3.refine'_2.refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ∀ (x : A) (y : L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y) +
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x ⊗ₜ[R] y)) (a₁ ⊗ₜ[R] l₁) =
      0
[PROOFSTEP]
intro a₂ l₂
[GOAL]
case refine'_3.refine'_2.refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂) +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) (a₁ ⊗ₜ[R] l₁) =
    0
[PROOFSTEP]
simp only [← lie_skew l₂ l₁, mul_comm a₁ a₂, TensorProduct.tmul_neg, bracket'_tmul, add_right_neg]
[GOAL]
case refine'_3.refine'_2.refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) x +
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) (a₁ ⊗ₜ[R] l₁) =
        0 →
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) y +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (a₁ ⊗ₜ[R] l₁) =
          0 →
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (x + y) +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x + y)) (a₁ ⊗ₜ[R] l₁) =
          0
[PROOFSTEP]
intro y₁ y₂ hy₁ hy₂
[GOAL]
case refine'_3.refine'_2.refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
a₁ : A
l₁ : L
y₁ y₂ : A ⊗[R] L
hy₁ :
  ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) y₁ +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y₁) (a₁ ⊗ₜ[R] l₁) =
    0
hy₂ :
  ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) y₂ +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y₂) (a₁ ⊗ₜ[R] l₁) =
    0
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (y₁ + y₂) +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (y₁ + y₂)) (a₁ ⊗ₜ[R] l₁) =
    0
[PROOFSTEP]
simp only [hy₁, hy₂, add_add_add_comm, add_zero, LinearMap.add_apply, LinearMap.map_add]
[GOAL]
case refine'_3.refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
⊢ ∀ (x y : A ⊗[R] L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) z₂ + ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) x = 0 →
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z₂ + ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) y = 0 →
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x + y)) z₂ +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) (x + y) =
          0
[PROOFSTEP]
intro y₁ y₂ hy₁ hy₂
[GOAL]
case refine'_3.refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₁) z₁ = 0
h₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) z₂ = 0
y₁ y₂ : A ⊗[R] L
hy₁ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y₁) z₂ + ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) y₁ = 0
hy₂ : ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y₂) z₂ + ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) y₂ = 0
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (y₁ + y₂)) z₂ +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) z₂) (y₁ + y₂) =
    0
[PROOFSTEP]
simp only [add_add_add_comm, hy₁, hy₂, add_zero, LinearMap.add_apply, LinearMap.map_add]
[GOAL]
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
⊢ ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆
[PROOFSTEP]
simp only [bracket_def]
[GOAL]
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) y)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) z)
[PROOFSTEP]
refine' x.induction_on _ _ _
[GOAL]
case refine'_1
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) 0) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) 0) y)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) 0) z)
[PROOFSTEP]
simp only [LinearMap.map_zero, add_zero, LinearMap.zero_apply]
[GOAL]
case refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
⊢ ∀ (x : A) (y_1 : L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x ⊗ₜ[R] y_1)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x ⊗ₜ[R] y_1)) y)) z +
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x ⊗ₜ[R] y_1)) z)
[PROOFSTEP]
intro a₁ l₁
[GOAL]
case refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
a₁ : A
l₁ : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) y)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z)
[PROOFSTEP]
refine' y.induction_on _ _ _
[GOAL]
case refine'_2.refine'_1
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
a₁ : A
l₁ : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) 0) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) 0)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) 0) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z)
[PROOFSTEP]
simp only [LinearMap.map_zero, add_zero, LinearMap.zero_apply]
[GOAL]
case refine'_2.refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
a₁ : A
l₁ : L
⊢ ∀ (x : A) (y : L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x ⊗ₜ[R] y)) z) =
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
              (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y)))
          z +
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x ⊗ₜ[R] y))
          (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z)
[PROOFSTEP]
intro a₂ l₂
[GOAL]
case refine'_2.refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
      (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
        z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z)
[PROOFSTEP]
refine' z.induction_on _ _ _
[GOAL]
case refine'_2.refine'_2.refine'_1
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
      (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) 0) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
        0 +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) 0)
[PROOFSTEP]
rw [LinearMap.map_zero, LinearMap.map_zero, LinearMap.map_zero, LinearMap.map_zero, add_zero]
[GOAL]
case refine'_2.refine'_2.refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ∀ (x : A) (y : L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) (x ⊗ₜ[R] y)) =
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
              (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
          (x ⊗ₜ[R] y) +
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
          (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y))
[PROOFSTEP]
intro a₃ l₃
[GOAL]
case refine'_2.refine'_2.refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
a₁ : A
l₁ : L
a₂ : A
l₂ : L
a₃ : A
l₃ : L
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
      (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) (a₃ ⊗ₜ[R] l₃)) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
        (a₃ ⊗ₜ[R] l₃) +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₃ ⊗ₜ[R] l₃))
[PROOFSTEP]
simp only [bracket'_tmul]
[GOAL]
case refine'_2.refine'_2.refine'_2
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
a₁ : A
l₁ : L
a₂ : A
l₂ : L
a₃ : A
l₃ : L
⊢ (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₁, ⁅l₂, l₃⁆⁆ = (a₁ * a₂ * a₃) ⊗ₜ[R] ⁅⁅l₁, l₂⁆, l₃⁆ + (a₂ * (a₁ * a₃)) ⊗ₜ[R] ⁅l₂, ⁅l₁, l₃⁆⁆
[PROOFSTEP]
rw [mul_left_comm a₂ a₁ a₃, mul_assoc, leibniz_lie, TensorProduct.tmul_add]
[GOAL]
case refine'_2.refine'_2.refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ∀ (x y : A ⊗[R] L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
          (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) x) =
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
                (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
            x +
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) x) →
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) y) =
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
                  (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
              y +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
              (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) y) →
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) (x + y)) =
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
                  (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
              (x + y) +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
              (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (x + y))
[PROOFSTEP]
intro u₁ u₂ h₁ h₂
[GOAL]
case refine'_2.refine'_2.refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
a₁ : A
l₁ : L
a₂ : A
l₂ : L
u₁ u₂ : A ⊗[R] L
h₁ :
  ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
      (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) u₁) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
        u₁ +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) u₁)
h₂ :
  ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
      (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) u₂) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
        u₂ +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) u₂)
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
      (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂)) (u₁ + u₂)) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
        (u₁ + u₂) +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₂ ⊗ₜ[R] l₂))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (u₁ + u₂))
[PROOFSTEP]
rw [map_add, map_add, map_add, map_add, map_add, h₁, h₂, add_add_add_comm]
[GOAL]
case refine'_2.refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) z) =
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) x))
            z +
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x)
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z) →
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) y))
              z +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y)
              (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z) →
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x + y)) z) =
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
                  (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (x + y)))
              z +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x + y))
              (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z)
[PROOFSTEP]
intro u₁ u₂ h₁ h₂
[GOAL]
case refine'_2.refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
a₁ : A
l₁ : L
u₁ u₂ : A ⊗[R] L
h₁ :
  ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₁) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) u₁)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₁) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z)
h₂ :
  ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₂) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) u₂)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₂) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z)
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁))
      (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (u₁ + u₂)) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L)
            (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) (u₁ + u₂)))
        z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (u₁ + u₂))
        (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (a₁ ⊗ₜ[R] l₁)) z)
[PROOFSTEP]
rw [map_add, LinearMap.add_apply, LinearMap.add_apply, map_add, map_add, map_add, LinearMap.add_apply, h₁, h₂,
  add_add_add_comm]
[GOAL]
case refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
⊢ ∀ (x y_1 : A ⊗[R] L),
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) y)) z +
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) x) z) →
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y_1) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y_1) y)) z +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y_1) z) →
        ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x + y_1)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
          ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x + y_1)) y)) z +
            ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (x + y_1)) z)
[PROOFSTEP]
intro u₁ u₂ h₁ h₂
[GOAL]
case refine'_3
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z u₁ u₂ : A ⊗[R] L
h₁ :
  ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₁) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₁) y)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₁) z)
h₂ :
  ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₂) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₂) y)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) u₂) z)
⊢ ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (u₁ + u₂)) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) z) =
    ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (u₁ + u₂)) y)) z +
      ↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) y) (↑(↑(LieAlgebra.ExtendScalars.bracket' R A L) (u₁ + u₂)) z)
[PROOFSTEP]
rw [map_add, LinearMap.add_apply, LinearMap.add_apply, LinearMap.add_apply, map_add, map_add, LinearMap.add_apply, h₁,
  h₂, add_add_add_comm]
[GOAL]
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
⊢ ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆
[PROOFSTEP]
simp only [bracket_def, LinearMap.add_apply, LinearMap.map_add]
[GOAL]
R : Type u
A : Type w
L : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : A ⊗[R] L
⊢ ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆
[PROOFSTEP]
simp only [bracket_def, LinearMap.map_add]


[GOAL]
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : CommRing F
inst✝⁹ : Ring K
inst✝⁸ : AddCommGroup A
inst✝⁷ : Algebra F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Module.Free F K
inst✝ : Module.Free K A
⊢ lift (Module.rank F K) * lift (Module.rank K A) = lift (Module.rank F A)
[PROOFSTEP]
obtain ⟨_, b⟩ := Module.Free.exists_basis (R := F) (M := K)
[GOAL]
case intro.mk
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : CommRing F
inst✝⁹ : Ring K
inst✝⁸ : AddCommGroup A
inst✝⁷ : Algebra F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Module.Free F K
inst✝ : Module.Free K A
fst✝ : Type v
b : Basis fst✝ F K
⊢ lift (Module.rank F K) * lift (Module.rank K A) = lift (Module.rank F A)
[PROOFSTEP]
obtain ⟨_, c⟩ := Module.Free.exists_basis (R := K) (M := A)
[GOAL]
case intro.mk.intro.mk
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : CommRing F
inst✝⁹ : Ring K
inst✝⁸ : AddCommGroup A
inst✝⁷ : Algebra F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Module.Free F K
inst✝ : Module.Free K A
fst✝¹ : Type v
b : Basis fst✝¹ F K
fst✝ : Type w
c : Basis fst✝ K A
⊢ lift (Module.rank F K) * lift (Module.rank K A) = lift (Module.rank F A)
[PROOFSTEP]
rw [← (Module.rank F K).lift_id, ← b.mk_eq_rank, ← (Module.rank K A).lift_id, ← c.mk_eq_rank, ← lift_umax.{w, v}, ←
  (b.smul c).mk_eq_rank, mk_prod, lift_mul, lift_lift, lift_lift, lift_lift, lift_lift, lift_umax.{v, w}]
[GOAL]
F✝ : Type u
K✝ : Type v
A✝ : Type w
inst✝²¹ : CommRing F✝
inst✝²⁰ : Ring K✝
inst✝¹⁹ : AddCommGroup A✝
inst✝¹⁸ : Algebra F✝ K✝
inst✝¹⁷ : Module K✝ A✝
inst✝¹⁶ : Module F✝ A✝
inst✝¹⁵ : IsScalarTower F✝ K✝ A✝
inst✝¹⁴ : StrongRankCondition F✝
inst✝¹³ : StrongRankCondition K✝
inst✝¹² : Module.Free F✝ K✝
inst✝¹¹ : Module.Free K✝ A✝
F : Type u
K A : Type v
inst✝¹⁰ : CommRing F
inst✝⁹ : Ring K
inst✝⁸ : AddCommGroup A
inst✝⁷ : Algebra F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Module.Free F K
inst✝ : Module.Free K A
⊢ Module.rank F K * Module.rank K A = Module.rank F A
[PROOFSTEP]
convert lift_rank_mul_lift_rank F K A
[GOAL]
case h.e'_2.h.e'_5
F✝ : Type u
K✝ : Type v
A✝ : Type w
inst✝²¹ : CommRing F✝
inst✝²⁰ : Ring K✝
inst✝¹⁹ : AddCommGroup A✝
inst✝¹⁸ : Algebra F✝ K✝
inst✝¹⁷ : Module K✝ A✝
inst✝¹⁶ : Module F✝ A✝
inst✝¹⁵ : IsScalarTower F✝ K✝ A✝
inst✝¹⁴ : StrongRankCondition F✝
inst✝¹³ : StrongRankCondition K✝
inst✝¹² : Module.Free F✝ K✝
inst✝¹¹ : Module.Free K✝ A✝
F : Type u
K A : Type v
inst✝¹⁰ : CommRing F
inst✝⁹ : Ring K
inst✝⁸ : AddCommGroup A
inst✝⁷ : Algebra F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Module.Free F K
inst✝ : Module.Free K A
⊢ Module.rank F K = lift (Module.rank F K)
[PROOFSTEP]
rw [lift_id]
[GOAL]
case h.e'_2.h.e'_6
F✝ : Type u
K✝ : Type v
A✝ : Type w
inst✝²¹ : CommRing F✝
inst✝²⁰ : Ring K✝
inst✝¹⁹ : AddCommGroup A✝
inst✝¹⁸ : Algebra F✝ K✝
inst✝¹⁷ : Module K✝ A✝
inst✝¹⁶ : Module F✝ A✝
inst✝¹⁵ : IsScalarTower F✝ K✝ A✝
inst✝¹⁴ : StrongRankCondition F✝
inst✝¹³ : StrongRankCondition K✝
inst✝¹² : Module.Free F✝ K✝
inst✝¹¹ : Module.Free K✝ A✝
F : Type u
K A : Type v
inst✝¹⁰ : CommRing F
inst✝⁹ : Ring K
inst✝⁸ : AddCommGroup A
inst✝⁷ : Algebra F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Module.Free F K
inst✝ : Module.Free K A
⊢ Module.rank K A = lift (Module.rank K A)
[PROOFSTEP]
rw [lift_id]
[GOAL]
case h.e'_3
F✝ : Type u
K✝ : Type v
A✝ : Type w
inst✝²¹ : CommRing F✝
inst✝²⁰ : Ring K✝
inst✝¹⁹ : AddCommGroup A✝
inst✝¹⁸ : Algebra F✝ K✝
inst✝¹⁷ : Module K✝ A✝
inst✝¹⁶ : Module F✝ A✝
inst✝¹⁵ : IsScalarTower F✝ K✝ A✝
inst✝¹⁴ : StrongRankCondition F✝
inst✝¹³ : StrongRankCondition K✝
inst✝¹² : Module.Free F✝ K✝
inst✝¹¹ : Module.Free K✝ A✝
F : Type u
K A : Type v
inst✝¹⁰ : CommRing F
inst✝⁹ : Ring K
inst✝⁸ : AddCommGroup A
inst✝⁷ : Algebra F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Module.Free F K
inst✝ : Module.Free K A
⊢ Module.rank F A = lift (Module.rank F A)
[PROOFSTEP]
rw [lift_id]
[GOAL]
F : Type u
K : Type v
A : Type w
inst✝¹² : CommRing F
inst✝¹¹ : Ring K
inst✝¹⁰ : AddCommGroup A
inst✝⁹ : Algebra F K
inst✝⁸ : Module K A
inst✝⁷ : Module F A
inst✝⁶ : IsScalarTower F K A
inst✝⁵ : StrongRankCondition F
inst✝⁴ : StrongRankCondition K
inst✝³ : Module.Free F K
inst✝² : Module.Free K A
inst✝¹ : Module.Finite F K
inst✝ : Module.Finite K A
⊢ finrank F K * finrank K A = finrank F A
[PROOFSTEP]
letI := nontrivial_of_invariantBasisNumber F
[GOAL]
F : Type u
K : Type v
A : Type w
inst✝¹² : CommRing F
inst✝¹¹ : Ring K
inst✝¹⁰ : AddCommGroup A
inst✝⁹ : Algebra F K
inst✝⁸ : Module K A
inst✝⁷ : Module F A
inst✝⁶ : IsScalarTower F K A
inst✝⁵ : StrongRankCondition F
inst✝⁴ : StrongRankCondition K
inst✝³ : Module.Free F K
inst✝² : Module.Free K A
inst✝¹ : Module.Finite F K
inst✝ : Module.Finite K A
this : Nontrivial F := nontrivial_of_invariantBasisNumber F
⊢ finrank F K * finrank K A = finrank F A
[PROOFSTEP]
let b := Module.Free.chooseBasis F K
[GOAL]
F : Type u
K : Type v
A : Type w
inst✝¹² : CommRing F
inst✝¹¹ : Ring K
inst✝¹⁰ : AddCommGroup A
inst✝⁹ : Algebra F K
inst✝⁸ : Module K A
inst✝⁷ : Module F A
inst✝⁶ : IsScalarTower F K A
inst✝⁵ : StrongRankCondition F
inst✝⁴ : StrongRankCondition K
inst✝³ : Module.Free F K
inst✝² : Module.Free K A
inst✝¹ : Module.Finite F K
inst✝ : Module.Finite K A
this : Nontrivial F := nontrivial_of_invariantBasisNumber F
b : Basis (Module.Free.ChooseBasisIndex F K) F K := Module.Free.chooseBasis F K
⊢ finrank F K * finrank K A = finrank F A
[PROOFSTEP]
let c := Module.Free.chooseBasis K A
[GOAL]
F : Type u
K : Type v
A : Type w
inst✝¹² : CommRing F
inst✝¹¹ : Ring K
inst✝¹⁰ : AddCommGroup A
inst✝⁹ : Algebra F K
inst✝⁸ : Module K A
inst✝⁷ : Module F A
inst✝⁶ : IsScalarTower F K A
inst✝⁵ : StrongRankCondition F
inst✝⁴ : StrongRankCondition K
inst✝³ : Module.Free F K
inst✝² : Module.Free K A
inst✝¹ : Module.Finite F K
inst✝ : Module.Finite K A
this : Nontrivial F := nontrivial_of_invariantBasisNumber F
b : Basis (Module.Free.ChooseBasisIndex F K) F K := Module.Free.chooseBasis F K
c : Basis (Module.Free.ChooseBasisIndex K A) K A := Module.Free.chooseBasis K A
⊢ finrank F K * finrank K A = finrank F A
[PROOFSTEP]
rw [finrank_eq_card_basis b, finrank_eq_card_basis c, finrank_eq_card_basis (b.smul c), Fintype.card_prod]
[GOAL]
F : Type u
K : Type v
A : Type w
inst✝⁶ : Field F
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup A
inst✝³ : Algebra F K
inst✝² : Module K A
inst✝¹ : Module F A
inst✝ : IsScalarTower F K A
hf : FiniteDimensional F A
b : Finset A
hb : span F ↑b = ⊤
⊢ restrictScalars F (span K ↑b) = restrictScalars F ⊤
[PROOFSTEP]
rw [Submodule.restrictScalars_top, eq_top_iff, ← hb, Submodule.span_le]
[GOAL]
F : Type u
K : Type v
A : Type w
inst✝⁶ : Field F
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup A
inst✝³ : Algebra F K
inst✝² : Module K A
inst✝¹ : Module F A
inst✝ : IsScalarTower F K A
hf : FiniteDimensional F A
b : Finset A
hb : span F ↑b = ⊤
⊢ ↑b ⊆ ↑(restrictScalars F (span K ↑b))
[PROOFSTEP]
exact Submodule.subset_span
[GOAL]
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
⊢ finrank F K * finrank K A = finrank F A
[PROOFSTEP]
by_cases hA : FiniteDimensional K A
[GOAL]
case pos
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
hA : FiniteDimensional K A
⊢ finrank F K * finrank K A = finrank F A
[PROOFSTEP]
replace hA : FiniteDimensional K A := hA
[GOAL]
case pos
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
hA : FiniteDimensional K A
⊢ finrank F K * finrank K A = finrank F A
[PROOFSTEP]
rw [finrank_mul_finrank']
[GOAL]
case neg
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
hA : ¬FiniteDimensional K A
⊢ finrank F K * finrank K A = finrank F A
[PROOFSTEP]
rw [finrank_of_infinite_dimensional hA, mul_zero, finrank_of_infinite_dimensional]
[GOAL]
case neg
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
hA : ¬FiniteDimensional K A
⊢ ¬FiniteDimensional F A
[PROOFSTEP]
exact mt (@right F K A _ _ _ _ _ _ _) hA
[GOAL]
F : Type u
K✝ : Type v
A✝ : Type w
inst✝⁹ : Field F
inst✝⁸ : DivisionRing K✝
inst✝⁷ : AddCommGroup A✝
inst✝⁶ : Algebra F K✝
inst✝⁵ : Module K✝ A✝
inst✝⁴ : Module F A✝
inst✝³ : IsScalarTower F K✝ A✝
A : Type u_1
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
⊢ K = ⊥ ∨ K = ⊤
[PROOFSTEP]
haveI : FiniteDimensional _ _ := finiteDimensional_of_finrank hp.pos
[GOAL]
F : Type u
K✝ : Type v
A✝ : Type w
inst✝⁹ : Field F
inst✝⁸ : DivisionRing K✝
inst✝⁷ : AddCommGroup A✝
inst✝⁶ : Algebra F K✝
inst✝⁵ : Module K✝ A✝
inst✝⁴ : Module F A✝
inst✝³ : IsScalarTower F K✝ A✝
A : Type u_1
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this : FiniteDimensional F A
⊢ K = ⊥ ∨ K = ⊤
[PROOFSTEP]
letI := divisionRingOfFiniteDimensional F K
[GOAL]
F : Type u
K✝ : Type v
A✝ : Type w
inst✝⁹ : Field F
inst✝⁸ : DivisionRing K✝
inst✝⁷ : AddCommGroup A✝
inst✝⁶ : Algebra F K✝
inst✝⁵ : Module K✝ A✝
inst✝⁴ : Module F A✝
inst✝³ : IsScalarTower F K✝ A✝
A : Type u_1
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this✝ : FiniteDimensional F A
this : DivisionRing { x // x ∈ K } := divisionRingOfFiniteDimensional F { x // x ∈ K }
⊢ K = ⊥ ∨ K = ⊤
[PROOFSTEP]
refine' (hp.eq_one_or_self_of_dvd _ ⟨_, (finrank_mul_finrank F K A).symm⟩).imp _ fun h => _
[GOAL]
case refine'_1
F : Type u
K✝ : Type v
A✝ : Type w
inst✝⁹ : Field F
inst✝⁸ : DivisionRing K✝
inst✝⁷ : AddCommGroup A✝
inst✝⁶ : Algebra F K✝
inst✝⁵ : Module K✝ A✝
inst✝⁴ : Module F A✝
inst✝³ : IsScalarTower F K✝ A✝
A : Type u_1
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this✝ : FiniteDimensional F A
this : DivisionRing { x // x ∈ K } := divisionRingOfFiniteDimensional F { x // x ∈ K }
⊢ finrank F { x // x ∈ K } = 1 → K = ⊥
[PROOFSTEP]
exact Subalgebra.eq_bot_of_finrank_one
[GOAL]
case refine'_2
F : Type u
K✝ : Type v
A✝ : Type w
inst✝⁹ : Field F
inst✝⁸ : DivisionRing K✝
inst✝⁷ : AddCommGroup A✝
inst✝⁶ : Algebra F K✝
inst✝⁵ : Module K✝ A✝
inst✝⁴ : Module F A✝
inst✝³ : IsScalarTower F K✝ A✝
A : Type u_1
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this✝ : FiniteDimensional F A
this : DivisionRing { x // x ∈ K } := divisionRingOfFiniteDimensional F { x // x ∈ K }
h : finrank F { x // x ∈ K } = finrank F A
⊢ K = ⊤
[PROOFSTEP]
exact Algebra.toSubmodule_eq_top.1 (eq_top_of_finrank_eq <| K.finrank_toSubmodule.trans h)