awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst_7 : NoZeroDivisors S
⊢ Algebra.IsAlgebraic.{u_1, u_2} R[X] S[X]
have pos : ∀ (h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)),
  Algebra.IsAlgebraic.{u_1, u_2} R[X] S[X]
Tactic: by_cases h : Function.Injective (algebraMap R S)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst_7 : NoZeroDivisors S
pos :
  ∀ (h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)),
    Algebra.IsAlgebraic.{u_1, u_2} R[X] S[X]
⊢ Algebra.IsAlgebraic.{u_1, u_2} R[X] S[X]
have neg : ∀ (h : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)),
  Algebra.IsAlgebraic.{u_1, u_2} R[X] S[X]
Tactic: by_cases h : Function.Injective (algebraMap R S)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst_7 : NoZeroDivisors S
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Algebra.IsAlgebraic.{u_1, u_2} R[X] S[X]
have this : NoZeroDivisors R
Tactic: have := h.noZeroDivisors _ (map_zero _) (map_mul _)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst_7 : NoZeroDivisors S
h : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Algebra.IsAlgebraic.{u_1, u_2} R[X] S[X]
have h₁ : ¬Function.Injective (α := R[X]) (β := S[X]) (map (algebraMap R S))
Tactic: rw [← Polynomial.map_injective_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
z : A
z' : S
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst_7 : NoZeroDivisors S
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)
have pos : ∀ (h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)),
  Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)
Tactic: by_cases h : Function.Injective (algebraMap R S)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
z : A
z' : S
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst_7 : NoZeroDivisors S
pos :
  ∀ (h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)),
    Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)
have neg : ∀ (h : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)),
  Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)
Tactic: by_cases h : Function.Injective (algebraMap R S)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
z : A
z' : S
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst_7 : NoZeroDivisors S
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)
have this : NoZeroDivisors R
Tactic: have := h.noZeroDivisors _ (map_zero _) (map_mul _)
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
z : A
z' : S
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst_7 : NoZeroDivisors S
h : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)
have neg : ∀
  (h :
    ¬Function.Injective (α := MvPolynomial σ R) (β := MvPolynomial σ S)
        (⇑(MvPolynomial.map (algebraMap R S)) : (a : MvPolynomial σ R) → MvPolynomial σ S)),
  Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)
Tactic: rw [← MvPolynomial.map_injective_iff] at h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
⊢ Module.rank.{u_1, u_2} (FractionRing R[X]) (FractionRing S[X]) = Module.rank R S
have this : IsDomain R
Tactic: have := IsDomain.of_faithfulSMul R S
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
this : IsDomain R
⊢ Module.rank.{u_1, u_2} (FractionRing R[X]) (FractionRing S[X]) = Module.rank R S
have rw : Module.rank.{u_1, u_2} R[X] S[X] = Module.rank R S
Tactic: rw [rank_fractionRing, rank_polynomial_polynomial]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
this : IsDomain R
rw : Module.rank.{u_1, u_2} R[X] S[X] = Module.rank R S
⊢ Module.rank.{u_1, u_2} (FractionRing R[X]) (FractionRing S[X]) = Module.rank R S
have rw₁ : Module.rank R S = Module.rank R S
Tactic: rw [rank_fractionRing, rank_polynomial_polynomial]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
σ : Type u
⊢ Module.rank (FractionRing (MvPolynomial σ R)) (FractionRing (MvPolynomial σ S)) = lift.{u, u_2} (Module.rank R S)
have this : IsDomain R
Tactic: have := IsDomain.of_faithfulSMul R S
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
σ : Type u
this : IsDomain R
⊢ Module.rank (FractionRing (MvPolynomial σ R)) (FractionRing (MvPolynomial σ S)) = lift.{u, u_2} (Module.rank R S)
have rw : Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = lift.{u, u_2} (Module.rank R S)
Tactic: rw [rank_fractionRing, rank_mvPolynomial_mvPolynomial]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
σ : Type u
this : IsDomain R
rw : Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = lift.{u, u_2} (Module.rank R S)
⊢ Module.rank (FractionRing (MvPolynomial σ R)) (FractionRing (MvPolynomial σ S)) = lift.{u, u_2} (Module.rank R S)
have rw₁ : lift.{u, u_2} (Module.rank R S) = lift.{u, u_2} (Module.rank R S)
Tactic: rw [rank_fractionRing, rank_mvPolynomial_mvPolynomial]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Integral (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
z : A
z' : S
inst_7 : IsDomain R
inst_8 : IsDomain S
inst_9 : IsTorsionFree R S
inst_10 : Module.Finite R S
⊢ FiniteDimensional.{u_1, u_2} (FractionRing R) (FractionRing S)
have obtain : ∀ (w : ℕ) (s : Fin w → S) (hs : Eq (α := Submodule R S) (Submodule.span R (Set.range s)) ⊤),
  FiniteDimensional.{u_1, u_2} (FractionRing R) (FractionRing S)
Tactic: obtain ⟨_, s, hs⟩ := Module.Finite.exists_fin (R := R) (M := S)
-- 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 : 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 H₁ : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
Tactic: rw [transcendental_iff] at H
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 : ∀ (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))⁻¹
have refine : ∀ (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: refine linearIndependent_iff'.2 fun s m hm i hi ↦ ?_
-- 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
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
have hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 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])
-- 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
hm : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, m i • (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) 0
i_1 : F
hi_1 : i_1 ∈ 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)
i : F
hi : i ∈ s
simp_rw :
  m i •
      ((∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)) *
        (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))
⊢ 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))
have simp_rw₁ : m i •
    ((∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)) *
        HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E) *
      (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))
Tactic: simp_rw [b, ← s.prod_erase_mul _ hi, mul_inv_cancel_right₀ (hnz i)]
-- 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
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
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
⊢ m i = 0
have 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))
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)]
-- 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
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
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))
⊢ m i = 0
have hm₁ : b * ∑ i ∈ s, m i • (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹ = b * 0
Tactic: replace hm := congr(b * $(hm))
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))
hm : b * ∑ i ∈ s, m i • (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹ = b * 0
⊢ m i = 0
have 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
Tactic: simp_rw [mul_zero, Finset.mul_sum, mul_smul_comm, Finset.sum_congr rfl h1] 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 : ∀ (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])
⊢ Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E)
have 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)
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 (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)
⊢ 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,
    (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)))
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 (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)))
⊢ 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)
      ((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)))
Tactic: simp_rw [← hm, p, map_sum, map_mul, map_prod,
    map_sub, aeval_X, aeval_C, Algebra.smul_def]