awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.toNat • p + a = (-m).toNat • p + b
have h₁ : m.toNat • p + a = b + (-m).toNat • p
Tactic: rwa [add_comm _ b, ← sub_eq_sub_iff_add_eq_add, ← natCast_zsmul, ← natCast_zsmul,
      sub_eq_add_neg, ← sub_zsmul, m.toNat_sub_toNat_neg]
-- 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
h₁ : m.toNat • p + a = b + (-m).toNat • p
⊢ m.toNat • p + a = (-m).toNat • p + b
have h₂ : m.toNat • p - (-m).toNat • p = b - a
Tactic: rwa [add_comm _ b, ← sub_eq_sub_iff_add_eq_add, ← natCast_zsmul, ← natCast_zsmul,
      sub_eq_add_neg, ← sub_zsmul, m.toNat_sub_toNat_neg]
-- 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
h₁ : m.toNat • p + a = b + (-m).toNat • p
h₂ : m.toNat • p - (-m).toNat • p = b - a
⊢ m.toNat • p + a = (-m).toNat • p + b
have h₃ : HSMul.hSMul (α := ℤ) (↑m.toNat : ℤ) p - (-m).toNat • p = b - a
Tactic: rwa [add_comm _ b, ← sub_eq_sub_iff_add_eq_add, ← natCast_zsmul, ← natCast_zsmul,
      sub_eq_add_neg, ← sub_zsmul, m.toNat_sub_toNat_neg]
-- 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
h₁ : m.toNat • p + a = b + (-m).toNat • p
h₂ : m.toNat • p - (-m).toNat • p = b - a
h₃ : HSMul.hSMul (α := ℤ) (↑m.toNat : ℤ) p - (-m).toNat • p = b - a
⊢ m.toNat • p + a = (-m).toNat • p + b
have h₄ : HSMul.hSMul (α := ℤ) (↑m.toNat : ℤ) p - HSMul.hSMul (α := ℤ) (↑(-m).toNat : ℤ) p = b - a
Tactic: rwa [add_comm _ b, ← sub_eq_sub_iff_add_eq_add, ← natCast_zsmul, ← natCast_zsmul,
      sub_eq_add_neg, ← sub_zsmul, m.toNat_sub_toNat_neg]
-- 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
h₁ : m.toNat • p + a = b + (-m).toNat • p
h₂ : m.toNat • p - (-m).toNat • p = b - a
h₃ : HSMul.hSMul (α := ℤ) (↑m.toNat : ℤ) p - (-m).toNat • p = b - a
h₄ : HSMul.hSMul (α := ℤ) (↑m.toNat : ℤ) p - HSMul.hSMul (α := ℤ) (↑(-m).toNat : ℤ) p = b - a
⊢ m.toNat • p + a = (-m).toNat • p + b
have h₅ : HSMul.hSMul (α := ℤ) (↑m.toNat : ℤ) p + -HSMul.hSMul (α := ℤ) (↑(-m).toNat : ℤ) p = b - a
Tactic: rwa [add_comm _ b, ← sub_eq_sub_iff_add_eq_add, ← natCast_zsmul, ← natCast_zsmul,
      sub_eq_add_neg, ← sub_zsmul, m.toNat_sub_toNat_neg]
-- 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
h₁ : m.toNat • p + a = b + (-m).toNat • p
h₂ : m.toNat • p - (-m).toNat • p = b - a
h₃ : HSMul.hSMul (α := ℤ) (↑m.toNat : ℤ) p - (-m).toNat • p = b - a
h₄ : HSMul.hSMul (α := ℤ) (↑m.toNat : ℤ) p - HSMul.hSMul (α := ℤ) (↑(-m).toNat : ℤ) p = b - a
h₅ : HSMul.hSMul (α := ℤ) (↑m.toNat : ℤ) p + -HSMul.hSMul (α := ℤ) (↑(-m).toNat : ℤ) p = b - a
⊢ m.toNat • p + a = (-m).toNat • p + b
have h₆ : HSub.hSub (α := ℤ) (↑m.toNat : ℤ) (↑(-m).toNat : ℤ) • p = b - a
Tactic: rwa [add_comm _ b, ← sub_eq_sub_iff_add_eq_add, ← natCast_zsmul, ← natCast_zsmul,
      sub_eq_add_neg, ← sub_zsmul, m.toNat_sub_toNat_neg]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z : ℤ
h : a ≡ b [PMOD z • p]
⊢ a ≡ b [PMOD p]
have rw : ∀ (h : ∃ (m : ℤ), m • z • p = b - a), ∃ (m : ℤ), m • p = b - a
Tactic: rw [modEq_iff_zsmul] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z : ℤ
h : ∃ (m : ℤ), m • z • p = b - a
⊢ ∃ (m : ℤ), m • p = b - a
have rcases : ∀ (m : ℤ) (h : m • z • p = b - a), ∃ (m : ℤ), m • p = b - a
Tactic: rcases h with ⟨m, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z : ℤ
h : a ≡ b [PMOD p]
⊢ z • a ≡ z • b [PMOD z • p]
have rw : ∀ (h : ∃ (m : ℤ), m • p = b - a), ∃ (m : ℤ), m • z • p = z • b - z • a
Tactic: rw [modEq_iff_zsmul] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z : ℤ
h : ∃ (m : ℤ), m • p = b - a
⊢ ∃ (m : ℤ), m • z • p = z • b - z • a
have rcases : ∀ (m : ℤ) (h : m • p = b - a), ∃ (m : ℤ), m • z • p = z • b - z • a
Tactic: rcases h with ⟨m, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z m : ℤ
h : m • p = b - a
⊢ ∃ (m : ℤ), m • z • p = z • b - z • a
have h₁ : m • z • p = z • b - z • a
Tactic: use m
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z m : ℤ
h : m • p = b - a
⊢ m • z • p = z • b - z • a
have h₁ : m • z • p = z • (b - a)
Tactic: rw [← zsmul_sub, ← h, ← mul_zsmul, ← mul_zsmul']
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z m : ℤ
h : m • p = b - a
h₁ : m • z • p = z • (b - a)
⊢ m • z • p = z • b - z • a
have h₂ : m • z • p = z • m • p
Tactic: rw [← zsmul_sub, ← h, ← mul_zsmul, ← mul_zsmul']
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z m : ℤ
h : m • p = b - a
h₁ : m • z • p = z • (b - a)
h₂ : m • z • p = z • m • p
⊢ m • z • p = z • b - z • a
have h₃ : (m * z) • p = z • m • p
Tactic: rw [← zsmul_sub, ← h, ← mul_zsmul, ← mul_zsmul']
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
z m : ℤ
h : m • p = b - a
h₁ : m • z • p = z • (b - a)
h₂ : m • z • p = z • m • p
h₃ : (m * z) • p = z • m • p
⊢ m • z • p = z • b - z • a
have h₄ : (m * z) • p = (m * z) • p
Tactic: rw [← zsmul_sub, ← h, ← mul_zsmul, ← mul_zsmul']
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b c : G
⊢ c + a ≡ b [PMOD p] ↔ a + c ≡ b [PMOD p]
have rw : a + c ≡ b [PMOD p] ↔ a + c ≡ b [PMOD p]
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
⊢ a ≡ b [PMOD p] ↔ ∃ (z : ℤ), b = a + z • p
have simp_rw : (∃ (m : ℤ), b - a = m • p) ↔ ∃ (z : ℤ), b = a + z • p
Tactic: simp_rw [modEq_iff_zsmul', sub_eq_iff_eq_add']
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a : G
⊢ a ≡ 0 [PMOD p] ↔ ∃ (z : ℤ), a = z • p
have rw : (∃ (z : ℤ), a = 0 + z • p) ↔ ∃ (z : ℤ), a = z • p
Tactic: rw [modEq_comm, modEq_iff_eq_add_zsmul]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
⊢ ¬a ≡ b [PMOD p] ↔ ∀ (z : ℤ), b ≠ a + z • p
have rw : (¬∃ (z : ℤ), b = a + z • p) ↔ ∀ (z : ℤ), b ≠ a + z • p
Tactic: rw [modEq_iff_eq_add_zsmul, not_exists]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
rw : (¬∃ (z : ℤ), b = a + z • p) ↔ ∀ (z : ℤ), b ≠ a + z • p
⊢ ¬a ≡ b [PMOD p] ↔ ∀ (z : ℤ), b ≠ a + z • p
have rw₁ : (∀ (x : ℤ), ¬b = a + x • p) ↔ ∀ (z : ℤ), b ≠ a + z • p
Tactic: rw [modEq_iff_eq_add_zsmul, not_exists]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ a ≡ b [PMOD p] ↔ ∃ (i : ℕ), i < n ∧ a ≡ b + i • p [PMOD n • p]
have simp_rw : b ≡ a [PMOD p] ↔ ∃ (i : ℕ), i < n ∧ b ≡ a - i • p [PMOD n • p]
Tactic: simp_rw [← sub_modEq_iff_modEq_add, modEq_comm (b := b)]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ b ≡ a [PMOD p] ↔ ∃ (i : ℕ), i < n ∧ b ≡ a - i • p [PMOD n • p]
have simp_rw : (∃ (m : ℤ), a - b = m • p) ↔ ∃ (i : ℕ), i < n ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + (↑i : ℤ)) • p
Tactic: simp_rw [modEq_iff_zsmul', sub_right_comm, sub_eq_iff_eq_add (b := _ • _), ← natCast_zsmul,
    ← mul_zsmul, ← add_zsmul]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ (∃ (m : ℤ), a - b = m • p) ↔ ∃ (i : ℕ), i < n ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + (↑i : ℤ)) • p
have mp : (∃ (m : ℤ), a - b = m • p) → ∃ (i : ℕ), i < n ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + (↑i : ℤ)) • p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
mp : (∃ (m : ℤ), a - b = m • p) → ∃ (i : ℕ), i < n ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + (↑i : ℤ)) • p
⊢ (∃ (m : ℤ), a - b = m • p) ↔ ∃ (i : ℕ), i < n ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + (↑i : ℤ)) • p
have mpr : (∃ (i : ℕ), i < n ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + (↑i : ℤ)) • p) → ∃ (m : ℤ), a - b = m • p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ ∃ (i : ℕ), i < n ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + (↑i : ℤ)) • p
have mp : (k % (↑n : ℤ)).toNat < n ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + (↑(k % (↑n : ℤ)).toNat : ℤ)) • p
Tactic: refine ⟨(k % n).toNat, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ (k % (↑n : ℤ)).toNat < n ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + (↑(k % (↑n : ℤ)).toNat : ℤ)) • p
have mp : k % (↑n : ℤ) < (↑n : ℤ) ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + k % (↑n : ℤ)) • p
Tactic: rw [← Int.ofNat_lt, Int.toNat_of_nonneg (Int.emod_nonneg _ (mod_cast hn))]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ k % (↑n : ℤ) < (↑n : ℤ) ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + k % (↑n : ℤ)) • p
have mp : k % (↑n : ℤ) < (↑n : ℤ)
Tactic: refine ⟨?_, k / n, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
mp : k % (↑n : ℤ) < (↑n : ℤ)
⊢ k % (↑n : ℤ) < (↑n : ℤ) ∧ ∃ (m : ℤ), a - b = (m * (↑n : ℤ) + k % (↑n : ℤ)) • p
have mp₁ : a - b = (k / (↑n : ℤ) * (↑n : ℤ) + k % (↑n : ℤ)) • p
Tactic: refine ⟨?_, k / n, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ k % (↑n : ℤ) < (↑n : ℤ)
have mp : LT.lt (α := ℤ) 0 (↑n : ℤ)
Tactic: refine Int.emod_lt_of_pos _ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ a - b = (k / (↑n : ℤ) * (↑n : ℤ) + k % (↑n : ℤ)) • p
have mp : k • p = (k / (↑n : ℤ) * (↑n : ℤ) + k % (↑n : ℤ)) • p
Tactic: rw [hk, Int.ediv_mul_add_emod]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
mp : k • p = (k / (↑n : ℤ) * (↑n : ℤ) + k % (↑n : ℤ)) • p
⊢ a - b = (k / (↑n : ℤ) * (↑n : ℤ) + k % (↑n : ℤ)) • p
have mp₁ : k • p = k • p
Tactic: rw [hk, Int.ediv_mul_add_emod]
-- Lean 4 proof step from Mathlib.Algebra.Group.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℕ
left : k < n
j : ℤ
hj : a - b = (j * (↑n : ℤ) + (↑k : ℤ)) • p
⊢ ∃ (m : ℤ), a - b = m • p
have mpr : ∃ (m : ℤ), (j * (↑n : ℤ) + (↑k : ℤ)) • p = m • p
Tactic: rw [hj]
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Even (goal)
Goal:
m_1 n m : ℕ
⊢ IsSquare m ↔ m.sqrt * m.sqrt = m
have simp_rw : IsSquare m ↔ ∃ (n : ℕ), n * n = m
Tactic: simp_rw [← Nat.exists_mul_self m, IsSquare, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Even (goal)
Goal:
m_1 n m : ℕ
simp_rw : IsSquare m ↔ ∃ (n : ℕ), n * n = m
⊢ IsSquare m ↔ m.sqrt * m.sqrt = m
have simp_rw₁ : (∃ (r : ℕ), m = r * r) ↔ ∃ (n : ℕ), n * n = m
Tactic: simp_rw [← Nat.exists_mul_self m, IsSquare, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Even (goal)
Goal:
m n : ℕ
⊢ Even (m * n) ↔ Even m ∨ Even n
have inl : ∀ (h₁ : m % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
Tactic: rcases mod_two_eq_zero_or_one m with h₁ | h₁
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Even (goal)
Goal:
m n : ℕ
inl : ∀ (h₁ : m % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
⊢ Even (m * n) ↔ Even m ∨ Even n
have inr : ∀ (h₁ : m % 2 = 1), Even (m * n) ↔ Even m ∨ Even n
Tactic: rcases mod_two_eq_zero_or_one m with h₁ | h₁
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Even (goal)
Goal:
m n : ℕ
h₁ : m % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n
have inl : ∀ (h₂ : n % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
Tactic: rcases mod_two_eq_zero_or_one n with h₂ | h₂
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Even (goal)
Goal:
m n : ℕ
h₁ : m % 2 = 0
inl : ∀ (h₂ : n % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
⊢ Even (m * n) ↔ Even m ∨ Even n
have inl₁ : ∀ (h₂ : n % 2 = 1), Even (m * n) ↔ Even m ∨ Even n
Tactic: rcases mod_two_eq_zero_or_one n with h₂ | h₂
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Even (goal)
Goal:
m n : ℕ
h₁ : m % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
have inr : ∀ (h₂ : n % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
Tactic: rcases mod_two_eq_zero_or_one n with h₂ | h₂
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Even (goal)
Goal:
m n : ℕ
h₁ : m % 2 = 1
inr : ∀ (h₂ : n % 2 = 0), Even (m * n) ↔ Even m ∨ Even n
⊢ Even (m * n) ↔ Even m ∨ Even n
have inr₁ : ∀ (h₂ : n % 2 = 1), Even (m * n) ↔ Even m ∨ Even n
Tactic: rcases mod_two_eq_zero_or_one n with h₂ | h₂
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Even (goal)
Goal:
m n : ℕ
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0
have zero : Even (HPow.hPow (β := ℕ) m 0) ↔ Even m ∧ Ne (α := ℕ) 0 0
Tactic: induction n with grind
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Even (goal)
Goal:
m n : ℕ
zero : Even (HPow.hPow (β := ℕ) m 0) ↔ Even m ∧ Ne (α := ℕ) 0 0
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0
have succ : ∀ (n : ℕ), (Even (m ^ n) ↔ Even m ∧ n ≠ 0) → (Even (m ^ (n + 1)) ↔ Even m ∧ n + 1 ≠ 0)
Tactic: induction n with grind
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Hom (goal)
Goal:
A : Type u_2
F : Type u_4
inst : FunLike F ℕ A
inst_1 : AddZeroClass A
inst_2 : AddMonoidHomClass F ℕ A
f g : F
h : Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) 1 : A) ((g : (a : ℕ) → A) 1 : A)
⊢ Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) 0 : A) ((g : (a : ℕ) → A) 0 : A)
have zero : Eq.{u_2 + 1} (α := A) (0 : A) ((g : (a : ℕ) → A) 0 : A)
Tactic: simp_rw [map_zero f, map_zero g]
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Hom (goal)
Goal:
A : Type u_2
F : Type u_4
inst : FunLike F ℕ A
inst_1 : AddZeroClass A
inst_2 : AddMonoidHomClass F ℕ A
f g : F
h : Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) 1 : A) ((g : (a : ℕ) → A) 1 : A)
n : ℕ
⊢ Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) n : A) ((g : (a : ℕ) → A) n : A)
have zero : Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) 0 : A) ((g : (a : ℕ) → A) 0 : A)
Tactic: induction n with
    | zero => simp_rw [map_zero f, map_zero g]
    | succ n ihn =>
      simp [h, ihn]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Hom (goal)
Goal:
A : Type u_2
F : Type u_4
inst : FunLike F ℕ A
inst_1 : AddZeroClass A
inst_2 : AddMonoidHomClass F ℕ A
f g : F
h : Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) 1 : A) ((g : (a : ℕ) → A) 1 : A)
n : ℕ
zero : Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) 0 : A) ((g : (a : ℕ) → A) 0 : A)
⊢ Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) n : A) ((g : (a : ℕ) → A) n : A)
have succ : ∀ (n : ℕ) (ihn : Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) n : A) ((g : (a : ℕ) → A) n : A)),
  Eq.{u_2 + 1} (α := A) ((f : (a : ℕ) → A) (n + 1) : A) ((g : (a : ℕ) → A) (n + 1) : A)
Tactic: induction n with
    | zero => simp_rw [map_zero f, map_zero g]
    | succ n ihn =>
      simp [h, ihn]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Hom (goal)
Goal:
M : Type u_1
inst : AddMonoid M
f : ℕ →+ M
n : ℕ
⊢ (f : (a : ℕ) → M) n = HSMul.hSMul (β := M) n ((f : (a : ℕ) → M) 1 : M)
have rw : (f : (a : ℕ) → M) n = HSMul.hSMul (β := M) n ((Equiv.symm (multiplesHom M) : (a : ℕ →+ M) → M) f : M)
Tactic: rw [← multiplesHom_symm_apply, ← multiplesHom_apply, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Hom (goal)
Goal:
M : Type u_1
inst : AddMonoid M
f : ℕ →+ M
n : ℕ
rw : (f : (a : ℕ) → M) n = HSMul.hSMul (β := M) n ((Equiv.symm (multiplesHom M) : (a : ℕ →+ M) → M) f : M)
⊢ (f : (a : ℕ) → M) n = HSMul.hSMul (β := M) n ((f : (a : ℕ) → M) 1 : M)
have rw₁ : Eq (α := M) ((f : (a : ℕ) → M) n : M)
  ((((multiplesHom M : (a : M) → ℕ →+ M) ((Equiv.symm (multiplesHom M) : (a : ℕ →+ M) → M) f) : ℕ →+ M) : (a : ℕ) → M)
      n :
    M)
Tactic: rw [← multiplesHom_symm_apply, ← multiplesHom_apply, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Hom (goal)
Goal:
M : Type u_1
inst : AddMonoid M
f : ℕ →+ M
n : ℕ
rw : (f : (a : ℕ) → M) n = HSMul.hSMul (β := M) n ((Equiv.symm (multiplesHom M) : (a : ℕ →+ M) → M) f : M)
rw₁ :
  Eq (α := M) ((f : (a : ℕ) → M) n : M)
    ((((multiplesHom M : (a : M) → ℕ →+ M) ((Equiv.symm (multiplesHom M) : (a : ℕ →+ M) → M) f) : ℕ →+ M) : (a : ℕ) → M)
        n :
      M)
⊢ (f : (a : ℕ) → M) n = HSMul.hSMul (β := M) n ((f : (a : ℕ) → M) 1 : M)
have rw₂ : Eq (α := M) ((f : (a : ℕ) → M) n : M) ((f : (a : ℕ) → M) n : M)
Tactic: rw [← multiplesHom_symm_apply, ← multiplesHom_apply, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Hom (goal)
Goal:
M : Type u_1
inst : Monoid M
f : Multiplicative ℕ →* M
n : Multiplicative ℕ
⊢ (f : (a : Multiplicative ℕ) → M) n =
    HPow.hPow (α := M) (β := ℕ)
      ((f : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
      ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ)
have rw : (f : (a : Multiplicative ℕ) → M) n =
  HPow.hPow (α := M) (β := ℕ) ((Equiv.symm (powersHom M) : (a : Multiplicative ℕ →* M) → M) f : M)
    ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ)
Tactic: rw [← powersHom_symm_apply, ← powersHom_apply, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Hom (goal)
Goal:
M : Type u_1
inst : Monoid M
f : Multiplicative ℕ →* M
n : Multiplicative ℕ
rw :
  (f : (a : Multiplicative ℕ) → M) n =
    HPow.hPow (α := M) (β := ℕ) ((Equiv.symm (powersHom M) : (a : Multiplicative ℕ →* M) → M) f : M)
      ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ)
⊢ (f : (a : Multiplicative ℕ) → M) n =
    HPow.hPow (α := M) (β := ℕ)
      ((f : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
      ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ)
have rw₁ : Eq (α := M) ((f : (a : Multiplicative ℕ) → M) n : M)
  ((((powersHom M : (a : M) → Multiplicative ℕ →* M) ((Equiv.symm (powersHom M) : (a : Multiplicative ℕ →* M) → M) f) :
          Multiplicative ℕ →* M) :
        (a : Multiplicative ℕ) → M)
      n :
    M)
Tactic: rw [← powersHom_symm_apply, ← powersHom_apply, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Hom (goal)
Goal:
M : Type u_1
inst : Monoid M
f : Multiplicative ℕ →* M
n : Multiplicative ℕ
rw :
  (f : (a : Multiplicative ℕ) → M) n =
    HPow.hPow (α := M) (β := ℕ) ((Equiv.symm (powersHom M) : (a : Multiplicative ℕ →* M) → M) f : M)
      ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ)
rw₁ :
  Eq (α := M) ((f : (a : Multiplicative ℕ) → M) n : M)
    ((((powersHom M : (a : M) → Multiplicative ℕ →* M)
              ((Equiv.symm (powersHom M) : (a : Multiplicative ℕ →* M) → M) f) :
            Multiplicative ℕ →* M) :
          (a : Multiplicative ℕ) → M)
        n :
      M)
⊢ (f : (a : Multiplicative ℕ) → M) n =
    HPow.hPow (α := M) (β := ℕ)
      ((f : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
      ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ)
have rw₂ : Eq (α := M) ((f : (a : Multiplicative ℕ) → M) n : M) ((f : (a : Multiplicative ℕ) → M) n : M)
Tactic: rw [← powersHom_symm_apply, ← powersHom_apply, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Hom (goal)
Goal:
M : Type u_1
inst : Monoid M
f g : Multiplicative ℕ →* M
h :
  Eq (α := M) ((f : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
    ((g : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
n : Multiplicative ℕ
⊢ Eq (α := M) ((f : (a : Multiplicative ℕ) → M) n : M) ((g : (a : Multiplicative ℕ) → M) n : M)
have rw : HPow.hPow (α := M) (β := ℕ)
    ((f : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
    ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ) =
  (g : (a : Multiplicative ℕ) → M) n
Tactic: rw [f.apply_mnat, g.apply_mnat, h]
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Hom (goal)
Goal:
M : Type u_1
inst : Monoid M
f g : Multiplicative ℕ →* M
h :
  Eq (α := M) ((f : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
    ((g : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
n : Multiplicative ℕ
rw :
  HPow.hPow (α := M) (β := ℕ)
      ((f : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
      ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ) =
    (g : (a : Multiplicative ℕ) → M) n
⊢ Eq (α := M) ((f : (a : Multiplicative ℕ) → M) n : M) ((g : (a : Multiplicative ℕ) → M) n : M)
have rw₁ : HPow.hPow (α := M) (β := ℕ)
    ((f : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
    ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ) =
  HPow.hPow (α := M) (β := ℕ)
    ((g : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
    ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ)
Tactic: rw [f.apply_mnat, g.apply_mnat, h]
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Hom (goal)
Goal:
M : Type u_1
inst : Monoid M
f g : Multiplicative ℕ →* M
h :
  Eq (α := M) ((f : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
    ((g : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
n : Multiplicative ℕ
rw :
  HPow.hPow (α := M) (β := ℕ)
      ((f : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
      ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ) =
    (g : (a : Multiplicative ℕ) → M) n
rw₁ :
  HPow.hPow (α := M) (β := ℕ)
      ((f : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
      ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ) =
    HPow.hPow (α := M) (β := ℕ)
      ((g : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
      ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ)
⊢ Eq (α := M) ((f : (a : Multiplicative ℕ) → M) n : M) ((g : (a : Multiplicative ℕ) → M) n : M)
have rw₂ : HPow.hPow (α := M) (β := ℕ)
    ((g : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
    ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ) =
  HPow.hPow (α := M) (β := ℕ)
    ((g : (a : Multiplicative ℕ) → M) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) : M)
    ((toAdd : (a : Multiplicative ℕ) → ℕ) n : ℕ)
Tactic: rw [f.apply_mnat, g.apply_mnat, h]
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Range (goal)
Goal:
a : ℕ
s : Finset ℕ
⊢ Disjoint (range a) (map (addLeftEmbedding a) s)
have simp_rw : ∀ ⦃a_1 : ℕ⦄, a_1 < a → ¬∃ a_3 ∈ s, a + a_3 = a_1
Tactic: simp_rw [disjoint_left, mem_map, mem_range, addLeftEmbedding_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Range (goal)
Goal:
a : ℕ
s : Finset ℕ
⊢ Disjoint (range a) (map (addRightEmbedding a) s)
have rw : Disjoint (range a) (map (addLeftEmbedding a) s)
Tactic: rw [← addLeftEmbedding_eq_addRightEmbedding]
-- Lean 4 proof step from Mathlib.Algebra.Group.Nat.Range (goal)
Goal:
a b : ℕ
⊢ range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)
have rw : (range (a + b)).val = (range a).val ∪ (map (addLeftEmbedding a) (range b)).val
Tactic: rw [← val_inj, union_val]