-- 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 : ∀ (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)
i : F
hi : i ∈ s
⊢ m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)

Tactic:
simp_rw [b, ← s.prod_erase_mul _ hi, mul_inv_cancel_right₀ (hnz i)]

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 : Transcendental F x
⊢ LinearIndependent F fun a => (x - (algebraMap F E) a)⁻¹

Tactic:
rw [transcendental_iff] at 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
⊢ 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 : ∀ (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
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
⊢ m i = 0

Tactic:
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

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

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
this : i ∈ s.erase j
⊢ m j * ∏ x ∈ s.erase j, (i - x) = 0

Tactic:
simp_rw [← (s.erase j).prod_erase_mul _ this, sub_self, mul_zero]

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
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)
⊢ m i = 0

Tactic:
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)]

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

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
a : F
h : x - (algebraMap F E) a = 0
⊢ (aeval x) (X - C a) = 0

Tactic:
simp [h]

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
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
⊢ m i = 0

Tactic:
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])))

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
⊢ 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
⊢ m i = 0

Tactic:
let b := s.prod fun j ↦ x - algebraMap F E 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
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)
⊢ 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)
hm : b * ∑ i ∈ s, m i • (x - (algebraMap F E) i)⁻¹ = b * 0
⊢ m i = 0

Tactic:
simp_rw [mul_zero, Finset.mul_sum, mul_smul_comm, Finset.sum_congr rfl h1] at 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 : ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j) = 0
⊢ m i = 0