awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
hcd : ∃ (m : ℕ), ∃ (n : ℕ), m • p + c = n • p + d
k l : ℕ
hab : k • p + a = l • p + b
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + (a + c) = n • p + (b + d)
have rcases : ∀ (m n : ℕ) (hcd : m • p + c = n • p + d), ∃ (m : ℕ), ∃ (n : ℕ), m • p + (a + c) = n • p + (b + d)
Tactic: rcases hcd with ⟨m, n, hcd⟩
Cleared hypotheses: hcd
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
k l : ℕ
hab : k • p + a = l • p + b
m n : ℕ
hcd : m • p + c = n • p + d
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + (a + c) = n • p + (b + d)
have h : (k + m) • p + (a + c) = (l + n) • p + (b + d)
Tactic: use k + m, l + n
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
k l : ℕ
hab : k • p + a = l • p + b
m n : ℕ
hcd : m • p + c = n • p + d
⊢ (k + m) • p + (a + c) = (l + n) • p + (b + d)
have h : k • p + m • p + (a + c) = (l + n) • p + (b + d)
Tactic: rw [add_nsmul, add_add_add_comm, hab, hcd, add_nsmul, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
k l : ℕ
hab : k • p + a = l • p + b
m n : ℕ
hcd : m • p + c = n • p + d
h : k • p + m • p + (a + c) = (l + n) • p + (b + d)
⊢ (k + m) • p + (a + c) = (l + n) • p + (b + d)
have h₁ : k • p + a + (m • p + c) = (l + n) • p + (b + d)
Tactic: rw [add_nsmul, add_add_add_comm, hab, hcd, add_nsmul, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
k l : ℕ
hab : k • p + a = l • p + b
m n : ℕ
hcd : m • p + c = n • p + d
h : k • p + m • p + (a + c) = (l + n) • p + (b + d)
h₁ : k • p + a + (m • p + c) = (l + n) • p + (b + d)
⊢ (k + m) • p + (a + c) = (l + n) • p + (b + d)
have h₂ : l • p + b + (m • p + c) = (l + n) • p + (b + d)
Tactic: rw [add_nsmul, add_add_add_comm, hab, hcd, add_nsmul, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
k l : ℕ
hab : k • p + a = l • p + b
m n : ℕ
hcd : m • p + c = n • p + d
h : k • p + m • p + (a + c) = (l + n) • p + (b + d)
h₁ : k • p + a + (m • p + c) = (l + n) • p + (b + d)
h₂ : l • p + b + (m • p + c) = (l + n) • p + (b + d)
⊢ (k + m) • p + (a + c) = (l + n) • p + (b + d)
have h₃ : l • p + b + (n • p + d) = (l + n) • p + (b + d)
Tactic: rw [add_nsmul, add_add_add_comm, hab, hcd, add_nsmul, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
k l : ℕ
hab : k • p + a = l • p + b
m n : ℕ
hcd : m • p + c = n • p + d
h : k • p + m • p + (a + c) = (l + n) • p + (b + d)
h₁ : k • p + a + (m • p + c) = (l + n) • p + (b + d)
h₂ : l • p + b + (m • p + c) = (l + n) • p + (b + d)
h₃ : l • p + b + (n • p + d) = (l + n) • p + (b + d)
⊢ (k + m) • p + (a + c) = (l + n) • p + (b + d)
have h₄ : l • p + b + (n • p + d) = l • p + n • p + (b + d)
Tactic: rw [add_nsmul, add_add_add_comm, hab, hcd, add_nsmul, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b c d p : M
k l : ℕ
hab : k • p + a = l • p + b
m n : ℕ
hcd : m • p + c = n • p + d
h : k • p + m • p + (a + c) = (l + n) • p + (b + d)
h₁ : k • p + a + (m • p + c) = (l + n) • p + (b + d)
h₂ : l • p + b + (m • p + c) = (l + n) • p + (b + d)
h₃ : l • p + b + (n • p + d) = (l + n) • p + (b + d)
h₄ : l • p + b + (n • p + d) = l • p + n • p + (b + d)
⊢ (k + m) • p + (a + c) = (l + n) • p + (b + d)
have h₅ : l • p + n • p + (b + d) = l • p + n • p + (b + d)
Tactic: rw [add_nsmul, add_add_add_comm, hab, hcd, add_nsmul, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
n : ℕ
h : a ≡ b [PMOD p]
⊢ n • a ≡ n • b [PMOD n • p]
have h₁ : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
Tactic: rw [modEq_iff_nsmul] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
n : ℕ
h : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
⊢ ∃ (m : ℕ), ∃ (n_1 : ℕ), m • n • p + n • a = n_1 • n • p + n • b
have rcases : ∀ (k l : ℕ) (h : k • p + a = l • p + b), ∃ (m : ℕ), ∃ (n_1 : ℕ), m • n • p + n • a = n_1 • n • p + n • b
Tactic: rcases h with ⟨k, l, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
n k l : ℕ
h : k • p + a = l • p + b
⊢ ∃ (m : ℕ), ∃ (n_1 : ℕ), m • n • p + n • a = n_1 • n • p + n • b
have h₁ : k • n • p + n • a = l • n • p + n • b
Tactic: use k, l
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
n k l : ℕ
h : k • p + a = l • p + b
⊢ k • n • p + n • a = l • n • p + n • b
have h₁ : (n * k) • p + n • a = l • n • p + n • b
Tactic: rw [← mul_nsmul, mul_nsmul', ← nsmul_add, h, nsmul_add, ← mul_nsmul, mul_nsmul']
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
n k l : ℕ
h : k • p + a = l • p + b
h₁ : (n * k) • p + n • a = l • n • p + n • b
⊢ k • n • p + n • a = l • n • p + n • b
have h₂ : n • k • p + n • a = l • n • p + n • b
Tactic: rw [← mul_nsmul, mul_nsmul', ← nsmul_add, h, nsmul_add, ← mul_nsmul, mul_nsmul']
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
n k l : ℕ
h : k • p + a = l • p + b
h₁ : (n * k) • p + n • a = l • n • p + n • b
h₂ : n • k • p + n • a = l • n • p + n • b
⊢ k • n • p + n • a = l • n • p + n • b
have h₃ : n • (k • p + a) = l • n • p + n • b
Tactic: rw [← mul_nsmul, mul_nsmul', ← nsmul_add, h, nsmul_add, ← mul_nsmul, mul_nsmul']
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
n k l : ℕ
h : k • p + a = l • p + b
h₁ : (n * k) • p + n • a = l • n • p + n • b
h₂ : n • k • p + n • a = l • n • p + n • b
h₃ : n • (k • p + a) = l • n • p + n • b
⊢ k • n • p + n • a = l • n • p + n • b
have h₄ : n • (l • p + b) = l • n • p + n • b
Tactic: rw [← mul_nsmul, mul_nsmul', ← nsmul_add, h, nsmul_add, ← mul_nsmul, mul_nsmul']
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
n k l : ℕ
h : k • p + a = l • p + b
h₁ : (n * k) • p + n • a = l • n • p + n • b
h₂ : n • k • p + n • a = l • n • p + n • b
h₃ : n • (k • p + a) = l • n • p + n • b
h₄ : n • (l • p + b) = l • n • p + n • b
⊢ k • n • p + n • a = l • n • p + n • b
have h₅ : n • l • p + n • b = l • n • p + n • b
Tactic: rw [← mul_nsmul, mul_nsmul', ← nsmul_add, h, nsmul_add, ← mul_nsmul, mul_nsmul']
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
n k l : ℕ
h : k • p + a = l • p + b
h₁ : (n * k) • p + n • a = l • n • p + n • b
h₂ : n • k • p + n • a = l • n • p + n • b
h₃ : n • (k • p + a) = l • n • p + n • b
h₄ : n • (l • p + b) = l • n • p + n • b
h₅ : n • l • p + n • b = l • n • p + n • b
⊢ k • n • p + n • a = l • n • p + n • b
have h₆ : (l * n) • p + n • b = l • n • p + n • b
Tactic: rw [← mul_nsmul, mul_nsmul', ← nsmul_add, h, nsmul_add, ← mul_nsmul, mul_nsmul']
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
n k l : ℕ
h : k • p + a = l • p + b
h₁ : (n * k) • p + n • a = l • n • p + n • b
h₂ : n • k • p + n • a = l • n • p + n • b
h₃ : n • (k • p + a) = l • n • p + n • b
h₄ : n • (l • p + b) = l • n • p + n • b
h₅ : n • l • p + n • b = l • n • p + n • b
h₆ : (l * n) • p + n • b = l • n • p + n • b
⊢ k • n • p + n • a = l • n • p + n • b
have h₇ : l • n • p + n • b = l • n • p + n • b
Tactic: rw [← mul_nsmul, mul_nsmul', ← nsmul_add, h, nsmul_add, ← mul_nsmul, mul_nsmul']
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
h : a ≡ b [PMOD p]
⊢ ModEq.{u_2} (M := N) ((f : (a : M) → N) p : N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)
have h₁ : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
Tactic: rw [modEq_iff_nsmul] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
h : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
⊢ ∃ (m : ℕ),
    ∃ (n : ℕ),
      HAdd.hAdd (β := N) (HSMul.hSMul (β := N) m ((f : (a : M) → N) p : N)) ((f : (a : M) → N) a : N) =
        HAdd.hAdd (β := N) (HSMul.hSMul (β := N) n ((f : (a : M) → N) p : N)) ((f : (a : M) → N) b : N)
have rcases : ∀ (m n : ℕ) (h : m • p + a = n • p + b),
  ∃ (m : ℕ),
    ∃ (n : ℕ),
      HAdd.hAdd (β := N) (HSMul.hSMul (β := N) m ((f : (a : M) → N) p : N)) ((f : (a : M) → N) a : N) =
        HAdd.hAdd (β := N) (HSMul.hSMul (β := N) n ((f : (a : M) → N) p : N)) ((f : (a : M) → N) b : N)
Tactic: rcases h with ⟨m, n, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
m n : ℕ
h : m • p + a = n • p + b
⊢ ∃ (m : ℕ),
    ∃ (n : ℕ),
      HAdd.hAdd (β := N) (HSMul.hSMul (β := N) m ((f : (a : M) → N) p : N)) ((f : (a : M) → N) a : N) =
        HAdd.hAdd (β := N) (HSMul.hSMul (β := N) n ((f : (a : M) → N) p : N)) ((f : (a : M) → N) b : N)
have h₁ : HAdd.hAdd (β := N) (HSMul.hSMul (β := N) m ((f : (a : M) → N) p : N)) ((f : (a : M) → N) a : N) =
  HAdd.hAdd (β := N) (HSMul.hSMul (β := N) n ((f : (a : M) → N) p : N)) ((f : (a : M) → N) b : N)
Tactic: use m, n
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
h : a ≡ b [PMOD p]
⊢ a + c ≡ b + d [PMOD p] ↔ c ≡ d [PMOD p]
have refine : ∀ (hadd : a + c ≡ b + d [PMOD p]), c ≡ d [PMOD p]
Tactic: refine ⟨fun hadd ↦ ?_, h.add⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (hypothesis)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
h : a ≡ b [PMOD p]
hadd : a + c ≡ b + d [PMOD p]
⊢ c ≡ d [PMOD p]
have h₁ : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
Tactic: rw [modEq_iff_nsmul] at *
Cleared hypotheses: h, hadd
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (hypothesis)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
h : a ≡ b [PMOD p]
hadd : a + c ≡ b + d [PMOD p]
h₁ : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
⊢ c ≡ d [PMOD p]
have hadd₁ : ∃ (m : ℕ), ∃ (n : ℕ), m • p + (a + c) = n • p + (b + d)
Tactic: rw [modEq_iff_nsmul] at *
Cleared hypotheses: h, hadd
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
h : ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
hadd : ∃ (m : ℕ), ∃ (n : ℕ), m • p + (a + c) = n • p + (b + d)
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + c = n • p + d
have rcases : ∀ (k l : ℕ) (h : k • p + a = l • p + b), ∃ (m : ℕ), ∃ (n : ℕ), m • p + c = n • p + d
Tactic: rcases h with ⟨k, l, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
hadd : ∃ (m : ℕ), ∃ (n : ℕ), m • p + (a + c) = n • p + (b + d)
k l : ℕ
h : k • p + a = l • p + b
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + c = n • p + d
have rcases : ∀ (m n : ℕ) (hadd : m • p + (a + c) = n • p + (b + d)), ∃ (m : ℕ), ∃ (n : ℕ), m • p + c = n • p + d
Tactic: rcases hadd with ⟨m, n, hadd⟩
Cleared hypotheses: hadd
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + c = n • p + d
have h₁ : (m + l) • p + c = (n + k) • p + d
Tactic: use m + l, n + k
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
⊢ (m + l) • p + c = (n + k) • p + d
have h₁ : (m + l) • p + c + a = (n + k) • p + d + a
Tactic: apply add_right_cancel (b := a)
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
⊢ (m + l) • p + c + a = (n + k) • p + d + a
have h₁ : (m + l) • p + (c + a) = (n + k) • p + d + a
Tactic: rw [add_assoc, add_comm c, add_nsmul, add_right_comm, hadd, ← add_assoc, add_right_comm _ b,
    add_right_comm _ b, add_assoc, ← h, add_add_add_comm, add_nsmul, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
h₁ : (m + l) • p + (c + a) = (n + k) • p + d + a
⊢ (m + l) • p + c + a = (n + k) • p + d + a
have h₂ : (m + l) • p + (a + c) = (n + k) • p + d + a
Tactic: rw [add_assoc, add_comm c, add_nsmul, add_right_comm, hadd, ← add_assoc, add_right_comm _ b,
    add_right_comm _ b, add_assoc, ← h, add_add_add_comm, add_nsmul, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
h₁ : (m + l) • p + (c + a) = (n + k) • p + d + a
h₂ : (m + l) • p + (a + c) = (n + k) • p + d + a
⊢ (m + l) • p + c + a = (n + k) • p + d + a
have h₃ : m • p + l • p + (a + c) = (n + k) • p + d + a
Tactic: rw [add_assoc, add_comm c, add_nsmul, add_right_comm, hadd, ← add_assoc, add_right_comm _ b,
    add_right_comm _ b, add_assoc, ← h, add_add_add_comm, add_nsmul, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
h₁ : (m + l) • p + (c + a) = (n + k) • p + d + a
h₂ : (m + l) • p + (a + c) = (n + k) • p + d + a
h₃ : m • p + l • p + (a + c) = (n + k) • p + d + a
⊢ (m + l) • p + c + a = (n + k) • p + d + a
have h₄ : m • p + (a + c) + l • p = (n + k) • p + d + a
Tactic: rw [add_assoc, add_comm c, add_nsmul, add_right_comm, hadd, ← add_assoc, add_right_comm _ b,
    add_right_comm _ b, add_assoc, ← h, add_add_add_comm, add_nsmul, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
h₁ : (m + l) • p + (c + a) = (n + k) • p + d + a
h₂ : (m + l) • p + (a + c) = (n + k) • p + d + a
h₃ : m • p + l • p + (a + c) = (n + k) • p + d + a
h₄ : m • p + (a + c) + l • p = (n + k) • p + d + a
⊢ (m + l) • p + c + a = (n + k) • p + d + a
have h₅ : n • p + (b + d) + l • p = (n + k) • p + d + a
Tactic: rw [add_assoc, add_comm c, add_nsmul, add_right_comm, hadd, ← add_assoc, add_right_comm _ b,
    add_right_comm _ b, add_assoc, ← h, add_add_add_comm, add_nsmul, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
h₁ : (m + l) • p + (c + a) = (n + k) • p + d + a
h₂ : (m + l) • p + (a + c) = (n + k) • p + d + a
h₃ : m • p + l • p + (a + c) = (n + k) • p + d + a
h₄ : m • p + (a + c) + l • p = (n + k) • p + d + a
h₅ : n • p + (b + d) + l • p = (n + k) • p + d + a
⊢ (m + l) • p + c + a = (n + k) • p + d + a
have h₆ : n • p + b + d + l • p = (n + k) • p + d + a
Tactic: rw [add_assoc, add_comm c, add_nsmul, add_right_comm, hadd, ← add_assoc, add_right_comm _ b,
    add_right_comm _ b, add_assoc, ← h, add_add_add_comm, add_nsmul, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
h₁ : (m + l) • p + (c + a) = (n + k) • p + d + a
h₂ : (m + l) • p + (a + c) = (n + k) • p + d + a
h₃ : m • p + l • p + (a + c) = (n + k) • p + d + a
h₄ : m • p + (a + c) + l • p = (n + k) • p + d + a
h₅ : n • p + (b + d) + l • p = (n + k) • p + d + a
h₆ : n • p + b + d + l • p = (n + k) • p + d + a
⊢ (m + l) • p + c + a = (n + k) • p + d + a
have h₇ : n • p + d + b + l • p = (n + k) • p + d + a
Tactic: rw [add_assoc, add_comm c, add_nsmul, add_right_comm, hadd, ← add_assoc, add_right_comm _ b,
    add_right_comm _ b, add_assoc, ← h, add_add_add_comm, add_nsmul, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
h₁ : (m + l) • p + (c + a) = (n + k) • p + d + a
h₂ : (m + l) • p + (a + c) = (n + k) • p + d + a
h₃ : m • p + l • p + (a + c) = (n + k) • p + d + a
h₄ : m • p + (a + c) + l • p = (n + k) • p + d + a
h₅ : n • p + (b + d) + l • p = (n + k) • p + d + a
h₆ : n • p + b + d + l • p = (n + k) • p + d + a
h₇ : n • p + d + b + l • p = (n + k) • p + d + a
⊢ (m + l) • p + c + a = (n + k) • p + d + a
have h₈ : n • p + d + l • p + b = (n + k) • p + d + a
Tactic: rw [add_assoc, add_comm c, add_nsmul, add_right_comm, hadd, ← add_assoc, add_right_comm _ b,
    add_right_comm _ b, add_assoc, ← h, add_add_add_comm, add_nsmul, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
h₁ : (m + l) • p + (c + a) = (n + k) • p + d + a
h₂ : (m + l) • p + (a + c) = (n + k) • p + d + a
h₃ : m • p + l • p + (a + c) = (n + k) • p + d + a
h₄ : m • p + (a + c) + l • p = (n + k) • p + d + a
h₅ : n • p + (b + d) + l • p = (n + k) • p + d + a
h₆ : n • p + b + d + l • p = (n + k) • p + d + a
h₇ : n • p + d + b + l • p = (n + k) • p + d + a
h₈ : n • p + d + l • p + b = (n + k) • p + d + a
⊢ (m + l) • p + c + a = (n + k) • p + d + a
have h₉ : n • p + d + (l • p + b) = (n + k) • p + d + a
Tactic: rw [add_assoc, add_comm c, add_nsmul, add_right_comm, hadd, ← add_assoc, add_right_comm _ b,
    add_right_comm _ b, add_assoc, ← h, add_add_add_comm, add_nsmul, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
h₁ : (m + l) • p + (c + a) = (n + k) • p + d + a
h₂ : (m + l) • p + (a + c) = (n + k) • p + d + a
h₃ : m • p + l • p + (a + c) = (n + k) • p + d + a
h₄ : m • p + (a + c) + l • p = (n + k) • p + d + a
h₅ : n • p + (b + d) + l • p = (n + k) • p + d + a
h₆ : n • p + b + d + l • p = (n + k) • p + d + a
h₇ : n • p + d + b + l • p = (n + k) • p + d + a
h₈ : n • p + d + l • p + b = (n + k) • p + d + a
h₉ : n • p + d + (l • p + b) = (n + k) • p + d + a
⊢ (m + l) • p + c + a = (n + k) • p + d + a
have h₁₀ : n • p + d + (k • p + a) = (n + k) • p + d + a
Tactic: rw [add_assoc, add_comm c, add_nsmul, add_right_comm, hadd, ← add_assoc, add_right_comm _ b,
    add_right_comm _ b, add_assoc, ← h, add_add_add_comm, add_nsmul, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
h₁ : (m + l) • p + (c + a) = (n + k) • p + d + a
h₂ : (m + l) • p + (a + c) = (n + k) • p + d + a
h₃ : m • p + l • p + (a + c) = (n + k) • p + d + a
h₄ : m • p + (a + c) + l • p = (n + k) • p + d + a
h₅ : n • p + (b + d) + l • p = (n + k) • p + d + a
h₆ : n • p + b + d + l • p = (n + k) • p + d + a
h₇ : n • p + d + b + l • p = (n + k) • p + d + a
h₈ : n • p + d + l • p + b = (n + k) • p + d + a
h₉ : n • p + d + (l • p + b) = (n + k) • p + d + a
h₁₀ : n • p + d + (k • p + a) = (n + k) • p + d + a
⊢ (m + l) • p + c + a = (n + k) • p + d + a
have h₁₁ : n • p + k • p + (d + a) = (n + k) • p + d + a
Tactic: rw [add_assoc, add_comm c, add_nsmul, add_right_comm, hadd, ← add_assoc, add_right_comm _ b,
    add_right_comm _ b, add_assoc, ← h, add_add_add_comm, add_nsmul, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
h₁ : (m + l) • p + (c + a) = (n + k) • p + d + a
h₂ : (m + l) • p + (a + c) = (n + k) • p + d + a
h₃ : m • p + l • p + (a + c) = (n + k) • p + d + a
h₄ : m • p + (a + c) + l • p = (n + k) • p + d + a
h₅ : n • p + (b + d) + l • p = (n + k) • p + d + a
h₆ : n • p + b + d + l • p = (n + k) • p + d + a
h₇ : n • p + d + b + l • p = (n + k) • p + d + a
h₈ : n • p + d + l • p + b = (n + k) • p + d + a
h₉ : n • p + d + (l • p + b) = (n + k) • p + d + a
h₁₀ : n • p + d + (k • p + a) = (n + k) • p + d + a
h₁₁ : n • p + k • p + (d + a) = (n + k) • p + d + a
⊢ (m + l) • p + c + a = (n + k) • p + d + a
have h₁₂ : n • p + k • p + (d + a) = n • p + k • p + d + a
Tactic: rw [add_assoc, add_comm c, add_nsmul, add_right_comm, hadd, ← add_assoc, add_right_comm _ b,
    add_right_comm _ b, add_assoc, ← h, add_add_add_comm, add_nsmul, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
M : Type u_1
inst : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
h₁ : (m + l) • p + (c + a) = (n + k) • p + d + a
h₂ : (m + l) • p + (a + c) = (n + k) • p + d + a
h₃ : m • p + l • p + (a + c) = (n + k) • p + d + a
h₄ : m • p + (a + c) + l • p = (n + k) • p + d + a
h₅ : n • p + (b + d) + l • p = (n + k) • p + d + a
h₆ : n • p + b + d + l • p = (n + k) • p + d + a
h₇ : n • p + d + b + l • p = (n + k) • p + d + a
h₈ : n • p + d + l • p + b = (n + k) • p + d + a
h₉ : n • p + d + (l • p + b) = (n + k) • p + d + a
h₁₀ : n • p + d + (k • p + a) = (n + k) • p + d + a
h₁₁ : n • p + k • p + (d + a) = (n + k) • p + d + a
h₁₂ : n • p + k • p + (d + a) = n • p + k • p + d + a
⊢ (m + l) • p + c + a = (n + k) • p + d + a
have h₁₃ : n • p + k • p + d + a = n • p + k • p + d + a
Tactic: rw [add_assoc, add_comm c, add_nsmul, add_right_comm, hadd, ← add_assoc, add_right_comm _ b,
    add_right_comm _ b, add_assoc, ← h, add_add_add_comm, add_nsmul, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
⊢ (∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b) ↔ ∃ (m : ℤ), m • p = b - a
have mp : (∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b) → ∃ (m : ℤ), m • p = b - a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
mp : (∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b) → ∃ (m : ℤ), m • p = b - a
⊢ (∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b) ↔ ∃ (m : ℤ), m • p = b - a
have mpr : (∃ (m : ℤ), m • p = b - a) → ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
m n : ℕ
h : m • p + a = n • p + b
⊢ ∃ (m : ℤ), m • p = b - a
have h₁ : HSub.hSub (α := ℤ) (↑m : ℤ) (↑n : ℤ) • p = b - a
Tactic: use m - n
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
m n : ℕ
h : m • p + a = n • p + b
⊢ HSub.hSub (α := ℤ) (↑m : ℤ) (↑n : ℤ) • p = b - a
have h₁ : HSMul.hSMul (α := ℤ) (↑m : ℤ) p + a = HSMul.hSMul (α := ℤ) (↑n : ℤ) p + b
Tactic: rw [sub_zsmul, ← sub_eq_add_neg, sub_eq_sub_iff_add_eq_add, add_comm b]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
m : ℤ
h : m • p = b - a
⊢ ∃ (m : ℕ), ∃ (n : ℕ), m • p + a = n • p + b
have h₁ : m.toNat • p + a = (-m).toNat • p + b
Tactic: use m.toNat, (-m).toNat