awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n a b : ℕ
cop : m.Coprime n
ha : a ≠ 0
hb : b ≠ 0
h : a * m + b * n = m * n
⊢ False
have obtain : ∀ (x : ℕ) (ha : n * x ≠ 0) (h : n * x * m + b * n = m * n), False
Tactic: obtain ⟨x, rfl⟩ : n ∣ a :=
    cop.symm.dvd_of_dvd_mul_right
      ((Nat.dvd_add_iff_left (Nat.dvd_mul_left n b)).mpr
        ((congr_arg _ h).mpr (Nat.dvd_mul_left n m)))
Cleared hypotheses: a, ha, h
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n b : ℕ
cop : m.Coprime n
hb : b ≠ 0
x : ℕ
ha : n * x ≠ 0
h : n * x * m + b * n = m * n
⊢ False
have obtain : ∀ (y : ℕ) (hb : m * y ≠ 0) (h : n * x * m + m * y * n = m * n), False
Tactic: obtain ⟨y, rfl⟩ : m ∣ b :=
    cop.dvd_of_dvd_mul_right
      ((Nat.dvd_add_iff_right (Nat.dvd_mul_left m (n * x))).mpr
        ((congr_arg _ h).mpr (Nat.dvd_mul_right m n)))
Cleared hypotheses: b, hb, h
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : n * x ≠ 0
y : ℕ
hb : m * y ≠ 0
h : n * x * m + m * y * n = m * n
⊢ False
have rw : ∀ (ha : 1 ≤ x ∧ n ≠ 0) (y : ℕ) (hb : 1 ≤ y ∧ m ≠ 0) (h : n * x * m + m * y * n = m * n), False
Tactic: rw [mul_comm, mul_ne_zero_iff, ← one_le_iff_ne_zero] at ha hb
Cleared hypotheses: ha, y, hb, h
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ False
have refine : (x + y) * (m * n) = m * n
Tactic: refine mul_ne_zero hb.2 ha.2 (eq_zero_of_mul_eq_self_left (ne_of_gt (add_le_add ha.1 hb.1)) ?_)
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ (x + y) * (m * n) = m * n
have rw : (x + y) * m * n = m * n
Tactic: rw [← mul_assoc, ← h, Nat.add_mul, Nat.add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
rw : (x + y) * m * n = m * n
⊢ (x + y) * (m * n) = m * n
have rw₁ : (x + y) * m * n = n * x * m + m * y * n
Tactic: rw [← mul_assoc, ← h, Nat.add_mul, Nat.add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
rw : (x + y) * m * n = m * n
rw₁ : (x + y) * m * n = n * x * m + m * y * n
⊢ (x + y) * (m * n) = m * n
have rw₂ : (x * m + y * m) * n = n * x * m + m * y * n
Tactic: rw [← mul_assoc, ← h, Nat.add_mul, Nat.add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
rw : (x + y) * m * n = m * n
rw₁ : (x + y) * m * n = n * x * m + m * y * n
rw₂ : (x * m + y * m) * n = n * x * m + m * y * n
⊢ (x + y) * (m * n) = m * n
have rw₃ : x * m * n + y * m * n = n * x * m + m * y * n
Tactic: rw [← mul_assoc, ← h, Nat.add_mul, Nat.add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
rw : (x + y) * m * n = m * n
rw₁ : (x + y) * m * n = n * x * m + m * y * n
rw₂ : (x * m + y * m) * n = n * x * m + m * y * n
rw₃ : x * m * n + y * m * n = n * x * m + m * y * n
⊢ (x + y) * (m * n) = m * n
have rw₄ : n * (x * m) + y * m * n = n * x * m + m * y * n
Tactic: rw [← mul_assoc, ← h, Nat.add_mul, Nat.add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
rw : (x + y) * m * n = m * n
rw₁ : (x + y) * m * n = n * x * m + m * y * n
rw₂ : (x * m + y * m) * n = n * x * m + m * y * n
rw₃ : x * m * n + y * m * n = n * x * m + m * y * n
rw₄ : n * (x * m) + y * m * n = n * x * m + m * y * n
⊢ (x + y) * (m * n) = m * n
have rw₅ : n * x * m + y * m * n = n * x * m + m * y * n
Tactic: rw [← mul_assoc, ← h, Nat.add_mul, Nat.add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
rw : (x + y) * m * n = m * n
rw₁ : (x + y) * m * n = n * x * m + m * y * n
rw₂ : (x * m + y * m) * n = n * x * m + m * y * n
rw₃ : x * m * n + y * m * n = n * x * m + m * y * n
rw₄ : n * (x * m) + y * m * n = n * x * m + m * y * n
rw₅ : n * x * m + y * m * n = n * x * m + m * y * n
⊢ (x + y) * (m * n) = m * n
have rw₆ : n * x * m + m * y * n = n * x * m + m * y * n
Tactic: rw [← mul_assoc, ← h, Nat.add_mul, Nat.add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
x n m : ℕ
hcop : n.Coprime m
⊢ x.gcd n * x.gcd m = x ↔ x ∣ n * m
have refine_1 : ∀ (h : x.gcd n * x.gcd m = x), x ∣ n * m
Tactic: refine ⟨fun h ↦ ?_, (dvd_antisymm ?_ <| dvd_gcd_mul_gcd_iff_dvd_mul.mpr ·)⟩
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
x n m : ℕ
hcop : n.Coprime m
refine_1 : ∀ (h : x.gcd n * x.gcd m = x), x ∣ n * m
⊢ x.gcd n * x.gcd m = x ↔ x ∣ n * m
have refine_2 : x ∣ n * m → x.gcd n * x.gcd m ∣ x
Tactic: refine ⟨fun h ↦ ?_, (dvd_antisymm ?_ <| dvd_gcd_mul_gcd_iff_dvd_mul.mpr ·)⟩
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
x n m : ℕ
hcop : n.Coprime m
h : x.gcd n * x.gcd m = x
⊢ x ∣ n * m
have refine_1 : x.gcd n ∣ n
Tactic: refine h ▸ Nat.mul_dvd_mul ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
x n m : ℕ
hcop : n.Coprime m
h : x.gcd n * x.gcd m = x
refine_1 : x.gcd n ∣ n
⊢ x ∣ n * m
have refine_1₁ : x.gcd m ∣ m
Tactic: refine h ▸ Nat.mul_dvd_mul ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
x n m : ℕ
hcop : n.Coprime m
h : x ∣ n * m
⊢ x.gcd n * x.gcd m ∣ x
have refine_2 : x.gcd n ∣ x
Tactic: refine (hcop.gcd_both x x).mul_dvd_of_dvd_of_dvd ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
x n m : ℕ
hcop : n.Coprime m
h : x ∣ n * m
refine_2 : x.gcd n ∣ x
⊢ x.gcd n * x.gcd m ∣ x
have refine_2₁ : x.gcd m ∣ x
Tactic: refine (hcop.gcd_both x x).mul_dvd_of_dvd_of_dvd ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
⊢ k / m * (m / n) = k / n
have inl : ∀ (hn : n = 0), k / m * (m / n) = k / n
Tactic: rcases n.eq_zero_or_pos with hn | hn
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
inl : ∀ (hn : n = 0), k / m * (m / n) = k / n
⊢ k / m * (m / n) = k / n
have inr : ∀ (hn : n > 0), k / m * (m / n) = k / n
Tactic: rcases n.eq_zero_or_pos with hn | hn
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
hn : n > 0
⊢ k / m * (m / n) = k / n
have inr : k = k / m * (m / n) * n
Tactic: refine (Nat.div_eq_of_eq_mul_left hn ?_).symm
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
hn : n > 0
⊢ k = k / m * (m / n) * n
have inr : k = k / m * (m / n * n)
Tactic: rw [mul_assoc, Nat.div_mul_cancel hkn, Nat.div_mul_cancel hkm]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
hn : n > 0
inr : k = k / m * (m / n * n)
⊢ k = k / m * (m / n) * n
have inr₁ : k = k / m * m
Tactic: rw [mul_assoc, Nat.div_mul_cancel hkn, Nat.div_mul_cancel hkm]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
hn : n > 0
inr : k = k / m * (m / n * n)
inr₁ : k = k / m * m
⊢ k = k / m * (m / n) * n
have inr₂ : k = k
Tactic: rw [mul_assoc, Nat.div_mul_cancel hkn, Nat.div_mul_cancel hkm]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
⊢ (k / m).lcm (k / n) = k / m.gcd n
have rw : k / m ∣ k / m.gcd n ∧ k / n ∣ k / m.gcd n ∧ ∀ (c : ℕ), k / m ∣ c → k / n ∣ c → k / m.gcd n ∣ c
Tactic: rw [Nat.lcm_eq_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
⊢ k / m ∣ k / m.gcd n ∧ k / n ∣ k / m.gcd n ∧ ∀ (c : ℕ), k / m ∣ c → k / n ∣ c → k / m.gcd n ∣ c
have refine : ∀ (c : ℕ) (hmc : k / m ∣ c) (hnc : k / n ∣ c), k / m.gcd n ∣ c
Tactic: refine ⟨div_dvd_div_left hkm (Nat.gcd_dvd_left m n),
        div_dvd_div_left hkn (Nat.gcd_dvd_right m n), fun c hmc hnc ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k / m ∣ c
hnc : k / n ∣ c
⊢ k / m.gcd n ∣ c
have inl : ∀ (hm : m = 0), k / m.gcd n ∣ c
Tactic: rcases m.eq_zero_or_pos with hm | hm
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k / m ∣ c
hnc : k / n ∣ c
inl : ∀ (hm : m = 0), k / m.gcd n ∣ c
⊢ k / m.gcd n ∣ c
have inr : ∀ (hm : m > 0), k / m.gcd n ∣ c
Tactic: rcases m.eq_zero_or_pos with hm | hm
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k / m ∣ c
hnc : k / n ∣ c
hm : m > 0
⊢ k / m.gcd n ∣ c
have inr : ∀ (hn : n = 0), k / m.gcd n ∣ c
Tactic: rcases n.eq_zero_or_pos with hn | hn
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (goal)
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k / m ∣ c
hnc : k / n ∣ c
hm : m > 0
inr : ∀ (hn : n = 0), k / m.gcd n ∣ c
⊢ k / m.gcd n ∣ c
have inr₁ : ∀ (hn : n > 0), k / m.gcd n ∣ c
Tactic: rcases n.eq_zero_or_pos with hn | hn
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (hypothesis)
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k / m ∣ c
hnc : k / n ∣ c
hm : m > 0
hn : n > 0
⊢ k / m.gcd n ∣ c
have hmc₁ : k ∣ m * c
Tactic: rw [Nat.div_dvd_iff_dvd_mul hkm hm] at hmc
Cleared hypotheses: hmc, hnc, hm, hn
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.Basic (hypothesis)
Goal:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k ∣ m * c
hnc : k / n ∣ c
hm : m > 0
hn : n > 0
⊢ k / m.gcd n ∣ c
have hnc₁ : k ∣ n * c
Tactic: rw [Nat.div_dvd_iff_dvd_mul hkn hn] at hnc
Cleared hypotheses: hnc, hm, hn
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.BigOperators (goal)
Goal:
l : List ℕ
k : ℕ
⊢ l.prod.Coprime k ↔ ∀ n ∈ l, n.Coprime k
have nil : Coprime (List.prod []) k ↔ ∀ (n : ℕ), Membership.mem (γ := List ℕ) [] n → n.Coprime k
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.BigOperators (goal)
Goal:
l : List ℕ
k : ℕ
nil : Coprime (List.prod []) k ↔ ∀ (n : ℕ), Membership.mem (γ := List ℕ) [] n → n.Coprime k
⊢ l.prod.Coprime k ↔ ∀ n ∈ l, n.Coprime k
have cons : ∀ (head : ℕ) (tail : List ℕ),
  (tail.prod.Coprime k ↔ ∀ n ∈ tail, n.Coprime k) → ((head :: tail).prod.Coprime k ↔ ∀ n ∈ head :: tail, n.Coprime k)
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.BigOperators (goal)
Goal:
k : ℕ
l : List ℕ
⊢ k.Coprime l.prod ↔ ∀ n ∈ l, k.Coprime n
have simp_rw : l.prod.Coprime k ↔ ∀ n ∈ l, n.Coprime k
Tactic: simp_rw [coprime_comm (n := k), coprime_list_prod_left_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.BigOperators (goal)
Goal:
m : Multiset ℕ
k : ℕ
⊢ m.prod.Coprime k ↔ ∀ n ∈ m, n.Coprime k
have h : ∀ (a : List ℕ), (Multiset.prod ⟦a⟧).Coprime k ↔ ∀ n ∈ ⟦a⟧, n.Coprime k
Tactic: induction m using Quotient.inductionOn
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.GCD.BigOperators (goal)
Goal:
k : ℕ
m : Multiset ℕ
⊢ k.Coprime m.prod ↔ ∀ n ∈ m, k.Coprime n
have h : ∀ (a : List ℕ), k.Coprime (Multiset.prod ⟦a⟧) ↔ ∀ n ∈ ⟦a⟧, k.Coprime n
Tactic: induction m using Quotient.inductionOn
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.Hyperoperation (goal)
Goal:
m k : ℕ
⊢ hyperoperation 1 m k = m + k
have zero : hyperoperation 1 m 0 = m + 0
Tactic: induction k with grind
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Hyperoperation (goal)
Goal:
m k : ℕ
zero : hyperoperation 1 m 0 = m + 0
⊢ hyperoperation 1 m k = m + k
have succ : ∀ (n : ℕ), hyperoperation 1 m n = m + n → hyperoperation 1 m (n + 1) = m + (n + 1)
Tactic: induction k with grind
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Hyperoperation (goal)
Goal:
m k : ℕ
⊢ hyperoperation 2 m k = m * k
have zero : hyperoperation 2 m 0 = m * 0
Tactic: induction k with grind
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Hyperoperation (goal)
Goal:
m k : ℕ
zero : hyperoperation 2 m 0 = m * 0
⊢ hyperoperation 2 m k = m * k
have succ : ∀ (n : ℕ), hyperoperation 2 m n = m * n → hyperoperation 2 m (n + 1) = m * (n + 1)
Tactic: induction k with grind
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Hyperoperation (goal)
Goal:
m k : ℕ
⊢ hyperoperation 3 m k = m ^ k
have zero : hyperoperation 3 m 0 = HPow.hPow (β := ℕ) m 0
Tactic: induction k with grind
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Hyperoperation (goal)
Goal:
m k : ℕ
zero : hyperoperation 3 m 0 = HPow.hPow (β := ℕ) m 0
⊢ hyperoperation 3 m k = m ^ k
have succ : ∀ (n : ℕ), hyperoperation 3 m n = m ^ n → hyperoperation 3 m (n + 1) = m ^ (n + 1)
Tactic: induction k with grind
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Hyperoperation (goal)
Goal:
n m : ℕ
⊢ hyperoperation (n + 2) m 1 = m
have zero : hyperoperation (HAdd.hAdd (α := ℕ) 0 2) m 1 = m
Tactic: induction n with grind
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Hyperoperation (goal)
Goal:
n m : ℕ
zero : hyperoperation (HAdd.hAdd (α := ℕ) 0 2) m 1 = m
⊢ hyperoperation (n + 2) m 1 = m
have succ : ∀ (n : ℕ), hyperoperation (n + 2) m 1 = m → hyperoperation (n + 1 + 2) m 1 = m
Tactic: induction n with grind
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Hyperoperation (goal)
Goal:
n : ℕ
⊢ hyperoperation (n + 1) 2 2 = 4
have zero : hyperoperation (HAdd.hAdd (α := ℕ) 0 1) 2 2 = 4
Tactic: induction n with grind
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Hyperoperation (goal)
Goal:
n : ℕ
zero : hyperoperation (HAdd.hAdd (α := ℕ) 0 1) 2 2 = 4
⊢ hyperoperation (n + 1) 2 2 = 4
have succ : ∀ (n : ℕ), hyperoperation (n + 1) 2 2 = 4 → hyperoperation (n + 1 + 1) 2 2 = 4
Tactic: induction n with grind
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Hyperoperation (goal)
Goal:
n k : ℕ
⊢ hyperoperation (n + 3) 1 k = 1
have zero : ∀ (k : ℕ), hyperoperation (HAdd.hAdd (α := ℕ) 0 3) 1 k = 1
Tactic: induction n generalizing k with grind [cases Nat]
Cleared hypotheses: n, k
-- Lean 4 proof step from Mathlib.Data.Nat.Hyperoperation (goal)
Goal:
n k : ℕ
zero : ∀ (k : ℕ), hyperoperation (HAdd.hAdd (α := ℕ) 0 3) 1 k = 1
⊢ hyperoperation (n + 3) 1 k = 1
have succ : ∀ (n : ℕ), (∀ (k : ℕ), hyperoperation (n + 3) 1 k = 1) → ∀ (k : ℕ), hyperoperation (n + 1 + 3) 1 k = 1
Tactic: induction n generalizing k with grind [cases Nat]
Cleared hypotheses: n, k
-- Lean 4 proof step from Mathlib.Data.Nat.Hyperoperation (goal)
Goal:
n k : ℕ
⊢ hyperoperation (n + 4) 0 k = if Even k then 1 else 0
have zero : hyperoperation (n + 4) 0 0 = if Even (α := ℕ) 0 then 1 else 0
Tactic: induction k with grind
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Hyperoperation (goal)
Goal:
n k : ℕ
zero : hyperoperation (n + 4) 0 0 = if Even (α := ℕ) 0 then 1 else 0
⊢ hyperoperation (n + 4) 0 k = if Even k then 1 else 0
have succ : ∀ (n_1 : ℕ),
  (hyperoperation (n + 4) 0 n_1 = if Even n_1 then 1 else 0) →
    hyperoperation (n + 4) 0 (n_1 + 1) = if Even (n_1 + 1) then 1 else 0
Tactic: induction k with grind
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n : ℕ
⊢ ¬2 * n % 2 = (2 * m + 1) % 2
have rw : ¬Eq (α := ℕ) 0 1
Tactic: rw [Nat.add_comm, add_mul_mod_self_left, mul_mod_right, mod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n : ℕ
rw : ¬Eq (α := ℕ) 0 1
⊢ ¬2 * n % 2 = (2 * m + 1) % 2
have rw₁ : LT.lt (α := ℕ) 1 2
Tactic: rw [Nat.add_comm, add_mul_mod_self_left, mul_mod_right, mod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n m : ℕ
⊢ m ≤ n / 2 ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
have rw : m * 2 ≤ n ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
Tactic: rw [Nat.le_div_iff_mul_le Nat.zero_lt_two, ← Int.ofNat_le, Int.natCast_mul, Int.ofNat_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n m : ℕ
rw : m * 2 ≤ n ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
⊢ m ≤ n / 2 ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
have rw₁ : LE.le (α := ℤ) (↑(m * 2) : ℤ) (↑n : ℤ) ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
Tactic: rw [Nat.le_div_iff_mul_le Nat.zero_lt_two, ← Int.ofNat_le, Int.natCast_mul, Int.ofNat_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n m : ℕ
rw : m * 2 ≤ n ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
rw₁ : LE.le (α := ℤ) (↑(m * 2) : ℤ) (↑n : ℤ) ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
⊢ m ≤ n / 2 ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
have rw₂ : HMul.hMul (α := ℤ) (↑m : ℤ) (↑2 : ℤ) ≤ (↑n : ℤ) ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
Tactic: rw [Nat.le_div_iff_mul_le Nat.zero_lt_two, ← Int.ofNat_le, Int.natCast_mul, Int.ofNat_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n m : ℕ
rw : m * 2 ≤ n ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
rw₁ : LE.le (α := ℤ) (↑(m * 2) : ℤ) (↑n : ℤ) ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
rw₂ : HMul.hMul (α := ℤ) (↑m : ℤ) (↑2 : ℤ) ≤ (↑n : ℤ) ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
⊢ m ≤ n / 2 ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
have rw₃ : HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ) ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
Tactic: rw [Nat.le_div_iff_mul_le Nat.zero_lt_two, ← Int.ofNat_le, Int.natCast_mul, Int.ofNat_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
⊢ leRec (motive := motive) refl le_succ_of_le ⋯ = refl
have zero : ∀ {motive : (m : ℕ) → 0 ≤ m → Sort u_1} (refl : motive 0 sorry)
  (le_succ_of_le : ⦃k : ℕ⦄ → (h : 0 ≤ k) → motive k h → motive (k + 1) sorry),
  leRec (motive := motive) refl le_succ_of_le sorry = refl
Tactic: cases n
Cleared hypotheses: n, motive, refl, le_succ_of_le
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
zero :
  ∀ {motive : (m : ℕ) → 0 ≤ m → Sort u_1} (refl : motive 0 ⋯)
    (le_succ_of_le : ⦃k : ℕ⦄ → (h : 0 ≤ k) → motive k h → motive (k + 1) ⋯),
    leRec (motive := motive) refl le_succ_of_le ⋯ = refl
⊢ leRec (motive := motive) refl le_succ_of_le ⋯ = refl
have succ : ∀ (n : ℕ) {motive : (m : ℕ) → n + 1 ≤ m → Sort u_1} (refl : motive (n + 1) sorry)
  (le_succ_of_le : ⦃k : ℕ⦄ → (h : n + 1 ≤ k) → motive k h → motive (k + 1) sorry),
  leRec (motive := motive) refl le_succ_of_le sorry = refl
Tactic: cases n
Cleared hypotheses: n, motive, refl, le_succ_of_le
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
| leRec (motive := motive) refl le_succ_of_le h2 = le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)
have lhs : leRec (motive := motive) refl le_succ_of_le h2
Tactic: lhs
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
| leRec (motive := motive) refl le_succ_of_le h2
have rw : le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)
Tactic: rw [leRec, Or.by_cases, dif_pos h1]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
| leRec (motive := motive) refl le_succ_of_le h2 = le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)
have rw : le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)
Tactic: lhs
    rw [leRec, Or.by_cases, dif_pos h1]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
⊢ leRec (motive := motive) refl le_succ_of_le h2 = le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)
have conv : leRec (motive := motive) refl le_succ_of_le h2 = le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)
Tactic: conv =>
    lhs
    rw [leRec, Or.by_cases, dif_pos h1]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
conv :
  leRec (motive := motive) refl le_succ_of_le h2 = le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)
⊢ leRec (motive := motive) refl le_succ_of_le h2 = le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)
have conv₁ : le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1) =
  le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)
Tactic: conv =>
    lhs
    rw [leRec, Or.by_cases, dif_pos h1]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
⊢ leRec (motive := motive) refl le_succ_of_le ⋯ = le_succ_of_le ⋯ refl
have rw : le_succ_of_le sorry (leRec (motive := motive) refl le_succ_of_le sorry) = le_succ_of_le sorry refl
Tactic: rw [leRec_succ, leRec_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
rw : le_succ_of_le ⋯ (leRec (motive := motive) refl le_succ_of_le ⋯) = le_succ_of_le ⋯ refl
⊢ leRec (motive := motive) refl le_succ_of_le ⋯ = le_succ_of_le ⋯ refl
have h1 : n ≤ n
Tactic: rw [leRec_succ, leRec_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
rw : le_succ_of_le ⋯ (leRec (motive := motive) refl le_succ_of_le ⋯) = le_succ_of_le ⋯ refl
h1 : n ≤ n
⊢ leRec (motive := motive) refl le_succ_of_le ⋯ = le_succ_of_le ⋯ refl
have rw₁ : le_succ_of_le sorry refl = le_succ_of_le sorry refl
Tactic: rw [leRec_succ, leRec_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
⊢ leRec (motive := motive) refl le_succ_of_le ⋯ =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) ⋯
have refl₁ : leRec (motive := motive) refl le_succ_of_le sorry =
  leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x sorry) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm
Tactic: rw [leRec_self]