awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_2} R
inst_4 : StrongRankCondition R
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
N : Type u_1
inst_7 : AddCommGroup N
inst_8 : Module R N
L : Submodule R M
inst_9 : Module.Finite.{u_2, u} R ↥L
f : M →ₗ[R] N
h : finrank.{u_2, u} R ↥L ≤ finrank.{u_2, u_1} R ↥(map f L)
⊢ Disjoint L f.ker

Tactic:
disjoint_iff.mpr <| LinearMap.injective_domRestrict_iff.mp <| LinearMap.ker_eq_bot.mp <|
    Submodule.rank_eq_zero.mp ?_

Premises used: Iff.mpr, LinearMap.ker_eq_bot, disjoint_iff, Submodule.rank_eq_zero, Iff.mp, LinearMap.injective_domRestrict_iff
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_2} R
inst_4 : StrongRankCondition R
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
N : Type u_1
inst_7 : AddCommGroup N
inst_8 : Module R N
L : Submodule R M
inst_9 : Module.Finite.{u_2, u} R ↥L
f : M →ₗ[R] N
h : finrank.{u_2, u} R ↥L ≤ finrank.{u_2, u_1} R ↥(map f L)
refine : Module.rank R ↥(f.domRestrict L).ker = 0
⊢ Disjoint L f.ker

Tactic:
refine disjoint_iff.mpr <| LinearMap.injective_domRestrict_iff.mp <| LinearMap.ker_eq_bot.mp <|
    Submodule.rank_eq_zero.mp ?_

Premises used: Iff.mpr, LinearMap.ker_eq_bot, disjoint_iff, Submodule.rank_eq_zero, Iff.mp, LinearMap.injective_domRestrict_iff
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_2} R
inst_4 : StrongRankCondition R
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
N : Type u_1
inst_7 : AddCommGroup N
inst_8 : Module R N
L : Submodule R M
inst_9 : Module.Finite.{u_2, u} R ↥L
f : M →ₗ[R] N
h : finrank.{u_2, u} R ↥L ≤ finrank.{u_2, u_1} R ↥(map f L)
rw : finrank.{u_2, u} R ↥(f.domRestrict L).ker = 0
⊢ Module.rank R ↥(f.domRestrict L).ker = 0

Tactic:
rw [← Submodule.finrank_eq_rank, Nat.cast_eq_zero]

Premises used: Submodule.finrank_eq_rank, Nat.cast_eq_zero
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_2} R
inst_4 : StrongRankCondition R
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
N : Type u_1
inst_7 : AddCommGroup N
inst_8 : Module R N
L : Submodule R M
inst_9 : Module.Finite.{u_2, u} R ↥L
f : M →ₗ[R] N
h : finrank.{u_2, u} R ↥L ≤ finrank.{u_2, u_1} R ↥(map f L)
⊢ finrank.{u_2, u} R ↥L ≤ finrank.{u_2, u_1} R ↥(f.domRestrict L).range

Tactic:
rw [← LinearMap.range_domRestrict] at h

Premises used: LinearMap.range_domRestrict
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_2} R
inst_4 : StrongRankCondition R
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
N : Type u_1
inst_7 : AddCommGroup N
inst_8 : Module R N
L : Submodule R M
inst_9 : Module.Finite.{u_2, u} R ↥L
f : M →ₗ[R] N
h : finrank.{u_2, u} R ↥L ≤ finrank.{u_2, u_1} R ↥(f.domRestrict L).range
⊢ finrank.{u_2, u} R (↥L ⧸ (f.domRestrict L).ker) + finrank.{u_2, u} R ↥(f.domRestrict L).ker = finrank.{u_2, u} R ↥L

Tactic:
have := (LinearMap.ker (f.domRestrict L)).finrank_quotient_add_finrank
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_2} R
inst_4 : StrongRankCondition R
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
N : Type u_1
inst_7 : AddCommGroup N
inst_8 : Module R N
L : Submodule R M
inst_9 : Module.Finite.{u_2, u} R ↥L
f : M →ₗ[R] N
h : finrank.{u_2, u} R ↥L ≤ finrank.{u_2, u_1} R ↥(f.domRestrict L).range
this :
  finrank.{u_2, u} R (↥L ⧸ (f.domRestrict L).ker) + finrank.{u_2, u} R ↥(f.domRestrict L).ker = finrank.{u_2, u} R ↥L
⊢ finrank.{u_2, u_1} R ↥(f.domRestrict L).range + finrank.{u_2, u} R ↥(f.domRestrict L).ker = finrank.{u_2, u} R ↥L

Tactic:
rw [LinearEquiv.finrank_eq (f.domRestrict L).quotKerEquivRange] at this

Premises used: LinearEquiv.finrank_eq, LinearMap.domRestrict, LinearMap.quotKerEquivRange
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_2} R
inst_4 : StrongRankCondition R
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
N : Type u_1
inst_7 : AddCommGroup N
inst_8 : Module R N
L : Submodule R M
inst_9 : Module.Finite.{u_2, u} R ↥L
f : M →ₗ[R] N
h : finrank.{u_2, u} R ↥L ≤ finrank.{u_2, u_1} R ↥(f.domRestrict L).range
this : finrank.{u_2, u_1} R ↥(f.domRestrict L).range + finrank.{u_2, u} R ↥(f.domRestrict L).ker = finrank.{u_2, u} R ↥L
⊢ finrank.{u_2, u} R ↥(f.domRestrict L).ker = 0

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
obtain :
  ∀ (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))),
    ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N
⊢ ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
obtain ⟨s, hs, hs'⟩ :=
    exists_finset_linearIndependent_of_le_finrank (R := R) (M := M ⧸ N) le_rfl

Premises used: le_rfl, exists_finset_linearIndependent_of_le_finrank
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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))
rwa : s ≠ ∅
rwa₁ : ¬s = ∅
rwa₂ : ¬s.card = 0
rwa₃ : ¬finrank.{u_1, u} R (M ⧸ N) = 0
rwa₄ : ¬finrank R M - finrank.{u_1, u} R ↥N = 0
rwa₅ : ¬finrank R M ≤ finrank.{u_1, u} R ↥N
rwa₆ rwa₇ rwa₈ rwa₉ : finrank.{u_1, u} R ↥N < finrank R M
⊢ s.Nonempty

Tactic:
rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero,
    hs, finrank_quotient, tsub_eq_zero_iff_le, not_le]

Premises used: not_le, Finset.nonempty_iff_ne_empty, tsub_eq_zero_iff_le, ne_eq, Finset.card_eq_zero, Submodule.finrank_quotient
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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))
obtain : ∀ (v : M ⧸ N) (hv : v ∈ s), ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N
⊢ ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
obtain ⟨v, hv⟩ : s.Nonempty := by rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero,
    hs, finrank_quotient, tsub_eq_zero_iff_le, not_le]

Premises used: Finset.Nonempty
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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 ⧸ N
hv : v ∈ s
obtain :
  ∀ (v : M) (hv : Membership.mem (α := M ⧸ N) s ((N.mkQ : (a : M) → M ⧸ N) v : M ⧸ N)),
    ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N
⊢ ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
obtain ⟨v, rfl⟩ := N.mkQ_surjective v

Premises used: Submodule.mkQ_surjective, rfl
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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)
⊢ ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
⟨v, fun r hr ↦ mt ?_ hr⟩

Premises used: mt, Exists.intro
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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)
refine : ∀ (r : R) (hr : r ≠ 0), r • v ∈ N → r = 0
⊢ ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
refine ⟨v, fun r hr ↦ mt ?_ hr⟩
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
⊢ 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)

Tactic:
have := linearIndependent_iff.mp hs' (Finsupp.single ⟨_, hv⟩ r)
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (this : r • v ∈ N → r = 0), 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

Premises used: Finsupp.single_eq_zero, Submodule.mkQ_apply, Finsupp.linearCombination_single, Submodule.Quotient.mk_eq_zero, map_smul
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) f

Tactic:
rw [← mem_degreeLT] at degree_f_lt

Premises used: Polynomial.mem_degreeLT
-- Module: Mathlib.LinearAlgebra.Lagrange
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
degree_f_lt₁ : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) f
⊢ ∀ x ∈ s, eval x f = 0

Tactic:
rw [← mem_degreeLT] at degree_f_lt

Premises used: Polynomial.mem_degreeLT
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ ∀ 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

Premises used: Polynomial.eval_eq_sum_degreeLTEquiv
-- Module: Mathlib.LinearAlgebra.Lagrange
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
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)
⊢ f = 0

Tactic:
rw [← degreeLTEquiv_eq_zero_iff_eq_zero degree_f_lt]

Premises used: Polynomial.degreeLTEquiv_eq_zero_iff_eq_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ 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:
Matrix.eq_zero_of_forall_index_sum_mul_pow_eq_zero
      (Injective.comp (Embedding.subtype _).inj' (equivFinOfCardEq (card_coe _)).symm.injective)
      fun _ => eval_f _ (Finset.coe_mem _)

Premises used: Finset.coe_mem, Fintype.equivFinOfCardEq, Function.comp, Membership.mem, Function.Embedding.inj', Matrix.eq_zero_of_forall_index_sum_mul_pow_eq_zero, Function.Injective.comp, Function.Embedding.subtype, Equiv.injective, Function.Embedding.toFun, Equiv.symm, DFunLike.coe, Fintype.card_coe
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ 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:
exact
    Matrix.eq_zero_of_forall_index_sum_mul_pow_eq_zero
      (Injective.comp (Embedding.subtype _).inj' (equivFinOfCardEq (card_coe _)).symm.injective)
      fun _ => eval_f _ (Finset.coe_mem _)

Premises used: Finset.coe_mem, Fintype.equivFinOfCardEq, Function.comp, Membership.mem, Function.Embedding.inj', Matrix.eq_zero_of_forall_index_sum_mul_pow_eq_zero, Function.Injective.comp, Function.Embedding.subtype, Equiv.injective, Function.Embedding.toFun, Equiv.symm, DFunLike.coe, Fintype.card_coe
-- Module: Mathlib.LinearAlgebra.Lagrange
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
rw : f - g = 0
⊢ f = g

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
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

Tactic:
eq_zero_of_degree_lt_of_eval_finset_eq_zero _ degree_fg_lt ?_

Premises used: Polynomial.eq_zero_of_degree_lt_of_eval_finset_eq_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
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
refine : ∀ x ∈ s, eval x (f - g) = 0
⊢ f - g = 0

Tactic:
refine eq_zero_of_degree_lt_of_eval_finset_eq_zero _ degree_fg_lt ?_

Premises used: Polynomial.eq_zero_of_degree_lt_of_eval_finset_eq_zero
-- Module: Mathlib.LinearAlgebra.Lagrange
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
simp_rw : ∀ x ∈ s, eval x f = eval x g
⊢ ∀ x ∈ s, eval x (f - g) = 0

Tactic:
simp_rw [eval_sub, sub_eq_zero]

Premises used: sub_eq_zero, Polynomial.eval_sub
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ ∀ x ∈ s, eval x f = eval x g

Tactic:
eval_fg
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ ∀ x ∈ s, eval x f = eval x g

Tactic:
exact eval_fg
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) f

Tactic:
rw [← mem_degreeLT] at degree_f_lt degree_g_lt

Premises used: Polynomial.mem_degreeLT
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) g

Tactic:
rw [← mem_degreeLT] at degree_f_lt degree_g_lt

Premises used: Polynomial.mem_degreeLT
-- Module: Mathlib.LinearAlgebra.Lagrange
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
degree_g_lt₁ : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) g
⊢ ∀ x ∈ s, eval x f = eval x g

Tactic:
rw [← mem_degreeLT] at degree_f_lt degree_g_lt

Premises used: Polynomial.mem_degreeLT
-- Module: Mathlib.LinearAlgebra.Lagrange
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

Tactic:
eq_of_degree_sub_lt_of_eval_finset_eq _ ?_ eval_fg

Premises used: Polynomial.eq_of_degree_sub_lt_of_eval_finset_eq
-- Module: Mathlib.LinearAlgebra.Lagrange
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
refine : (f - g).degree < (↑(#s) : WithBot ℕ)
⊢ f = g

Tactic:
refine eq_of_degree_sub_lt_of_eval_finset_eq _ ?_ eval_fg

Premises used: Polynomial.eq_of_degree_sub_lt_of_eval_finset_eq
-- Module: Mathlib.LinearAlgebra.Lagrange
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
rw : Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) (f - g)
⊢ (f - g).degree < (↑(#s) : WithBot ℕ)

Tactic:
rw [← mem_degreeLT]

Premises used: Polynomial.mem_degreeLT
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) (f - g)

Tactic:
Submodule.sub_mem _ degree_f_lt degree_g_lt

Premises used: Set.Mem, Submodule.sub_mem
-- Module: Mathlib.LinearAlgebra.Lagrange
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
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R #s) (f - g)

Tactic:
exact Submodule.sub_mem _ degree_f_lt degree_g_lt

Premises used: Submodule.sub_mem
-- Module: Mathlib.LinearAlgebra.Lagrange
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
inr : ∀ (hf : f ≠ 0), f = g
⊢ f = g

Tactic:
rcases eq_or_ne f 0 with rfl | hf

Premises used: eq_or_ne, OfNat.ofNat, rfl