awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
inst_1 : Nontrivial R
⊢ degree.{u_1} (R := R)
      (∑ x : Fin E.order,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (E.coeffs x) : R[X]) (HPow.hPow (α := R[X]) X (↑x : ℕ))) <
    (↑E.order : WithBot ℕ)

Tactic:
degree_sum_fin_lt E.coeffs

Premises used: LinearRecurrence.coeffs, Polynomial.degree_sum_fin_lt
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
inst_1 : Nontrivial R
⊢ degree.{u_1} (R := R)
      (∑ x : Fin E.order,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (E.coeffs x) : R[X]) (HPow.hPow (α := R[X]) X (↑x : ℕ))) <
    (↑E.order : WithBot ℕ)

Tactic:
exact degree_sum_fin_lt E.coeffs

Premises used: LinearRecurrence.coeffs, Polynomial.degree_sum_fin_lt
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
h : Nontrivial R
rw : Eq.{u_1 + 1} (α := R) (∑ b : Fin E.order, coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (E.coeffs b)) E.order) 0
⊢ E.charPoly.Monic

Tactic:
rw [Monic, leadingCoeff, natDegree_eq_of_degree_eq_some <| charPoly_degree_eq_order _, charPoly,
    coeff_sub, coeff_monomial_same, finsetSum_coeff, sub_eq_self]

Premises used: Polynomial.finsetSum_coeff, Polynomial.leadingCoeff, sub_eq_self, Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.Monic, Polynomial.coeff_monomial_same, LinearRecurrence.charPoly_degree_eq_order, Polynomial.coeff_sub, LinearRecurrence.charPoly
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
h : Nontrivial R
⊢ Eq.{u_1 + 1} (α := R) (∑ b : Fin E.order, coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (E.coeffs b)) E.order) 0

Tactic:
sum_eq_zero fun _ _ ↦ coeff_eq_zero_of_degree_lt ?_

Premises used: Finset.sum_eq_zero, Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
h : Nontrivial R
refine :
  ∀ (x : Fin E.order),
    Membership.mem (γ := Finset (Fin E.order)) univ x →
      degree.{u_1} (R := R) ((monomial (↑x : ℕ) : (a : R) → R[X]) (E.coeffs x)) < (↑E.order : WithBot ℕ)
⊢ Eq.{u_1 + 1} (α := R) (∑ b : Fin E.order, coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (E.coeffs b)) E.order) 0

Tactic:
refine sum_eq_zero fun _ _ ↦ coeff_eq_zero_of_degree_lt ?_

Premises used: Finset.sum_eq_zero, Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
h : Nontrivial R
x : Fin E.order
h_1 : Membership.mem (γ := Finset (Fin E.order)) univ x
grw : LT.lt (α := WithBot ℕ) (↑(↑x : ℕ) : WithBot ℕ) (↑E.order : WithBot ℕ)
⊢ degree.{u_1} (R := R) ((monomial (↑x : ℕ) : (a : R) → R[X]) (E.coeffs x)) < (↑E.order : WithBot ℕ)

Tactic:
grw [degree_monomial_le]

Premises used: Polynomial.degree_monomial_le
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
h : Nontrivial R
x : Fin E.order
h_1 : Membership.mem (γ := Finset (Fin E.order)) univ x
⊢ LT.lt (α := WithBot ℕ) (↑(↑x : ℕ) : WithBot ℕ) (↑E.order : WithBot ℕ)

Tactic:
simp
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
q : R
simp : (E.IsSolution fun (n : ℕ) ↦ q ^ n) ↔ q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ (↑x : ℕ) = 0
⊢ (E.IsSolution fun (n : ℕ) ↦ q ^ n) ↔
    eval₂ (RingHom.id R) q
        (HSub.hSub (α := R[X]) ((monomial E.order : (a : R) → R[X]) 1)
          (∑ i : Fin E.order, (monomial (↑i : ℕ) : (a : R) → R[X]) (E.coeffs i))) =
      0

Tactic:
simp only [Polynomial.eval₂_finsetSum, one_mul, RingHom.id_apply, Polynomial.eval₂_monomial,
    Polynomial.eval₂_sub]

Premises used: RingHom.id_apply, Polynomial.eval₂_monomial, Polynomial.eval₂_sub, Polynomial.eval₂_finsetSum, one_mul
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
q : R
mp : (E.IsSolution fun (n : ℕ) ↦ q ^ n) → q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ (↑x : ℕ) = 0
mpr : q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ (↑x : ℕ) = 0 → E.IsSolution fun (n : ℕ) ↦ q ^ n
⊢ (E.IsSolution fun (n : ℕ) ↦ q ^ n) ↔ q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ (↑x : ℕ) = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
q : R
h : E.IsSolution fun (n : ℕ) ↦ q ^ n
⊢ q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ (↑x : ℕ) = 0

Tactic:
simpa [sub_eq_zero] using h 0

Premises used: sub_eq_zero, OfNat.ofNat
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
q : R
h : q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ (↑x : ℕ) = 0
n : ℕ
mpr :
  Eq.{u_1 + 1} (α := R) (∑ i : Fin E.order, q ^ n * (E.coeffs i * q ^ (↑i : ℕ)))
    (∑ x : Fin E.order, E.coeffs x * (q ^ n * q ^ (↑x : ℕ)))
⊢ Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ q ^ n) (n + E.order))
    (∑ i : Fin E.order, E.coeffs i * (fun (n : ℕ) ↦ q ^ n) (n + (↑i : ℕ)))

Tactic:
simp only [pow_add, sub_eq_zero.mp h, mul_sum]

Premises used: Finset.mul_sum, sub_eq_zero, pow_add, Iff.mp
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
q : R
h : q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ (↑x : ℕ) = 0
n : ℕ
x : Fin E.order
h_1 : Membership.mem (γ := Finset (Fin E.order)) univ x
⊢ q ^ n * (E.coeffs x * q ^ (↑x : ℕ)) = E.coeffs x * (q ^ n * q ^ (↑x : ℕ))

Tactic:
ring
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
q : R
h : q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ (↑x : ℕ) = 0
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (∑ i : Fin E.order, q ^ n * (E.coeffs i * q ^ (↑i : ℕ)))
    (∑ x : Fin E.order, E.coeffs x * (q ^ n * q ^ (↑x : ℕ)))

Tactic:
exact sum_congr rfl fun _ _ ↦ by ring

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Module.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
u : Rˣ
x : M
rw : (↑(-u) : R) • x = -(u • x)
rw₁ : -(↑u : R) • x = -(u • x)
rw₂ : -((↑u : R) • x) = -(u • x)
rw₃ rw₄ : -((↑u : R) • x) = -((↑u : R) • x)
⊢ -u • x = -(u • x)

Tactic:
rw [Units.smul_def, Units.val_neg, _root_.neg_smul, Units.smul_def]

Premises used: neg_smul, Units.val_neg, Units.smul_def
-- Module: Mathlib.Algebra.Module.Basic
Goal:
M : Type u_3
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
x : M
⊢ HSMul.hSMul.{u_5, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) x +
      HSMul.hSMul.{u_5, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) x =
    x

Tactic:
Convex.combo_self invOf_two_add_invOf_two _

Premises used: Convex.combo_self, invOf_two_add_invOf_two
-- Module: Mathlib.Algebra.Module.Basic
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
pos :
  ∀ (hR : Eq.{u_6 + 1} (α := R) (↑n : R) 0),
    (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
      HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
neg :
  ∀ (hR : ¬Eq.{u_6 + 1} (α := R) (↑n : R) 0),
    (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
      HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)

Tactic:
by_cases hR : (n : R) = 0

Premises used: Nat.cast
-- Module: Mathlib.Algebra.Module.Basic
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : Eq.{u_6 + 1} (α := R) (↑n : R) 0
pos :
  ∀ (hS : Eq.{u_7 + 1} (α := S) (↑n : S) 0),
    (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
      HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
neg :
  ∀ (hS : ¬Eq.{u_7 + 1} (α := S) (↑n : S) 0),
    (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
      HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)

Tactic:
by_cases hS : (n : S) = 0

Premises used: Nat.cast
-- Module: Mathlib.Algebra.Module.Basic
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : ¬Eq.{u_6 + 1} (α := R) (↑n : R) 0
pos :
  ∀ (hS : Eq.{u_7 + 1} (α := S) (↑n : S) 0),
    (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
      HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
neg :
  ∀ (hS : ¬Eq.{u_7 + 1} (α := S) (↑n : S) 0),
    (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
      HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)

Tactic:
by_cases hS : (n : S) = 0

Premises used: Nat.cast
-- Module: Mathlib.Algebra.Module.Basic
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : Eq.{u_7 + 1} (α := S) (↑n : S) 0
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)

Tactic:
simp [hR, hS, map_zero f]

Premises used: map_zero
-- Module: Mathlib.Algebra.Module.Basic
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : ¬Eq.{u_7 + 1} (α := S) (↑n : S) 0
this : ∀ (y : M), Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) y : M₂) (0 : M₂)
rw : 0 = HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
rw₁ : 0 = HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ 0
rw₂ rw₃ : Eq.{u_4 + 1} (α := M₂) 0 0
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)

Tactic:
rw [this, this, smul_zero]

Premises used: smul_zero
-- Module: Mathlib.Algebra.Module.Basic
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : ¬Eq.{u_7 + 1} (α := S) (↑n : S) 0
neg : ∀ (y : M), Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) y : M₂) (0 : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)

Tactic:
suffices ∀ y, f y = 0 by rw [this, this, smul_zero]
-- Module: Mathlib.Algebra.Module.Basic
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
hR : Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : ¬Eq.{u_7 + 1} (α := S) (↑n : S) 0
x : M
neg :
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹
      ((f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R) x) : M₂) =
    0
⊢ Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) (0 : M₂)

Tactic:
rw [← inv_smul_smul₀ hS (f x), ← map_natCast_smul f R S]

Premises used: inv_smul_smul₀, map_natCast_smul, DFunLike.coe
-- Module: Mathlib.Algebra.Module.Basic
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
hR : Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : ¬Eq.{u_7 + 1} (α := S) (↑n : S) 0
x : M
⊢ HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹
      ((f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R) x) : M₂) =
    0

Tactic:
simp [hR, map_zero f]

Premises used: map_zero
-- Module: Mathlib.Algebra.Module.Basic
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : ¬Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : Eq.{u_7 + 1} (α := S) (↑n : S) 0
this : ∀ (y : M), Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) y : M₂) (0 : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)

Tactic:
simp [this]
-- Module: Mathlib.Algebra.Module.Basic
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : ¬Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : Eq.{u_7 + 1} (α := S) (↑n : S) 0
pos : ∀ (y : M), Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) y : M₂) (0 : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)

Tactic:
suffices ∀ y, f y = 0 by simp [this]
-- Module: Mathlib.Algebra.Module.Basic
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
hR : ¬Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : Eq.{u_7 + 1} (α := S) (↑n : S) 0
x : M
pos :
  Eq.{u_4 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x)) :
      M₂)
    (0 : M₂)
pos₁ :
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)
      ((f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) : M₂) =
    0
pos₂ :
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) 0
      ((f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) : M₂) =
    0
pos₃ pos₄ : Eq.{u_4 + 1} (α := M₂) 0 0
⊢ Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) (0 : M₂)

Tactic:
rw [← smul_inv_smul₀ hR x, map_natCast_smul f R S, hS, zero_smul]

Premises used: smul_inv_smul₀, map_natCast_smul, zero_smul
-- Module: Mathlib.Algebra.Module.Basic
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : ¬Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : ¬Eq.{u_7 + 1} (α := S) (↑n : S) 0
neg :
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (↑n : S)⁻¹
      (HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)
        ((f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) : M₂)) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
neg₁ :
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹
      ((f : (a : M) → M₂)
          (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x)) :
        M₂) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
neg₂ neg₃ :
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)

Tactic:
rw [← inv_smul_smul₀ hS (f _), ← map_natCast_smul f R S, smul_inv_smul₀ hR]

Premises used: inv_smul_smul₀, smul_inv_smul₀, map_natCast_smul, DFunLike.coe
-- Module: Mathlib.Algebra.Module.Basic
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
z : ℤ
x : M
inl :
  ∀ (n : ℕ),
    (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑(↑n : ℤ) : R)⁻¹ x) =
      HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(↑n : ℤ) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
inr :
  ∀ (n : ℕ),
    (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑(-(↑n : ℤ)) : R)⁻¹ x) =
      HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(-(↑n : ℤ)) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑z : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑z : S)⁻¹ ((f : (a : M) → M₂) x : M₂)

Tactic:
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Algebra.Module.Basic
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
x : M
n : ℕ
inl :
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(↑n : ℤ) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
inl₁ :
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
inl₂ inl₃ :
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑(↑n : ℤ) : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(↑n : ℤ) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)

Tactic:
rw [Int.cast_natCast, Int.cast_natCast, map_inv_natCast_smul _ R S]

Premises used: Int.cast_natCast, map_inv_natCast_smul
-- Module: Mathlib.Algebra.Module.Basic
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
x : M
n : ℕ
inr :
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (-(↑(↑n : ℤ) : R))⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (-(↑(↑n : ℤ) : S))⁻¹ ((f : (a : M) → M₂) x : M₂)
inr₁ :
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (-(↑n : R))⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (-(↑n : S))⁻¹ ((f : (a : M) → M₂) x : M₂)
inr₂ :
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (-(↑n : R)⁻¹) x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (-(↑n : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
inr₃ :
  (f : (a : M) → M₂) (-HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    -HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
inr₄ :
  -(f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    -HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑(-(↑n : ℤ)) : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(-(↑n : ℤ)) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)

Tactic:
simp_rw [Int.cast_neg, Int.cast_natCast, inv_neg, neg_smul, map_neg,
      map_inv_natCast_smul _ R S]

Premises used: Int.cast_neg, Int.cast_natCast, neg_smul, inv_neg, map_neg, map_inv_natCast_smul
-- Module: Mathlib.Algebra.Module.Basic
Goal:
E : Type u_5
R : Type u_6
S : Type u_7
inst : AddCommMonoid E
inst_1 : DivisionSemiring R
inst_2 : DivisionSemiring S
inst_3 : Module R E
inst_4 : Module S E
n : ℕ
x : E
⊢ HSMul.hSMul.{u_6, u_5, u_5} (α := R) (↑n : R)⁻¹ x = HSMul.hSMul.{u_7, u_5, u_5} (α := S) (↑n : S)⁻¹ x

Tactic:
map_inv_natCast_smul (AddMonoidHom.id E) R S n x

Premises used: AddMonoidHom.id, map_inv_natCast_smul
-- Module: Mathlib.Algebra.Module.Basic
Goal:
E : Type u_5
R : Type u_6
S : Type u_7
inst : AddCommGroup E
inst_1 : DivisionRing R
inst_2 : DivisionRing S
inst_3 : Module R E
inst_4 : Module S E
n : ℤ
x : E
⊢ HSMul.hSMul.{u_6, u_5, u_5} (α := R) (↑n : R)⁻¹ x = HSMul.hSMul.{u_7, u_5, u_5} (α := S) (↑n : S)⁻¹ x

Tactic:
map_inv_intCast_smul (AddMonoidHom.id E) R S n x

Premises used: AddMonoidHom.id, map_inv_intCast_smul
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_5
E : Type u_6
R : Type u_7
inst : AddCommMonoid E
inst_1 : DivisionSemiring R
inst_2 : Module R E
inst_3 : DistribSMul α E
n : ℕ
s : α
x : E
⊢ HSMul.hSMul.{u_7, u_6, u_6} (α := R) (↑n : R)⁻¹ (s • x) = s • HSMul.hSMul.{u_7, u_6, u_6} (α := R) (↑n : R)⁻¹ x

Tactic:
(map_inv_natCast_smul (DistribSMul.toAddMonoidHom E s) R R n x).symm

Premises used: map_inv_natCast_smul, Eq.symm, DistribSMul.toAddMonoidHom
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_5
E : Type u_6
R : Type u_7
inst : AddCommGroup E
inst_1 : DivisionRing R
inst_2 : Module R E
inst_3 : DistribSMul α E
n : ℤ
s : α
x : E
⊢ HSMul.hSMul.{u_7, u_6, u_6} (α := R) (↑n : R)⁻¹ (s • x) = s • HSMul.hSMul.{u_7, u_6, u_6} (α := R) (↑n : R)⁻¹ x

Tactic:
(map_inv_intCast_smul (DistribSMul.toAddMonoidHom E s) R R n x).symm

Premises used: Eq.symm, DistribSMul.toAddMonoidHom, map_inv_intCast_smul
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
f : α → R
g : α → M
x : α
hfg : x ∈ support (f • g)
hf : f x = 0
rw : f x • g x = 0
rw₁ : HSMul.hSMul.{u_2, u_3, u_3} (α := R) 0 (g x) = 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := M) 0 0
⊢ (f • g) x = 0

Tactic:
rw [Pi.smul_apply', hf, zero_smul]

Premises used: Pi.smul_apply', zero_smul
-- Module: Mathlib.Algebra.Module.Basic
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
f : α → R
g : α → M
x : α
hbf : x ∈ support (f • g)
hf : g x = 0
rw : f x • g x = 0
rw₁ : HSMul.hSMul (β := M) (f x) 0 = 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := M) 0 0
⊢ (f • g) x = 0

Tactic:
rw [Pi.smul_apply', hf, smul_zero]

Premises used: Pi.smul_apply', smul_zero