awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
P : Type u_5
inst_6 : AddCommMonoid P
inst_7 : Module R P
Q : Type u_6
inst_8 : AddCommMonoid Q
inst_9 : Module R Q
f' : P →ₗ[R] Q
inst_10 : IsLocalizedModule p f'
g : M →ₗ[R] P
⊢ range.{u_1, u_1, u_4, u_6} (R := R) (M := N) (τ₁₂ := RingHom.id R)
      ((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g) =
    localized₀ p f' g.range
have h : ∀ (x : Q),
  Membership.mem (γ := Submodule R Q)
      (range.{u_1, u_1, u_4, u_6} (R := R) (M := N) (τ₁₂ := RingHom.id R)
        ((IsLocalizedModule.map p f f' : (a : M →ₗ[R] P) → N →ₗ[R] Q) g))
      x ↔
    x ∈ localized₀ p f' g.range
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : M
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (-1) a + a = 0
have nth_rw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (-1) a + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 a = 0
Tactic: nth_rw 2 [← one_smul R a]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : M
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (-1) a + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 a = 0
have rw : HAdd.hAdd (α := R) (-1) 1 • a = 0
Tactic: rw [← add_smul, neg_add_cancel, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : M
rw : HAdd.hAdd (α := R) (-1) 1 • a = 0
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (-1) a + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 a = 0
have rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 a = 0
Tactic: rw [← add_smul, neg_add_cancel, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : M
rw : HAdd.hAdd (α := R) (-1) 1 • a = 0
rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 a = 0
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (-1) a + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 a = 0
have rw₂ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [← add_smul, neg_add_cancel, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : M
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑0 : R) b = HSMul.hSMul (α := ℕ) 0 b
have zero : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 b = HSMul.hSMul (α := ℕ) 0 b
Tactic: rw [Nat.cast_zero, zero_smul, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : M
zero : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 b = HSMul.hSMul (α := ℕ) 0 b
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑0 : R) b = HSMul.hSMul (α := ℕ) 0 b
have zero₁ : 0 = HSMul.hSMul (α := ℕ) 0 b
Tactic: rw [Nat.cast_zero, zero_smul, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : M
zero : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 b = HSMul.hSMul (α := ℕ) 0 b
zero₁ : 0 = HSMul.hSMul (α := ℕ) 0 b
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑0 : R) b = HSMul.hSMul (α := ℕ) 0 b
have zero₂ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [Nat.cast_zero, zero_smul, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : M
n : ℕ
ih : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b = n • b
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(n + 1) : R) b = (n + 1) • b
have succ : HAdd.hAdd (α := R) (↑n : R) 1 • b = (n + 1) • b
Tactic: rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : M
n : ℕ
ih : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b = n • b
succ : HAdd.hAdd (α := R) (↑n : R) 1 • b = (n + 1) • b
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(n + 1) : R) b = (n + 1) • b
have succ₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 b = (n + 1) • b
Tactic: rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : M
n : ℕ
ih : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b = n • b
succ : HAdd.hAdd (α := R) (↑n : R) 1 • b = (n + 1) • b
succ₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 b = (n + 1) • b
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(n + 1) : R) b = (n + 1) • b
have succ₂ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 b =
  n • b + HSMul.hSMul (α := ℕ) 1 b
Tactic: rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : M
n : ℕ
ih : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b = n • b
succ : HAdd.hAdd (α := R) (↑n : R) 1 • b = (n + 1) • b
succ₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 b = (n + 1) • b
succ₂ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 b =
    n • b + HSMul.hSMul (α := ℕ) 1 b
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(n + 1) : R) b = (n + 1) • b
have succ₃ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b + b = n • b + HSMul.hSMul (α := ℕ) 1 b
Tactic: rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : M
n : ℕ
ih : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b = n • b
succ : HAdd.hAdd (α := R) (↑n : R) 1 • b = (n + 1) • b
succ₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 b = (n + 1) • b
succ₂ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 b =
    n • b + HSMul.hSMul (α := ℕ) 1 b
succ₃ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b + b = n • b + HSMul.hSMul (α := ℕ) 1 b
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(n + 1) : R) b = (n + 1) • b
have succ₄ : n • b + b = n • b + HSMul.hSMul (α := ℕ) 1 b
Tactic: rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : M
n : ℕ
ih : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b = n • b
succ : HAdd.hAdd (α := R) (↑n : R) 1 • b = (n + 1) • b
succ₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 b = (n + 1) • b
succ₂ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b + HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 b =
    n • b + HSMul.hSMul (α := ℕ) 1 b
succ₃ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b + b = n • b + HSMul.hSMul (α := ℕ) 1 b
succ₄ : n • b + b = n • b + HSMul.hSMul (α := ℕ) 1 b
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(n + 1) : R) b = (n + 1) • b
have succ₅ : n • b + b = n • b + b
Tactic: rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
b : M
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b = n • b
have zero : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑0 : R) b = HSMul.hSMul (α := ℕ) 0 b
Tactic: induction n with
  | zero => rw [Nat.cast_zero, zero_smul, zero_smul]
  | succ n ih => rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
b : M
zero : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑0 : R) b = HSMul.hSMul (α := ℕ) 0 b
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b = n • b
have succ : ∀ (n : ℕ) (ih : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b = n • b),
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(n + 1) : R) b = (n + 1) • b
Tactic: induction n with
  | zero => rw [Nat.cast_zero, zero_smul, zero_smul]
  | succ n ih => rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : R
y : M
⊢ (n • x) • y = n • x • y
have zero : HSMul.hSMul (α := ℕ) 0 x • y = HSMul.hSMul (α := ℕ) 0 (x • y)
Tactic: induction n with
    | zero => simp only [zero_smul]
    | succ n ih => simp only [add_smul, one_smul, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : R
y : M
zero : HSMul.hSMul (α := ℕ) 0 x • y = HSMul.hSMul (α := ℕ) 0 (x • y)
⊢ (n • x) • y = n • x • y
have succ : ∀ (n : ℕ) (ih : (n • x) • y = n • x • y), ((n + 1) • x) • y = (n + 1) • x • y
Tactic: induction n with
    | zero => simp only [zero_smul]
    | succ n ih => simp only [add_smul, one_smul, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_5
inst : NonAssocSemiring R
m : ℕ
⊢ HSMul.hSMul (β := R) m 1 = (↑m : R)
have rw : HMul.hMul (α := R) (↑m : R) 1 = (↑m : R)
Tactic: rw [nsmul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_5
inst : NonAssocSemiring R
m : ℕ
rw : HMul.hMul (α := R) (↑m : R) 1 = (↑m : R)
⊢ HSMul.hSMul (β := R) m 1 = (↑m : R)
have rw₁ : Eq.{u_5 + 1} (α := R) (↑m : R) (↑m : R)
Tactic: rw [nsmul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_5
inst : NonAssocRing R
m : ℤ
⊢ HSMul.hSMul (β := R) m 1 = (↑m : R)
have rw : HMul.hMul (α := R) (↑m : R) 1 = (↑m : R)
Tactic: rw [zsmul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_5
inst : NonAssocRing R
m : ℤ
rw : HMul.hMul (α := R) (↑m : R) 1 = (↑m : R)
⊢ HSMul.hSMul (β := R) m 1 = (↑m : R)
have rw₁ : Eq.{u_5 + 1} (α := R) (↑m : R) (↑m : R)
Tactic: rw [zsmul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℤ
b : M
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b = n • b
have ofNat : ∀ (a : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(ofNat a) : R) b = ofNat a • b
Tactic: cases n with
  | ofNat => simp [Nat.cast_smul_eq_nsmul]
  | negSucc => simp [add_smul, Nat.cast_smul_eq_nsmul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℤ
b : M
ofNat : ∀ (a : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(Int.ofNat a) : R) b = Int.ofNat a • b
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b = n • b
have negSucc : ∀ (a : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑-[a+1] : R) b = -[a+1] • b
Tactic: cases n with
  | ofNat => simp [Nat.cast_smul_eq_nsmul]
  | negSucc => simp [add_smul, Nat.cast_smul_eq_nsmul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R_1 : Type u_1
S : Type u_2
M_1 : Type u_3
M₂ : Type u_4
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℤ
x : R
y : M
⊢ (n • x) • y = n • x • y
have ofNat : ∀ (a : ℕ), (Int.ofNat a • x) • y = Int.ofNat a • x • y
Tactic: cases n with
    | ofNat => simp [mul_smul, Nat.cast_smul_eq_nsmul]
    | negSucc => simp [mul_smul, add_smul, Nat.cast_smul_eq_nsmul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R_1 : Type u_1
S : Type u_2
M_1 : Type u_3
M₂ : Type u_4
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℤ
x : R
y : M
ofNat : ∀ (a : ℕ), (Int.ofNat a • x) • y = Int.ofNat a • x • y
⊢ (n • x) • y = n • x • y
have negSucc : ∀ (a : ℕ), (Int.negSucc a • x) • y = Int.negSucc a • x • y
Tactic: cases n with
    | ofNat => simp [mul_smul, Nat.cast_smul_eq_nsmul]
    | negSucc => simp [mul_smul, add_smul, Nat.cast_smul_eq_nsmul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoidWithOne M
inst_2 : CharZero M
inst_3 : Module R M
⊢ CharZero R
have refine : ∀ (m n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)), Eq.{u_3 + 1} (α := M) (↑m : M) (↑n : M)
Tactic: refine ⟨fun m n h => @Nat.cast_injective M _ _ _ _ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoidWithOne M
inst_2 : CharZero M
inst_3 : Module R M
m n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)
⊢ Eq.{u_3 + 1} (α := M) (↑m : M) (↑n : M)
have rw : HSMul.hSMul (β := M) m 1 = (↑n : M)
Tactic: rw [← nsmul_one, ← nsmul_one, ← Nat.cast_smul_eq_nsmul R, ← Nat.cast_smul_eq_nsmul R, h]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoidWithOne M
inst_2 : CharZero M
inst_3 : Module R M
m n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)
rw : HSMul.hSMul (β := M) m 1 = (↑n : M)
⊢ Eq.{u_3 + 1} (α := M) (↑m : M) (↑n : M)
have rw₁ : HSMul.hSMul (β := M) m 1 = HSMul.hSMul (β := M) n 1
Tactic: rw [← nsmul_one, ← nsmul_one, ← Nat.cast_smul_eq_nsmul R, ← Nat.cast_smul_eq_nsmul R, h]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoidWithOne M
inst_2 : CharZero M
inst_3 : Module R M
m n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)
rw : HSMul.hSMul (β := M) m 1 = (↑n : M)
rw₁ : HSMul.hSMul (β := M) m 1 = HSMul.hSMul (β := M) n 1
⊢ Eq.{u_3 + 1} (α := M) (↑m : M) (↑n : M)
have rw₂ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) (↑m : R) 1 = HSMul.hSMul (β := M) n 1
Tactic: rw [← nsmul_one, ← nsmul_one, ← Nat.cast_smul_eq_nsmul R, ← Nat.cast_smul_eq_nsmul R, h]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoidWithOne M
inst_2 : CharZero M
inst_3 : Module R M
m n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)
rw : HSMul.hSMul (β := M) m 1 = (↑n : M)
rw₁ : HSMul.hSMul (β := M) m 1 = HSMul.hSMul (β := M) n 1
rw₂ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) (↑m : R) 1 = HSMul.hSMul (β := M) n 1
⊢ Eq.{u_3 + 1} (α := M) (↑m : M) (↑n : M)
have rw₃ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) (↑m : R) 1 = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) (↑n : R) 1
Tactic: rw [← nsmul_one, ← nsmul_one, ← Nat.cast_smul_eq_nsmul R, ← Nat.cast_smul_eq_nsmul R, h]
-- Lean 4 proof step from Mathlib.Algebra.Module.NatInt (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoidWithOne M
inst_2 : CharZero M
inst_3 : Module R M
m n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)
rw : HSMul.hSMul (β := M) m 1 = (↑n : M)
rw₁ : HSMul.hSMul (β := M) m 1 = HSMul.hSMul (β := M) n 1
rw₂ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) (↑m : R) 1 = HSMul.hSMul (β := M) n 1
rw₃ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) (↑m : R) 1 = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) (↑n : R) 1
⊢ Eq.{u_3 + 1} (α := M) (↑m : M) (↑n : M)
have rw₄ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) (↑n : R) 1 = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) (↑n : R) 1
Tactic: rw [← nsmul_one, ← nsmul_one, ← Nat.cast_smul_eq_nsmul R, ← Nat.cast_smul_eq_nsmul R, h]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
⊢ DirectSum.IsInternal (S := Submodule R M) fun (p : ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))) ↦
    torsionBy R M
      (IsPrincipal.generator (↑p : Ideal R) ^ Multiset.count (↑p : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤)))
have h : ∀ (x : ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))),
  Eq (α := Submodule R M)
    (torsionBy R M
      (IsPrincipal.generator (↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))))
    (torsionBySet R M
      (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
Tactic: convert! isInternal_prime_power_torsion hM
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
x : ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))
⊢ Eq (α := Submodule R M)
    (torsionBy R M
      (IsPrincipal.generator (↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))))
    (torsionBySet R M
      (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
have h : Eq (α := Submodule R M)
  (torsionBySet R M
    (↑(R ∙
          IsPrincipal.generator (↑x : Ideal R) ^
            Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) :
      Set R))
  (torsionBySet R M
    (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
Tactic: rw [← torsionBySet_span_singleton_eq, Ideal.submodule_span_eq, ← Ideal.span_singleton_pow,
    Ideal.span_singleton_generator]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
x : ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))
h :
  Eq (α := Submodule R M)
    (torsionBySet R M
      (↑(R ∙
            IsPrincipal.generator (↑x : Ideal R) ^
              Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) :
        Set R))
    (torsionBySet R M
      (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
⊢ Eq (α := Submodule R M)
    (torsionBy R M
      (IsPrincipal.generator (↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))))
    (torsionBySet R M
      (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
have h₁ : Eq (α := Submodule R M)
  (torsionBySet R M
    (↑(Ideal.span
          {IsPrincipal.generator (↑x : Ideal R) ^
              Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))}) :
      Set R))
  (torsionBySet R M
    (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
Tactic: rw [← torsionBySet_span_singleton_eq, Ideal.submodule_span_eq, ← Ideal.span_singleton_pow,
    Ideal.span_singleton_generator]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
x : ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))
h :
  Eq (α := Submodule R M)
    (torsionBySet R M
      (↑(R ∙
            IsPrincipal.generator (↑x : Ideal R) ^
              Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) :
        Set R))
    (torsionBySet R M
      (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
h₁ :
  Eq (α := Submodule R M)
    (torsionBySet R M
      (↑(Ideal.span
            {IsPrincipal.generator (↑x : Ideal R) ^
                Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))}) :
        Set R))
    (torsionBySet R M
      (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
⊢ Eq (α := Submodule R M)
    (torsionBy R M
      (IsPrincipal.generator (↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))))
    (torsionBySet R M
      (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
have h₂ : Eq (α := Submodule R M)
  (torsionBySet R M
    (↑(HPow.hPow (α := Ideal R) (Ideal.span {IsPrincipal.generator (↑x : Ideal R)})
          (Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤)))) :
      Set R))
  (torsionBySet R M
    (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
Tactic: rw [← torsionBySet_span_singleton_eq, Ideal.submodule_span_eq, ← Ideal.span_singleton_pow,
    Ideal.span_singleton_generator]
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
x : ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))
h :
  Eq (α := Submodule R M)
    (torsionBySet R M
      (↑(R ∙
            IsPrincipal.generator (↑x : Ideal R) ^
              Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) :
        Set R))
    (torsionBySet R M
      (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
h₁ :
  Eq (α := Submodule R M)
    (torsionBySet R M
      (↑(Ideal.span
            {IsPrincipal.generator (↑x : Ideal R) ^
                Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))}) :
        Set R))
    (torsionBySet R M
      (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
h₂ :
  Eq (α := Submodule R M)
    (torsionBySet R M
      (↑(HPow.hPow (α := Ideal R) (Ideal.span {IsPrincipal.generator (↑x : Ideal R)})
            (Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤)))) :
        Set R))
    (torsionBySet R M
      (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
⊢ Eq (α := Submodule R M)
    (torsionBy R M
      (IsPrincipal.generator (↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))))
    (torsionBySet R M
      (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
have h₃ : Eq (α := Submodule R M)
  (torsionBySet R M
    (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
  (torsionBySet R M
    (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
Tactic: rw [← torsionBySet_span_singleton_eq, Ideal.submodule_span_eq, ← Ideal.span_singleton_pow,
    Ideal.span_singleton_generator]