awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
N : Submodule R M
h : finrank.{u_1, u} R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank.{u_1, u} R (M ⧸ N)
hs' : LinearIndependent.{u, u_1, u} (ι := ↥s) R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s))
v : M
hv : Membership.mem (α := M ⧸ N) s ((N.mkQ : (a : M) → M ⧸ N) v : M ⧸ N)
r : R
hr : r ≠ 0
this :
  Eq.{u + 1} (α := M ⧸ N)
      ((Finsupp.linearCombination R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s)) : (a : ↥s →₀ R) → M ⧸ N)
          (Finsupp.single (Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) r) :
        M ⧸ N)
      (0 : M ⧸ N) →
    Eq (α := Finsupp.{u, u_1} (↥s) R)
      (Finsupp.single (Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) r :
        Finsupp.{u, u_1} (↥s) R)
      (0 : Finsupp.{u, u_1} (↥s) R)
⊢ r • v ∈ N → r = 0
have rwa : ∀
  (this :
    HSMul.hSMul (β := M ⧸ N) r
          ((↑(Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) : M ⧸ N) : M ⧸ N) =
        0 →
      Eq (α := Finsupp.{u, u_1} (↥s) R)
        (Finsupp.single (Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) r :
          Finsupp.{u, u_1} (↥s) R)
        (0 : Finsupp.{u, u_1} (↥s) R)),
  r • v ∈ N → r = 0
Tactic: rwa [Finsupp.linearCombination_single, Finsupp.single_eq_zero, ← map_smul,
    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
N : Submodule R M
h : finrank.{u_1, u} R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank.{u_1, u} R (M ⧸ N)
hs' : LinearIndependent.{u, u_1, u} (ι := ↥s) R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s))
v : M
hv : Membership.mem (α := M ⧸ N) s ((N.mkQ : (a : M) → M ⧸ N) v : M ⧸ N)
r : R
hr : r ≠ 0
this :
  Eq.{u + 1} (α := M ⧸ N)
      ((Finsupp.linearCombination R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s)) : (a : ↥s →₀ R) → M ⧸ N)
          (Finsupp.single (Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) r) :
        M ⧸ N)
      (0 : M ⧸ N) →
    Eq (α := Finsupp.{u, u_1} (↥s) R)
      (Finsupp.single (Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) r :
        Finsupp.{u, u_1} (↥s) R)
      (0 : Finsupp.{u, u_1} (↥s) R)
rwa :
  ∀
    (this :
      HSMul.hSMul (β := M ⧸ N) r
            ((↑(Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) : M ⧸ N) : M ⧸ N) =
          0 →
        Eq (α := Finsupp.{u, u_1} (↥s) R)
          (Finsupp.single (Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) r :
            Finsupp.{u, u_1} (↥s) R)
          (0 : Finsupp.{u, u_1} (↥s) R)),
    r • v ∈ N → r = 0
⊢ r • v ∈ N → r = 0
have rwa₁ : ∀
  (this :
    HSMul.hSMul (β := M ⧸ N) r
          ((↑(Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) : M ⧸ N) : M ⧸ N) =
        0 →
      r = 0),
  r • v ∈ N → r = 0
Tactic: rwa [Finsupp.linearCombination_single, Finsupp.single_eq_zero, ← map_smul,
    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
N : Submodule R M
h : finrank.{u_1, u} R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank.{u_1, u} R (M ⧸ N)
hs' : LinearIndependent.{u, u_1, u} (ι := ↥s) R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s))
v : M
hv : Membership.mem (α := M ⧸ N) s ((N.mkQ : (a : M) → M ⧸ N) v : M ⧸ N)
r : R
hr : r ≠ 0
this :
  Eq.{u + 1} (α := M ⧸ N)
      ((Finsupp.linearCombination R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s)) : (a : ↥s →₀ R) → M ⧸ N)
          (Finsupp.single (Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) r) :
        M ⧸ N)
      (0 : M ⧸ N) →
    Eq (α := Finsupp.{u, u_1} (↥s) R)
      (Finsupp.single (Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) r :
        Finsupp.{u, u_1} (↥s) R)
      (0 : Finsupp.{u, u_1} (↥s) R)
rwa :
  ∀
    (this :
      HSMul.hSMul (β := M ⧸ N) r
            ((↑(Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) : M ⧸ N) : M ⧸ N) =
          0 →
        Eq (α := Finsupp.{u, u_1} (↥s) R)
          (Finsupp.single (Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) r :
            Finsupp.{u, u_1} (↥s) R)
          (0 : Finsupp.{u, u_1} (↥s) R)),
    r • v ∈ N → r = 0
rwa₁ :
  ∀
    (this :
      HSMul.hSMul (β := M ⧸ N) r
            ((↑(Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) : M ⧸ N) : M ⧸ N) =
          0 →
        r = 0),
    r • v ∈ N → r = 0
⊢ r • v ∈ N → r = 0
have rwa₂ : ∀ (this : Eq (α := M ⧸ N) ((N.mkQ : (a : M) → M ⧸ N) (r • v) : M ⧸ N) (0 : M ⧸ N) → r = 0), r • v ∈ N → r = 0
Tactic: rwa [Finsupp.linearCombination_single, Finsupp.single_eq_zero, ← map_smul,
    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
N : Submodule R M
h : finrank.{u_1, u} R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank.{u_1, u} R (M ⧸ N)
hs' : LinearIndependent.{u, u_1, u} (ι := ↥s) R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s))
v : M
hv : Membership.mem (α := M ⧸ N) s ((N.mkQ : (a : M) → M ⧸ N) v : M ⧸ N)
r : R
hr : r ≠ 0
this :
  Eq.{u + 1} (α := M ⧸ N)
      ((Finsupp.linearCombination R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s)) : (a : ↥s →₀ R) → M ⧸ N)
          (Finsupp.single (Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) r) :
        M ⧸ N)
      (0 : M ⧸ N) →
    Eq (α := Finsupp.{u, u_1} (↥s) R)
      (Finsupp.single (Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) r :
        Finsupp.{u, u_1} (↥s) R)
      (0 : Finsupp.{u, u_1} (↥s) R)
rwa :
  ∀
    (this :
      HSMul.hSMul (β := M ⧸ N) r
            ((↑(Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) : M ⧸ N) : M ⧸ N) =
          0 →
        Eq (α := Finsupp.{u, u_1} (↥s) R)
          (Finsupp.single (Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) r :
            Finsupp.{u, u_1} (↥s) R)
          (0 : Finsupp.{u, u_1} (↥s) R)),
    r • v ∈ N → r = 0
rwa₁ :
  ∀
    (this :
      HSMul.hSMul (β := M ⧸ N) r
            ((↑(Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) : M ⧸ N) : M ⧸ N) =
          0 →
        r = 0),
    r • v ∈ N → r = 0
rwa₂ : ∀ (this : Eq (α := M ⧸ N) ((N.mkQ : (a : M) → M ⧸ N) (r • v) : M ⧸ N) (0 : M ⧸ N) → r = 0), r • v ∈ N → r = 0
⊢ r • v ∈ N → r = 0
have rwa₃ : ∀ (this : Eq (α := M ⧸ N) (Quotient.mk (r • v)) 0 → r = 0), r • v ∈ N → r = 0
Tactic: rwa [Finsupp.linearCombination_single, Finsupp.single_eq_zero, ← map_smul,
    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
N : Submodule R M
h : finrank.{u_1, u} R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank.{u_1, u} R (M ⧸ N)
hs' : LinearIndependent.{u, u_1, u} (ι := ↥s) R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s))
v : M
hv : Membership.mem (α := M ⧸ N) s ((N.mkQ : (a : M) → M ⧸ N) v : M ⧸ N)
r : R
hr : r ≠ 0
this :
  Eq.{u + 1} (α := M ⧸ N)
      ((Finsupp.linearCombination R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s)) : (a : ↥s →₀ R) → M ⧸ N)
          (Finsupp.single (Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) r) :
        M ⧸ N)
      (0 : M ⧸ N) →
    Eq (α := Finsupp.{u, u_1} (↥s) R)
      (Finsupp.single (Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) r :
        Finsupp.{u, u_1} (↥s) R)
      (0 : Finsupp.{u, u_1} (↥s) R)
rwa :
  ∀
    (this :
      HSMul.hSMul (β := M ⧸ N) r
            ((↑(Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) : M ⧸ N) : M ⧸ N) =
          0 →
        Eq (α := Finsupp.{u, u_1} (↥s) R)
          (Finsupp.single (Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) r :
            Finsupp.{u, u_1} (↥s) R)
          (0 : Finsupp.{u, u_1} (↥s) R)),
    r • v ∈ N → r = 0
rwa₁ :
  ∀
    (this :
      HSMul.hSMul (β := M ⧸ N) r
            ((↑(Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) : M ⧸ N) : M ⧸ N) =
          0 →
        r = 0),
    r • v ∈ N → r = 0
rwa₂ : ∀ (this : Eq (α := M ⧸ N) ((N.mkQ : (a : M) → M ⧸ N) (r • v) : M ⧸ N) (0 : M ⧸ N) → r = 0), r • v ∈ N → r = 0
rwa₃ : ∀ (this : Eq (α := M ⧸ N) (Quotient.mk (r • v)) 0 → r = 0), r • v ∈ N → r = 0
⊢ r • v ∈ N → r = 0
have rwa₄ : ∀ (this : r • v ∈ N → r = 0), r • v ∈ N → r = 0
Tactic: rwa [Finsupp.linearCombination_single, Finsupp.single_eq_zero, ← map_smul,
    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
s : Finset R
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
eval_f : ∀ x ∈ s, eval x f = 0
⊢ f = 0
have degree_f_lt₁ : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) f
Tactic: rw [← mem_degreeLT] at degree_f_lt
Cleared hypotheses: degree_f_lt, eval_f
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
s : Finset R
degree_f_lt : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) f
eval_f : ∀ x ∈ s, eval x f = 0
⊢ f = 0
have eval_f₁ : ∀ x ∈ s,
  Eq.{u_1 + 1} (α := R)
    (∑ i : Fin #s,
      HMul.hMul (α := R)
        ((degreeLTEquiv R #s : (a : ↥(degreeLT R #s)) → Fin #s → R)
            (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) x) f degree_f_lt)
            i :
          R)
        (x ^ (↑i : ℕ)))
    0
Tactic: simp_rw [eval_eq_sum_degreeLTEquiv degree_f_lt] at eval_f
Cleared hypotheses: eval_f
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
s : Finset R
degree_f_lt : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) f
eval_f :
  ∀ x ∈ s,
    Eq.{u_1 + 1} (α := R)
      (∑ i : Fin #s,
        HMul.hMul (α := R)
          ((degreeLTEquiv R #s : (a : ↥(degreeLT R #s)) → Fin #s → R)
              (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) x) f
                degree_f_lt)
              i :
            R)
          (x ^ (↑i : ℕ)))
      0
⊢ f = 0
have rw : Eq (α := Fin #s → R)
  ((degreeLTEquiv R #s : (a : ↥(degreeLT R #s)) → Fin #s → R)
      (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) x) f degree_f_lt) :
    Fin #s → R)
  (0 : Fin #s → R)
Tactic: rw [← degreeLTEquiv_eq_zero_iff_eq_zero degree_f_lt]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : (f - g).degree < (↑(#s) : WithBot ℕ)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f = g
have rw : f - g = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : (f - g).degree < (↑(#s) : WithBot ℕ)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f - g = 0
have refine : ∀ x ∈ s, eval x (f - g) = 0
Tactic: refine eq_zero_of_degree_lt_of_eval_finset_eq_zero _ degree_fg_lt ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
degree_g_lt : g.degree < (↑(#s) : WithBot ℕ)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f = g
have degree_f_lt₁ : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) f
Tactic: rw [← mem_degreeLT] at degree_f_lt degree_g_lt
Cleared hypotheses: degree_f_lt, degree_g_lt, eval_fg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
degree_g_lt : g.degree < (↑(#s) : WithBot ℕ)
eval_fg : ∀ x ∈ s, eval x f = eval x g
degree_f_lt₁ : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) f
⊢ f = g
have degree_g_lt₁ : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) g
Tactic: rw [← mem_degreeLT] at degree_f_lt degree_g_lt
Cleared hypotheses: degree_f_lt, degree_g_lt, eval_fg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) f
degree_g_lt : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) g
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f = g
have refine : (f - g).degree < (↑(#s) : WithBot ℕ)
Tactic: refine eq_of_degree_sub_lt_of_eval_finset_eq _ ?_ eval_fg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) f
degree_g_lt : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) g
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ (f - g).degree < (↑(#s) : WithBot ℕ)
have rw : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) (f - g)
Tactic: rw [← mem_degreeLT]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
s : Finset R
h_deg_le : f.degree ≤ (↑(#s) : WithBot ℕ)
h_deg_eq : f.degree = g.degree
hlc : f.leadingCoeff = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x f = eval x g
⊢ f = g
have inl : ∀ (h_deg_le : degree.{u_1} (R := R) 0 ≤ (↑(#s) : WithBot ℕ)) (h_deg_eq : degree.{u_1} (R := R) 0 = g.degree)
  (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ x ∈ s, eval x 0 = eval x g), 0 = g
Tactic: rcases eq_or_ne f 0 with rfl | hf
Cleared hypotheses: f, h_deg_le, h_deg_eq, hlc, h_eval
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
s : Finset R
h_deg_le : f.degree ≤ (↑(#s) : WithBot ℕ)
h_deg_eq : f.degree = g.degree
hlc : f.leadingCoeff = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x f = eval x g
inl :
  ∀ (h_deg_le : degree.{u_1} (R := R) 0 ≤ (↑(#s) : WithBot ℕ)) (h_deg_eq : degree.{u_1} (R := R) 0 = g.degree)
    (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ x ∈ s, eval x 0 = eval x g), 0 = g
⊢ f = g
have inr : ∀ (hf : f ≠ 0), f = g
Tactic: rcases eq_or_ne f 0 with rfl | hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
g : R[X]
s : Finset R
h_deg_le : degree.{u_1} (R := R) 0 ≤ (↑(#s) : WithBot ℕ)
h_deg_eq : degree.{u_1} (R := R) 0 = g.degree
hlc : leadingCoeff 0 = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x 0 = eval x g
⊢ 0 = g
have inl : ∀ (h_deg_eq : ⊥ = g.degree) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ x ∈ s, eval x 0 = eval x g), 0 = g
Tactic: rwa [degree_zero, eq_comm, degree_eq_bot, eq_comm] at h_deg_eq
Cleared hypotheses: h_deg_eq, hlc, h_eval
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
g : R[X]
s : Finset R
h_deg_le : degree.{u_1} (R := R) 0 ≤ (↑(#s) : WithBot ℕ)
h_deg_eq : degree.{u_1} (R := R) 0 = g.degree
hlc : leadingCoeff 0 = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x 0 = eval x g
inl : ∀ (h_deg_eq : ⊥ = g.degree) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ x ∈ s, eval x 0 = eval x g), 0 = g
⊢ 0 = g
have inl₁ : ∀ (h_deg_eq : g.degree = ⊥) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ x ∈ s, eval x 0 = eval x g), 0 = g
Tactic: rwa [degree_zero, eq_comm, degree_eq_bot, eq_comm] at h_deg_eq
Cleared hypotheses: h_deg_eq, hlc, h_eval
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
g : R[X]
s : Finset R
h_deg_le : degree.{u_1} (R := R) 0 ≤ (↑(#s) : WithBot ℕ)
h_deg_eq : degree.{u_1} (R := R) 0 = g.degree
hlc : leadingCoeff 0 = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x 0 = eval x g
inl : ∀ (h_deg_eq : ⊥ = g.degree) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ x ∈ s, eval x 0 = eval x g), 0 = g
inl₁ :
  ∀ (h_deg_eq : g.degree = ⊥) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ x ∈ s, eval x 0 = eval x g), 0 = g
⊢ 0 = g
have inl₂ : ∀ (h_deg_eq : g = 0) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ x ∈ s, eval x 0 = eval x g), 0 = g
Tactic: rwa [degree_zero, eq_comm, degree_eq_bot, eq_comm] at h_deg_eq
Cleared hypotheses: h_deg_eq, hlc, h_eval
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
g : R[X]
s : Finset R
h_deg_le : degree.{u_1} (R := R) 0 ≤ (↑(#s) : WithBot ℕ)
h_deg_eq : degree.{u_1} (R := R) 0 = g.degree
hlc : leadingCoeff 0 = g.leadingCoeff
h_eval : ∀ x ∈ s, eval x 0 = eval x g
inl : ∀ (h_deg_eq : ⊥ = g.degree) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ x ∈ s, eval x 0 = eval x g), 0 = g
inl₁ :
  ∀ (h_deg_eq : g.degree = ⊥) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ x ∈ s, eval x 0 = eval x g), 0 = g
inl₂ : ∀ (h_deg_eq : g = 0) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ x ∈ s, eval x 0 = eval x g), 0 = g
⊢ 0 = g
have inl₃ : ∀ (h_deg_eq : 0 = g) (hlc : leadingCoeff 0 = g.leadingCoeff) (h_eval : ∀ x ∈ s, eval x 0 = eval x g), 0 = g
Tactic: rwa [degree_zero, eq_comm, degree_eq_bot, eq_comm] at h_deg_eq
Cleared hypotheses: h_deg_eq, hlc, h_eval
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
eval_f : ∀ i ∈ s, eval (v i) f = 0
⊢ f = 0
have degree_f_lt₁ : f.degree < (↑(#(image v s)) : WithBot ℕ)
Tactic: rw [← card_image_of_injOn hvs] at degree_f_lt
Cleared hypotheses: degree_f_lt, eval_f
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#(image v s)) : WithBot ℕ)
eval_f : ∀ i ∈ s, eval (v i) f = 0
⊢ f = 0
have refine : ∀ x ∈ image v s, eval x f = 0
Tactic: refine eq_zero_of_degree_lt_of_eval_finset_eq_zero _ degree_f_lt ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#(image v s)) : WithBot ℕ)
eval_f : ∀ i ∈ s, eval (v i) f = 0
x : R
hx : x ∈ image v s
⊢ eval x f = 0
have rcases : ∀ (w : ι) (hj : w ∈ s) (hx : v w ∈ image v s), eval (v w) f = 0
Tactic: rcases mem_image.mp hx with ⟨_, hj, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
eval_f : ∀ i ∈ s, eval (v i) f = 0
⊢ f = 0
have rw : ∀ (degree_f_lt : f.degree < (↑(#(image v s)) : WithBot ℕ)) (eval_f : ∀ i ∈ s, eval (v i) f = 0), f = 0
Tactic: classical
    rw [← card_image_of_injOn hvs] at degree_f_lt
    refine eq_zero_of_degree_lt_of_eval_finset_eq_zero _ degree_f_lt ?_
    intro x hx
    rcases mem_image.mp hx with ⟨_, hj, rfl⟩
    exact eval_f _ hj
Cleared hypotheses: degree_f_lt, eval_f
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
eval_f : ∀ i ∈ s, eval (v i) f = 0
rw rw₁ rw₂ : ∀ (degree_f_lt : f.degree < (↑(#(image v s)) : WithBot ℕ)) (eval_f : ∀ i ∈ s, eval (v i) f = 0), f = 0
⊢ f = 0
have rw₃ : ∀ (degree_f_lt : f.degree < (↑(#(image v s)) : WithBot ℕ)) (eval_f : ∀ i ∈ s, eval (v i) f = 0),
  ∀ x ∈ image v s, eval x f = 0
Tactic: classical
    rw [← card_image_of_injOn hvs] at degree_f_lt
    refine eq_zero_of_degree_lt_of_eval_finset_eq_zero _ degree_f_lt ?_
    intro x hx
    rcases mem_image.mp hx with ⟨_, hj, rfl⟩
    exact eval_f _ hj
Cleared hypotheses: degree_f_lt, eval_f
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
eval_f : ∀ i ∈ s, eval (v i) f = 0
rw rw₁ rw₂ : ∀ (degree_f_lt : f.degree < (↑(#(image v s)) : WithBot ℕ)) (eval_f : ∀ i ∈ s, eval (v i) f = 0), f = 0
rw₃ rw₄ :
  ∀ (degree_f_lt : f.degree < (↑(#(image v s)) : WithBot ℕ)) (eval_f : ∀ i ∈ s, eval (v i) f = 0) (x : R)
    (hx : x ∈ image v s), eval x f = 0
⊢ f = 0
have rw₅ : ∀ (degree_f_lt : f.degree < (↑(#(image v s)) : WithBot ℕ)) (eval_f : ∀ i ∈ s, eval (v i) f = 0) (w : ι) (hj : w ∈ s)
  (hx : v w ∈ image v s), eval (v w) f = 0
Tactic: classical
    rw [← card_image_of_injOn hvs] at degree_f_lt
    refine eq_zero_of_degree_lt_of_eval_finset_eq_zero _ degree_f_lt ?_
    intro x hx
    rcases mem_image.mp hx with ⟨_, hj, rfl⟩
    exact eval_f _ hj
Cleared hypotheses: degree_f_lt, eval_f
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_fg_lt : (f - g).degree < (↑(#s) : WithBot ℕ)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f = g
have rw : f - g = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_fg_lt : (f - g).degree < (↑(#s) : WithBot ℕ)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f - g = 0
have refine : ∀ i ∈ s, eval (v i) (f - g) = 0
Tactic: refine eq_zero_of_degree_lt_of_eval_index_eq_zero _ hvs degree_fg_lt ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
degree_g_lt : g.degree < (↑(#s) : WithBot ℕ)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ f = g
have refine : (f - g).degree < (↑(#s) : WithBot ℕ)
Tactic: refine eq_of_degree_sub_lt_of_eval_index_eq _ hvs ?_ eval_fg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v (↑s : Set ι)
degree_f_lt : f.degree < (↑(#s) : WithBot ℕ)
degree_g_lt : g.degree < (↑(#s) : WithBot ℕ)
eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g
⊢ (f - g).degree < (↑(#s) : WithBot ℕ)
have rw : ∀ (degree_f_lt : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) f)
  (degree_g_lt : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) g)
  (eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g), Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) (f - g)
Tactic: rw [← mem_degreeLT] at degree_f_lt degree_g_lt ⊢
Cleared hypotheses: degree_f_lt, degree_g_lt, eval_fg