awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.LinearIndependent (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
h1 :
  ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
hm :
  Eq.{u_2 + 1} (α := E)
    (∑ x_1 ∈ s,
      HSMul.hSMul (β := E) (m x_1) (∏ j ∈ s.erase x_1, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)))
    0
p : F[X] :=
  ∑ i ∈ s,
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m i) : F[X])
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])
simp_rw :
  Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E)
    (∑ x_1 ∈ s,
        HSMul.hSMul (β := E) (m x_1) (∏ j ∈ s.erase x_1, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)) :
      E)
simp_rw₁ :
  Eq.{u_2 + 1} (α := E)
    ((aeval x : (a : F[X]) → E)
        (∑ i ∈ s,
          HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m i) : F[X])
            (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])) :
      E)
    (∑ x_1 ∈ s,
        HSMul.hSMul (β := E) (m x_1) (∏ j ∈ s.erase x_1, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)) :
      E)
simp_rw₂ :
  Eq.{u_2 + 1} (α := E)
    (∑ x_1 ∈ s,
      (aeval x : (a : F[X]) → E)
        (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m x_1) : F[X])
          (∏ j ∈ s.erase x_1, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])))
    (∑ x_1 ∈ s,
      HSMul.hSMul (β := E) (m x_1) (∏ j ∈ s.erase x_1, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)))
simp_rw₃ :
  Eq.{u_2 + 1} (α := E)
    (∑ x_1 ∈ s,
      HMul.hMul (α := E) (β := E) ((aeval x : (a : F[X]) → E) ((C : (a : F) → F[X]) (m x_1) : F[X]) : E)
        ((aeval x : (a : F[X]) → E)
            (∏ j ∈ s.erase x_1, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X])) :
          E))
    (∑ x_1 ∈ s,
      HSMul.hSMul (β := E) (m x_1) (∏ j ∈ s.erase x_1, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)))
⊢ Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E)
have simp_rw₄ : Eq.{u_2 + 1} (α := E)
  (∑ x_1 ∈ s,
    HMul.hMul (α := E) (β := E) ((aeval x : (a : F[X]) → E) ((C : (a : F) → F[X]) (m x_1) : F[X]) : E)
      (∏ x_2 ∈ s.erase x_1,
          (aeval x : (a : F[X]) → E) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x_2 : F[X])) :
        E))
  (∑ x_1 ∈ s,
    HSMul.hSMul (β := E) (m x_1) (∏ j ∈ s.erase x_1, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)))
Tactic: simp_rw [← hm, p, map_sum, map_mul, map_prod,
    map_sub, aeval_X, aeval_C, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.LinearIndependent (hypothesis)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
h1 :
  ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
hm :
  Eq.{u_2 + 1} (α := E)
    (∑ x_1 ∈ s,
      HSMul.hSMul (β := E) (m x_1) (∏ j ∈ s.erase x_1, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)))
    0
p : F[X] :=
  ∑ i ∈ s,
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m i) : F[X])
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])
⊢ m i = 0
have hm₁ : Eq (α := F) ((aeval i : (a : F[X]) → F) p : F) ((aeval i : (a : F[X]) → F) 0 : F)
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])))
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.LinearIndependent (hypothesis)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
h1 :
  ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
p : F[X] :=
  ∑ i ∈ s,
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m i) : F[X])
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])
hm : Eq (α := F) ((aeval i : (a : F[X]) → F) p : F) ((aeval i : (a : F[X]) → F) 0 : F)
j : F
hj : j ∈ s.erase i
⊢ m j * ∏ x ∈ s.erase j, (i - x) = 0
have this : i ∈ s.erase j
Tactic: have := Finset.mem_erase_of_ne_of_mem (Finset.ne_of_mem_erase hj).symm hi
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.LinearIndependent (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
h1 :
  ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
p : F[X] :=
  ∑ i ∈ s,
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m i) : F[X])
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])
hm : Eq (α := F) ((aeval i : (a : F[X]) → F) p : F) ((aeval i : (a : F[X]) → F) 0 : F)
j : F
hj : j ∈ s.erase i
this : i ∈ s.erase j
⊢ m j * ∏ x ∈ s.erase j, (i - x) = 0
have simp_rw : m j * ((∏ x ∈ (s.erase j).erase i, (i - x)) * (i - i)) = 0
Tactic: simp_rw [← (s.erase j).prod_erase_mul _ this, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.LinearIndependent (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
h1 :
  ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
p : F[X] :=
  ∑ i ∈ s,
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m i) : F[X])
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])
hm : Eq (α := F) ((aeval i : (a : F[X]) → F) p : F) ((aeval i : (a : F[X]) → F) 0 : F)
j : F
hj : j ∈ s.erase i
this : i ∈ s.erase j
simp_rw : m j * ((∏ x ∈ (s.erase j).erase i, (i - x)) * (i - i)) = 0
⊢ m j * ∏ x ∈ s.erase j, (i - x) = 0
have simp_rw₁ : m j * HMul.hMul (α := F) (∏ x ∈ (s.erase j).erase i, (i - x)) 0 = 0
Tactic: simp_rw [← (s.erase j).prod_erase_mul _ this, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.LinearIndependent (hypothesis)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
h1 :
  ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
p : F[X] :=
  ∑ i ∈ s,
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m i) : F[X])
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])
hm : Eq (α := F) ((aeval i : (a : F[X]) → F) p : F) ((aeval i : (a : F[X]) → F) 0 : F)
⊢ m i = 0
have h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.LinearIndependent (hypothesis)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
h1 :
  ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
p : F[X] :=
  ∑ i ∈ s,
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m i) : F[X])
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])
hm : Eq (α := F) ((aeval i : (a : F[X]) → F) p : F) ((aeval i : (a : F[X]) → F) 0 : F)
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
⊢ m i = 0
have hm₁ : m i * ∏ x ∈ s.erase i, (i - x) = 0
Tactic: simp_rw [map_zero, p, map_sum, map_mul, map_prod, map_sub, aeval_X,
    aeval_C, Algebra.algebraMap_self_apply, ← s.sum_erase_add _ hi,
    Finset.sum_eq_zero h2, zero_add] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.LinearIndependent (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : Transcendental F x
⊢ LinearIndependent.{u_1, u_1, u_2} F (M := E) fun (a : F) ↦
    (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E))⁻¹
have rw : ∀ (H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0),
  LinearIndependent.{u_1, u_1, u_2} F (M := E) fun (a : F) ↦
    (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E))⁻¹
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.algebraMap_self_apply, ← 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.LinearIndependent (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : Transcendental F x
rw rw₁ rw₂ :
  ∀ (H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0),
    LinearIndependent.{u_1, u_1, u_2} F (M := E) fun (a : F) ↦
      (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E))⁻¹
⊢ LinearIndependent.{u_1, u_1, u_2} F (M := E) fun (a : F) ↦
    (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E))⁻¹
have rw₃ : ∀ (H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0) (s : Finset F)
  (m : F → F)
  (hm : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, m i • (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) 0)
  (i : F) (hi : i ∈ s), m i = 0
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.algebraMap_self_apply, ← 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.LinearIndependent (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : Transcendental F x
rw rw₁ rw₂ :
  ∀ (H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0),
    LinearIndependent.{u_1, u_1, u_2} F (M := E) fun (a : F) ↦
      (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E))⁻¹
rw₃ :
  ∀ (H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0) (s : Finset F)
    (m : F → F)
    (hm : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, m i • (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) 0)
    (i : F) (hi : i ∈ s), m i = 0
⊢ LinearIndependent.{u_1, u_1, u_2} F (M := E) fun (a : F) ↦
    (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E))⁻¹
have rw₄ : ∀ (H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0) (s : Finset F)
  (m : F → F)
  (hm : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, m i • (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) 0)
  (i : F) (hi : i ∈ s) (hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0), m i = 0
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.algebraMap_self_apply, ← 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
hf : Transcendental R f
⊢ Transcendental ↥(supported R s) (A := MvPolynomial σ R)
    ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f : MvPolynomial σ R)
have rw : ∀ (hf : Function.Injective (α := R[X]) (β := R[X]) (⇑(Polynomial.aeval f) : (a : R[X]) → R[X])),
  Function.Injective (α := (↥(supported R s))[X]) (β := MvPolynomial σ R)
    (⇑(Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f) :
          (↥(supported R s))[X] →ₐ[↥(supported R s)] MvPolynomial σ R) :
      (a : (↥(supported R s))[X]) → MvPolynomial σ R)
Tactic: rw [transcendental_iff_injective] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
hf : Function.Injective (α := R[X]) (β := R[X]) (⇑(Polynomial.aeval f) : (a : R[X]) → R[X])
g : MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] →ₐ[R] MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] :=
  mapAlgHom (Polynomial.aeval f)
⊢ Function.Injective (α := (↥(supported R s))[X]) (β := MvPolynomial σ R)
    (⇑(Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f) :
          (↥(supported R s))[X] →ₐ[↥(supported R s)] MvPolynomial σ R) :
      (a : (↥(supported R s))[X]) → MvPolynomial σ R)
have hf₁ : Function.Injective (α := MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X]) (β :=
  MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X])
  (⇑g : (a : MvPolynomial (↑s : Type u_1) R[X]) → MvPolynomial (↑s : Type u_1) R[X])
Tactic: replace hf : Function.Injective g := MvPolynomial.map_injective _ hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.MvPolynomial (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] →ₐ[R] MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X] :=
  mapAlgHom (Polynomial.aeval f)
hf :
  Function.Injective (α := MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X]) (β :=
    MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X])
    (⇑g : (a : MvPolynomial (↑s : Type u_1) R[X]) → MvPolynomial (↑s : Type u_1) R[X])
u : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.comp
        (AlgHom.comp (Subalgebra.val (supported R (insert i s)))
          (↑(AlgEquiv.trans
                (AlgEquiv.trans (AlgEquiv.symm (optionEquivRight R (↑s : Type u_1)))
                  (renameEquiv R (Set.subtypeInsertEquivOption (t := s) h).symm))
                (AlgEquiv.symm (supportedEquivMvPolynomial (insert i s)))) :
            MvPolynomial (↑s : Type u_1) R[X] →ₐ[R] ↥(supported R (insert i s))))
        g).comp
    (↑(AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) (optionEquivRight R (↑s : Type u_1))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial (↑s : Type u_1) R[X])
v : (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X] →ₐ[R] MvPolynomial σ R :=
  AlgHom.comp
    (AlgHom.restrictScalars R (S := ↥(supported R s))
      (Polynomial.aeval ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) f)))
    (↑(Polynomial.mapAlgEquiv (AlgEquiv.symm (supportedEquivMvPolynomial s))) :
      (MvPolynomial (↑s : Type u_1) R)[X] →ₐ[R] (↥(supported R s))[X])
⊢ Function.Injective (α := (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X]) (β :=
    MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X])
    (Function.comp (β := MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X])
      (⇑g : (a : MvPolynomial (↑s : Type u_1) R[X]) → MvPolynomial (↑s : Type u_1) R[X])
      (Function.comp (β := MvPolynomial.{u_1, u_2} (Option (↑s : Type u_1)) R)
        (⇑(optionEquivRight R (↑s : Type u_1)) :
          (a : MvPolynomial (Option (↑s : Type u_1)) R) → MvPolynomial (↑s : Type u_1) R[X])
        (⇑(AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) :
          (a : (MvPolynomial (↑s : Type u_1) R)[X]) → MvPolynomial (Option (↑s : Type u_1)) R)))
have apply : Function.Injective (α := (MvPolynomial.{u_1, u_2} (↑s : Type u_1) R)[X]) (β :=
  MvPolynomial.{u_1, u_2} (↑s : Type u_1) R[X])
  (Function.comp (β := MvPolynomial.{u_1, u_2} (Option (↑s : Type u_1)) R)
    (⇑(optionEquivRight R (↑s : Type u_1)) :
      (a : MvPolynomial (Option (↑s : Type u_1)) R) → MvPolynomial (↑s : Type u_1) R[X])
    (⇑(AlgEquiv.symm (optionEquivLeft R (↑s : Type u_1))) :
      (a : (MvPolynomial (↑s : Type u_1) R)[X]) → MvPolynomial (Option (↑s : Type u_1)) R))
Tactic: apply hf.comp