[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ StrongRankCondition R
[PROOFSTEP]
suffices ∀ n, ∀ f : (Fin (n + 1) → R) →ₗ[R] Fin n → R, ¬Injective f by rwa [strongRankCondition_iff_succ R]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
this : ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ↑f
⊢ StrongRankCondition R
[PROOFSTEP]
rwa [strongRankCondition_iff_succ R]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ↑f
[PROOFSTEP]
intro n f
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
⊢ ¬Injective ↑f
[PROOFSTEP]
by_contra hf
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
⊢ False
[PROOFSTEP]
let g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := (ExtendByZero.linearMap R castSucc).comp f
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
⊢ False
[PROOFSTEP]
have hg : Injective g := (extend_injective Fin.strictMono_castSucc.injective _).comp hf
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
⊢ False
[PROOFSTEP]
have hnex : ¬∃ i : Fin n, castSucc i = last n := fun ⟨i, hi⟩ => ne_of_lt (castSucc_lt_last i) hi
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
⊢ False
[PROOFSTEP]
let a₀ := (minpoly R g).coeff 0
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
a₀ : R := coeff (minpoly R g) 0
⊢ False
[PROOFSTEP]
have : a₀ ≠ 0 := minpoly_coeff_zero_of_injective hg
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
a₀ : R := coeff (minpoly R g) 0
this : a₀ ≠ 0
⊢ False
[PROOFSTEP]
have : a₀ = 0 := by
  -- Evaluate `(minpoly R g) g` at the vector `(0,...,0,1)`
  have heval := LinearMap.congr_fun (minpoly.aeval R g) (Pi.single (Fin.last n) 1)
  obtain ⟨P, hP⟩ := X_dvd_iff.2 (erase_same (minpoly R g) 0)
  rw [← monomial_add_erase (minpoly R g) 0, hP] at heval 
  replace heval :=
    congr_fun heval
      (Fin.last n)
        -- Porting note: ...it's just that this line gives a timeout without slightly raising heartbeats
  simpa [hnex] using heval
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
a₀ : R := coeff (minpoly R g) 0
this : a₀ ≠ 0
⊢ a₀ = 0
[PROOFSTEP]
have heval := LinearMap.congr_fun (minpoly.aeval R g) (Pi.single (Fin.last n) 1)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
a₀ : R := coeff (minpoly R g) 0
this : a₀ ≠ 0
heval : ↑(↑(aeval g) (minpoly R g)) (Pi.single (last n) 1) = ↑0 (Pi.single (last n) 1)
⊢ a₀ = 0
[PROOFSTEP]
obtain ⟨P, hP⟩ := X_dvd_iff.2 (erase_same (minpoly R g) 0)
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
a₀ : R := coeff (minpoly R g) 0
this : a₀ ≠ 0
heval : ↑(↑(aeval g) (minpoly R g)) (Pi.single (last n) 1) = ↑0 (Pi.single (last n) 1)
P : R[X]
hP : erase 0 (minpoly R g) = X * P
⊢ a₀ = 0
[PROOFSTEP]
rw [← monomial_add_erase (minpoly R g) 0, hP] at heval 
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
a₀ : R := coeff (minpoly R g) 0
this : a₀ ≠ 0
P : R[X]
heval : ↑(↑(aeval g) (↑(monomial 0) (coeff (minpoly R g) 0) + X * P)) (Pi.single (last n) 1) = ↑0 (Pi.single (last n) 1)
hP : erase 0 (minpoly R g) = X * P
⊢ a₀ = 0
[PROOFSTEP]
replace heval :=
  congr_fun heval
    (Fin.last n)
      -- Porting note: ...it's just that this line gives a timeout without slightly raising heartbeats
[GOAL]
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
a₀ : R := coeff (minpoly R g) 0
this : a₀ ≠ 0
P : R[X]
hP : erase 0 (minpoly R g) = X * P
heval :
  ↑(↑(aeval g) (↑(monomial 0) (coeff (minpoly R g) 0) + X * P)) (Pi.single (last n) 1) (last n) =
    ↑0 (Pi.single (last n) 1) (last n)
⊢ a₀ = 0
[PROOFSTEP]
simpa [hnex] using heval
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R := LinearMap.comp (ExtendByZero.linearMap R castSucc) f
hg : Injective ↑g
hnex : ¬∃ i, castSucc i = last n
a₀ : R := coeff (minpoly R g) 0
this✝ : a₀ ≠ 0
this : a₀ = 0
⊢ False
[PROOFSTEP]
contradiction
