awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
x : L
inst_9 : Nontrivial R
mp :
  Ne.{u_1 + 1} (α := R) (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) φ.nilRank) 0 →
    Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) = φ.nilRank
mpr :
  Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) = φ.nilRank →
    Ne.{u_1 + 1} (α := R) (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) φ.nilRank) 0
⊢ Ne.{u_1 + 1} (α := R) (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) φ.nilRank) 0 ↔
    Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) = φ.nilRank

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
x : L
inst_9 : Nontrivial R
h : Ne.{u_1 + 1} (α := R) (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) φ.nilRank) 0
⊢ Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) = φ.nilRank

Tactic:
le_antisymm
      (Polynomial.natTrailingDegree_le_of_ne_zero h)
      (nilRank_le_natTrailingDegree_charpoly φ x)

Premises used: le_antisymm, LinearMap.nilRank_le_natTrailingDegree_charpoly, Polynomial.natTrailingDegree_le_of_ne_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
x : L
inst_9 : Nontrivial R
h : Ne.{u_1 + 1} (α := R) (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) φ.nilRank) 0
⊢ Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) = φ.nilRank

Tactic:
exact le_antisymm
      (Polynomial.natTrailingDegree_le_of_ne_zero h)
      (nilRank_le_natTrailingDegree_charpoly φ x)

Premises used: le_antisymm, LinearMap.nilRank_le_natTrailingDegree_charpoly, Polynomial.natTrailingDegree_le_of_ne_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
x : L
inst_9 : Nontrivial R
h : Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) = φ.nilRank
mpr :
  Ne.{u_1 + 1} (α := R)
    (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))
      (Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))))
    0
⊢ Ne.{u_1 + 1} (α := R) (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) φ.nilRank) 0

Tactic:
rw [← h]
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
x : L
inst_9 : Nontrivial R
h : Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) = φ.nilRank
mpr : Ne.{u_1 + 1} (α := Polynomial R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) 0
⊢ Ne.{u_1 + 1} (α := R)
    (Polynomial.coeff (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))
      (Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x))))
    0

Tactic:
apply Polynomial.trailingCoeff_nonzero_iff_nonzero.mpr

Premises used: Iff.mpr, Polynomial.trailingCoeff_nonzero_iff_nonzero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
x : L
inst_9 : Nontrivial R
h : Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) = φ.nilRank
⊢ Ne.{u_1 + 1} (α := Polynomial R) (charpoly.{u_1, u_3} (M := M) ((φ : (a : L) → End R M) x)) 0

Tactic:
apply (LinearMap.charpoly_monic _).ne_zero

Premises used: LinearMap.charpoly_monic, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card.{u_3} (ChooseBasisIndex R M)
⊢ φ.nilRank + (n - φ.nilRank) = finrank R M

Tactic:
simp [n, nilRank_le_card φ bₘ, finrank_eq_card_chooseBasisIndex]

Premises used: Module.finrank_eq_card_chooseBasisIndex, LinearMap.nilRank_le_card
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card.{u_3} (ChooseBasisIndex R M)
⊢ ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)

Tactic:
have aux :
    ((polyCharpoly φ b).coeff (nilRank φ)).IsHomogeneous (n - nilRank φ) :=
    polyCharpoly_coeff_isHomogeneous _ b (nilRank φ) (n - nilRank φ)
      (by simp [n, nilRank_le_card φ bₘ, finrank_eq_card_chooseBasisIndex])
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card.{u_3} (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
by_contra! :
  ∀
    (h₀ :
      ∀ (r : ChooseBasisIndex R L → R),
        Eq.{u_1 + 1} (α := R)
          ((eval r : (a : MvPolynomial (ChooseBasisIndex R L) R) → R) ((φ.polyCharpoly b).coeff φ.nilRank) : R)
          (0 : R)),
    False
⊢ ∃ (r : ChooseBasisIndex R L → R),
    Ne.{u_1 + 1} (α := R)
      ((eval r : (a : MvPolynomial (ChooseBasisIndex R L) R) → R) ((φ.polyCharpoly b).coeff φ.nilRank) : R) (0 : R)

Tactic:
by_contra! h₀
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card.{u_3} (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
h₀ :
  ∀ (r : ChooseBasisIndex R L → R),
    Eq.{u_1 + 1} (α := R)
      ((eval r : (a : MvPolynomial (ChooseBasisIndex R L) R) → R) ((φ.polyCharpoly b).coeff φ.nilRank) : R) (0 : R)
apply : (φ.polyCharpoly b).coeff φ.nilRank = 0
⊢ False

Tactic:
apply polyCharpoly_coeff_nilRank_ne_zero φ b

Premises used: LinearMap.polyCharpoly_coeff_nilRank_ne_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card.{u_3} (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
h₀ :
  ∀ (r : ChooseBasisIndex R L → R),
    Eq.{u_1 + 1} (α := R)
      ((eval r : (a : MvPolynomial (ChooseBasisIndex R L) R) → R) ((φ.polyCharpoly b).coeff φ.nilRank) : R) (0 : R)
apply : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑(n - φ.nilRank) : Cardinal.{u_1}) (↑(finrank R M) : Cardinal.{u_1})
⊢ (φ.polyCharpoly b).coeff φ.nilRank = 0

Tactic:
apply aux.eq_zero_of_forall_eval_eq_zero_of_le_card h₀ (le_trans _ h)

Premises used: MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card, le_trans
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card.{u_3} (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
h₀ :
  ∀ (r : ChooseBasisIndex R L → R),
    Eq.{u_1 + 1} (α := R)
      ((eval r : (a : MvPolynomial (ChooseBasisIndex R L) R) → R) ((φ.polyCharpoly b).coeff φ.nilRank) : R) (0 : R)
⊢ LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑(n - φ.nilRank) : Cardinal.{u_1}) (↑(finrank R M) : Cardinal.{u_1})

Tactic:
simp only [n, finrank_eq_card_chooseBasisIndex, Nat.cast_le, Nat.sub_le]

Premises used: Nat.sub_le, Module.finrank_eq_card_chooseBasisIndex, Nat.cast_le
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card.{u_3} (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
obtain :
  ∀ (x : ChooseBasisIndex R L → R)
    (hx :
      Ne.{u_1 + 1} (α := R)
        ((eval x : (a : MvPolynomial (ChooseBasisIndex R L) R) → R) ((φ.polyCharpoly b).coeff φ.nilRank) : R) (0 : R)),
    ∃ (x : L), φ.IsNilRegular x
⊢ ∃ (x : L), φ.IsNilRegular x

Tactic:
obtain ⟨x, hx⟩ : ∃ r, eval r ((polyCharpoly _ b).coeff (nilRank φ)) ≠ 0 := by
    by_contra! h₀
    apply polyCharpoly_coeff_nilRank_ne_zero φ b
    apply aux.eq_zero_of_forall_eval_eq_zero_of_le_card h₀ (le_trans _ h)
    simp only [n, finrank_eq_card_chooseBasisIndex, Nat.cast_le, Nat.sub_le]
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card.{u_3} (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
x : ChooseBasisIndex R L → R
hx :
  Ne.{u_1 + 1} (α := R)
    ((eval x : (a : MvPolynomial (ChooseBasisIndex R L) R) → R) ((φ.polyCharpoly b).coeff φ.nilRank) : R) (0 : R)
c : Finsupp.{u_2, u_1} (ChooseBasisIndex R L) R :=
  (Equiv.symm Finsupp.equivFunOnFinite : (a : ChooseBasisIndex R L → R) → ChooseBasisIndex R L →₀ R) x
h₁ : φ.IsNilRegular ((b.repr.symm : (a : ChooseBasisIndex R L →₀ R) → L) c)
⊢ ∃ (x : L), φ.IsNilRegular x

Tactic:
use b.repr.symm c

Premises used: LinearEquiv.symm, Module.Basis.repr, DFunLike.coe
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card.{u_3} (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
x : ChooseBasisIndex R L → R
hx :
  Ne.{u_1 + 1} (α := R)
    ((eval x : (a : MvPolynomial (ChooseBasisIndex R L) R) → R) ((φ.polyCharpoly b).coeff φ.nilRank) : R) (0 : R)
c : Finsupp.{u_2, u_1} (ChooseBasisIndex R L) R :=
  (Equiv.symm Finsupp.equivFunOnFinite : (a : ChooseBasisIndex R L → R) → ChooseBasisIndex R L →₀ R) x
h₁ :
  Ne.{u_1 + 1} (α := R)
    ((eval
            (⇑((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) ((b.repr.symm : (a : ChooseBasisIndex R L →₀ R) → L) c) :
                  Finsupp.{u_2, u_1} (ChooseBasisIndex R L) R) :
              (a : ChooseBasisIndex R L) → R) :
          (a : MvPolynomial (ChooseBasisIndex R L) R) → R)
        ((φ.polyCharpoly b).coeff φ.nilRank) :
      R)
    (0 : R)
h₂ h₃ h₄ h₅ :
  Ne.{u_1 + 1} (α := R)
    ((eval (⇑c : (a : ChooseBasisIndex R L) → R) : (a : MvPolynomial (ChooseBasisIndex R L) R) → R)
        ((φ.polyCharpoly b).coeff φ.nilRank) :
      R)
    (0 : R)
⊢ φ.IsNilRegular ((b.repr.symm : (a : ChooseBasisIndex R L →₀ R) → L) c)

Tactic:
rwa [isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero _ b, LinearEquiv.apply_symm_apply]

Premises used: LinearMap.isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero, LinearEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
inst_10 : Infinite R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ Cardinal.mk R
⊢ ∃ (x : L), φ.IsNilRegular x

Tactic:
apply exists_isNilRegular_of_finrank_le_card

Premises used: LinearMap.exists_isNilRegular_of_finrank_le_card
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
inst_10 : Infinite R
⊢ (↑(finrank R M) : Cardinal.{u_1}) ≤ Cardinal.mk R

Tactic:
Cardinal.natCast_le_aleph0.trans <| Cardinal.infinite_iff.mp ‹Infinite R›

Premises used: Cardinal.infinite_iff, Iff.mp, LE.le.trans, Cardinal.natCast_le_aleph0
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
inst_10 : Infinite R
⊢ (↑(finrank R M) : Cardinal.{u_1}) ≤ Cardinal.mk R

Tactic:
exact Cardinal.natCast_le_aleph0.trans <| Cardinal.infinite_iff.mp ‹Infinite R›

Premises used: Cardinal.infinite_iff, Iff.mp, LE.le.trans, Cardinal.natCast_le_aleph0
-- Module: Mathlib.Algebra.Module.LinearMap.Prod
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
map_add : ∀ (x y : M × M), (x + y).1 + (x + y).2 = x.1 + x.2 + (y.1 + y.2)
map_smul : ∀ (c : R) (x : M × M), (c • x).1 + (c • x).2 = c • (x.1 + x.2)
⊢ IsLinearMap R (M₂ := M) fun (x : M × M) ↦ x.1 + x.2

Tactic:
apply IsLinearMap.mk

Premises used: IsLinearMap.mk
-- Module: Mathlib.Algebra.Module.LinearMap.Prod
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M × M
map_add : x.1 + y.1 + (x.2 + y.2) = x.1 + x.2 + (y.1 + y.2)
⊢ (x + y).1 + (x + y).2 = x.1 + x.2 + (y.1 + y.2)

Tactic:
simp only [Prod.fst_add, Prod.snd_add]

Premises used: Prod.fst_add, Prod.snd_add
-- Module: Mathlib.Algebra.Module.LinearMap.Prod
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M × M
⊢ x.1 + y.1 + (x.2 + y.2) = x.1 + x.2 + (y.1 + y.2)

Tactic:
abel
-- Module: Mathlib.Algebra.Module.LinearMap.Prod
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ ∀ (c : R) (x : M × M), (c • x).1 + (c • x).2 = c • (x.1 + x.2)

Tactic:
simp [smul_add]

Premises used: smul_add
-- Module: Mathlib.Algebra.Module.LinearMap.Prod
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
map_add : ∀ (x y : M × M), (x + y).1 - (x + y).2 = x.1 - x.2 + (y.1 - y.2)
map_smul : ∀ (c : R) (x : M × M), (c • x).1 - (c • x).2 = c • (x.1 - x.2)
⊢ IsLinearMap R (M₂ := M) fun (x : M × M) ↦ x.1 - x.2

Tactic:
apply IsLinearMap.mk

Premises used: IsLinearMap.mk
-- Module: Mathlib.Algebra.Module.LinearMap.Prod
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ ∀ (x y : M × M), (x + y).1 - (x + y).2 = x.1 - x.2 + (y.1 - y.2)

Tactic:
simp [add_comm, add_assoc, add_left_comm, sub_eq_add_neg]

Premises used: add_left_comm, add_assoc, sub_eq_add_neg, add_comm
-- Module: Mathlib.Algebra.Module.LinearMap.Prod
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ ∀ (c : R) (x : M × M), (c • x).1 - (c • x).2 = c • (x.1 - x.2)

Tactic:
simp [smul_sub]

Premises used: smul_sub
-- Module: Mathlib.Algebra.Module.LinearMap.Rat
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommGroup M
inst_1 : Module ℚ M
inst_2 : AddCommGroup M₂
inst_3 : Module ℚ M₂
f g : M →+ M₂
h : Eq (α := M →ₗ[ℚ] M₂) f.toRatLinearMap g.toRatLinearMap
h₁ : ∀ (x : M), Eq.{u_2 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) x : M₂)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.LinearMap.Rat
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommGroup M
inst_1 : Module ℚ M
inst_2 : AddCommGroup M₂
inst_3 : Module ℚ M₂
f g : M →+ M₂
h : Eq (α := M →ₗ[ℚ] M₂) f.toRatLinearMap g.toRatLinearMap
x : M
⊢ Eq.{u_2 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) x : M₂)

Tactic:
LinearMap.congr_fun h x

Premises used: LinearMap.congr_fun
-- Module: Mathlib.Algebra.Module.LinearMap.Rat
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommGroup M
inst_1 : Module ℚ M
inst_2 : AddCommGroup M₂
inst_3 : Module ℚ M₂
f g : M →+ M₂
h : Eq (α := M →ₗ[ℚ] M₂) f.toRatLinearMap g.toRatLinearMap
x : M
⊢ Eq.{u_2 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) x : M₂)

Tactic:
exact LinearMap.congr_fun h x

Premises used: LinearMap.congr_fun
-- Module: Mathlib.Algebra.Module.LinearMap.Rat
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommGroup M
inst_1 : Module ℚ M
inst_2 : AddCommGroup M₂
inst_3 : Module ℚ M₂
f : M →+ M₂
⊢ Eq (α := (a : M) → M₂) (⇑f.toRatLinearMap : (a : M) → M₂) (⇑f : (a : M) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : ∀ (a b : Prod.{v, u} M ↥S), (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) a b ↔ r S M a b
⊢ (⇑(OreLocalization.oreEqv S M) : M × ↥S → M × ↥S → Prop) = r S M

Tactic:
ext a b
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
h : (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) a b → r S M a b
h₁ : r S M a b → (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) a b
⊢ (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) a b ↔ r S M a b

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : (↑u : R) * (↑b.2 : R) = v * (↑a.2 : R)
h : u • b.2 • a.1 = u • a.2 • b.1
⊢ r S M a b

Tactic:
use u
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : (↑u : R) * (↑b.2 : R) = v * (↑a.2 : R)
h : (v * (↑a.2 : R)) • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
⊢ u • b.2 • a.1 = u • a.2 • b.1

Tactic:
simp only [Submonoid.smul_def, smul_smul, h₂]

Premises used: smul_smul, Submonoid.smul_def
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : (↑u : R) * (↑b.2 : R) = v * (↑a.2 : R)
h : ((↑a.2 : R) * v) • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
h₃ : (↑a.2 : R) • v • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
h₄ : (↑a.2 : R) • u • b.1 = ((↑u : R) * (↑a.2 : R)) • b.1
h₅ : (↑a.2 : R) • u • b.1 = ((↑a.2 : R) * (↑u : R)) • b.1
h₆ : (↑a.2 : R) • u • b.1 = (↑a.2 : R) • (↑u : R) • b.1
h₇ h₈ : (↑a.2 : R) • (↑u : R) • b.1 = (↑a.2 : R) • (↑u : R) • b.1
⊢ (v * (↑a.2 : R)) • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1

Tactic:
rw [mul_comm, mul_smul, ← h₁, mul_comm, mul_smul, Submonoid.smul_def]

Premises used: Submonoid.smul_def, mul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
u : ↥S
hu : u • b.2 • a.1 = u • a.2 • b.1
h : (u * a.2) • b.1 = ((↑u : R) * (↑b.2 : R)) • a.1 ∧ (↑(u * a.2) : R) * (↑b.2 : R) = (↑u : R) * (↑b.2 : R) * (↑a.2 : R)
⊢ (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) a b

Tactic:
use u * a.2, u * b.2

Premises used: Prod.snd