-- Mathlib/RingTheory/Algebraic/LinearIndependent.lean
theorem Transcendental.linearIndependent_sub_inv
    {F E : Type*} [Field F] [Field E] [Algebra F E] {x : E} (H : Transcendental F x) :
    LinearIndependent F fun a ↦ (x - algebraMap F E a)⁻¹

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : Transcendental F x
⊢ LinearIndependent F fun a => (x - (algebraMap F E) a)⁻¹

Tactic:
classical
rw [transcendental_iff] at H
refine linearIndependent_iff'.2 fun s m hm i hi ↦ ?_
have hnz (a : F) : x - algebraMap F E a ≠ 0 := fun h ↦
  X_sub_C_ne_zero a <| H (.X - .C a) (by simp [h])
let b := s.prod fun j ↦ x - algebraMap F E j
have h1 : ∀ i ∈ s, m i • (b * (x - algebraMap F E i)⁻¹) =
    m i • (s.erase i).prod fun j ↦ x - algebraMap F E j := fun i hi ↦ by
  simp_rw [b, ← s.prod_erase_mul _ hi, mul_inv_cancel_right₀ (hnz i)]
replace hm := congr(b * $(hm))
simp_rw [mul_zero, Finset.mul_sum, mul_smul_comm, Finset.sum_congr rfl h1] at hm
let p : Polynomial F := s.sum fun i ↦ .C (m i) * (s.erase i).prod fun j ↦ .X - .C j
replace hm := congr(Polynomial.aeval i $(H p (by simp_rw [← hm, p, map_sum, map_mul, map_prod,
  map_sub, aeval_X, aeval_C, Algebra.smul_def])))
have h2 : ∀ j ∈ s.erase i, m j * ((s.erase j).prod fun x ↦ i - x) = 0 := fun j hj ↦ by
  have := Finset.mem_erase_of_ne_of_mem (Finset.ne_of_mem_erase hj).symm hi
  simp_rw [← (s.erase j).prod_erase_mul _ this, sub_self, mul_zero]
simp_rw [map_zero, p, map_sum, map_mul, map_prod, map_sub, aeval_X,
  aeval_C, Algebra.id.map_eq_self, ← s.sum_erase_add _ hi,
  Finset.sum_eq_zero h2, zero_add] at hm
exact eq_zero_of_ne_zero_of_mul_right_eq_zero (Finset.prod_ne_zero_iff.2 fun j hj ↦
  sub_ne_zero.2 (Finset.ne_of_mem_erase hj).symm) hm

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
hm : (aeval i) p = (aeval i) 0
j : F
hj : j ∈ s.erase i
⊢ m j * ∏ x ∈ s.erase j, (i - x) = 0

Tactic:
have := Finset.mem_erase_of_ne_of_mem (Finset.ne_of_mem_erase hj).symm hi

Result:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
hm : (aeval i) p = (aeval i) 0
j : F
hj : j ∈ s.erase i
this : i ∈ s.erase j
⊢ m j * ∏ x ∈ s.erase j, (i - x) = 0

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j) = 0
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
⊢ (aeval x) p = 0

Tactic:
simp_rw [← hm, p, map_sum, map_mul, map_prod,
map_sub, aeval_X, aeval_C, Algebra.smul_def]

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j) = 0
⊢ m i = 0

Tactic:
let p : Polynomial F := s.sum fun i ↦ .C (m i) * (s.erase i).prod fun j ↦ .X - .C j

Result:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j) = 0
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
⊢ m i = 0

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
hm : m i * ∏ x ∈ s.erase i, (i - x) = 0
⊢ m i = 0

Tactic:
exact eq_zero_of_ne_zero_of_mul_right_eq_zero (Finset.prod_ne_zero_iff.2 fun j hj ↦
  sub_ne_zero.2 (Finset.ne_of_mem_erase hj).symm) hm

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
⊢ LinearIndependent F fun a => (x - (algebraMap F E) a)⁻¹

Tactic:
refine linearIndependent_iff'.2 fun s m hm i hi ↦ ?_

Result:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
hm : ∑ i ∈ s, m i • (x - (algebraMap F E) i)⁻¹ = 0
i : F
hi : i ∈ s
⊢ m i = 0

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
hm : ∑ i ∈ s, m i • (x - (algebraMap F E) i)⁻¹ = 0
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
⊢ m i = 0

Tactic:
replace hm := congr(b * $(hm))

Result:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : b * ∑ i ∈ s, m i • (x - (algebraMap F E) i)⁻¹ = b * 0
⊢ m i = 0

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
hm : ∑ i ∈ s, m i • (x - (algebraMap F E) i)⁻¹ = 0
i : F
hi : i ∈ s
⊢ m i = 0

Tactic:
have hnz (a : F) : x - algebraMap F E a ≠ 0 := fun h ↦
  X_sub_C_ne_zero a <| H (.X - .C a) (by simp [h])

Result:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
hm : ∑ i ∈ s, m i • (x - (algebraMap F E) i)⁻¹ = 0
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
⊢ m i = 0