awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Int (hypothesis)
Goal:
p : ℕ
hp : Prime p
a b : ℤ
h : (↑p : ℤ) ∣ a * b
⊢ (↑p : ℤ) ∣ a ∨ (↑p : ℤ) ∣ b
have h₁ : p ∣ a.natAbs ∨ p ∣ b.natAbs
Tactic: rw [← Int.dvd_natAbs, Int.natCast_dvd_natCast, Int.natAbs_mul, hp.dvd_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Int (goal)
Goal:
p : ℕ
hp : Prime p
a b : ℤ
h : p ∣ a.natAbs ∨ p ∣ b.natAbs
⊢ (↑p : ℤ) ∣ a ∨ (↑p : ℤ) ∣ b
have rwa : Dvd.dvd (α := ℤ) (↑p : ℤ) (↑a.natAbs : ℤ) ∨ (↑p : ℤ) ∣ b
Tactic: rwa [← Int.dvd_natAbs, Int.natCast_dvd_natCast, ← Int.dvd_natAbs, Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Int (goal)
Goal:
p : ℕ
hp : Prime p
a b : ℤ
h : p ∣ a.natAbs ∨ p ∣ b.natAbs
rwa : Dvd.dvd (α := ℤ) (↑p : ℤ) (↑a.natAbs : ℤ) ∨ (↑p : ℤ) ∣ b
⊢ (↑p : ℤ) ∣ a ∨ (↑p : ℤ) ∣ b
have rwa₁ : p ∣ a.natAbs ∨ (↑p : ℤ) ∣ b
Tactic: rwa [← Int.dvd_natAbs, Int.natCast_dvd_natCast, ← Int.dvd_natAbs, Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Int (goal)
Goal:
p : ℕ
hp : Prime p
a b : ℤ
h : p ∣ a.natAbs ∨ p ∣ b.natAbs
rwa : Dvd.dvd (α := ℤ) (↑p : ℤ) (↑a.natAbs : ℤ) ∨ (↑p : ℤ) ∣ b
rwa₁ : p ∣ a.natAbs ∨ (↑p : ℤ) ∣ b
⊢ (↑p : ℤ) ∣ a ∨ (↑p : ℤ) ∣ b
have rwa₂ : p ∣ a.natAbs ∨ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑b.natAbs : ℤ)
Tactic: rwa [← Int.dvd_natAbs, Int.natCast_dvd_natCast, ← Int.dvd_natAbs, Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Int (hypothesis)
Goal:
p q m n : ℕ
hp : Prime p
hq : Prime q
h : p ^ (m + 1) = q ^ (n + 1)
⊢ p = q ∧ m = n
have H : p = q
Tactic: have H := dvd_antisymm (Prime.dvd_of_dvd_pow hp <| h ▸ dvd_pow_self p (succ_ne_zero m))
    (Prime.dvd_of_dvd_pow hq <| h.symm ▸ dvd_pow_self q (succ_ne_zero n))
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Int (goal)
Goal:
p q m n : ℕ
hp : Prime p
hq : Prime q
hm : m ≠ 0
hn : n ≠ 0
h : p ^ m = q ^ n
⊢ p = q ∧ m = n
have obtain : ∀ (m : ℕ) (hm : m + 1 ≠ 0) (h : p ^ (m + 1) = q ^ n), p = q ∧ m + 1 = n
Tactic: obtain ⟨m, rfl⟩ := exists_eq_add_one_of_ne_zero hm
Cleared hypotheses: m, hm, h
-- Lean 4 proof step from Mathlib.Data.Nat.Prime.Int (goal)
Goal:
p q n : ℕ
hp : Prime p
hq : Prime q
hn : n ≠ 0
m : ℕ
hm : m + 1 ≠ 0
h : p ^ (m + 1) = q ^ n
⊢ p = q ∧ m + 1 = n
have obtain : ∀ (n : ℕ) (hn : n + 1 ≠ 0) (h : p ^ (m + 1) = q ^ (n + 1)), p = q ∧ m + 1 = n + 1
Tactic: obtain ⟨n, rfl⟩ := exists_eq_add_one_of_ne_zero hn
Cleared hypotheses: n, hn, h
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n p : ℕ
⊢ p ∈ n.primeFactors ↔ Prime p ∧ p ∣ n ∧ n ≠ 0
have simp_rw : p ∈ n.primeFactorsList.toFinset ↔ Prime p ∧ p ∣ n ∧ n ≠ 0
Tactic: simp_rw [← toFinset_factors, List.mem_toFinset, mem_primeFactorsList']
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n p : ℕ
simp_rw : p ∈ n.primeFactorsList.toFinset ↔ Prime p ∧ p ∣ n ∧ n ≠ 0
⊢ p ∈ n.primeFactors ↔ Prime p ∧ p ∣ n ∧ n ≠ 0
have simp_rw₁ : p ∈ n.primeFactorsList ↔ Prime p ∧ p ∣ n ∧ n ≠ 0
Tactic: simp_rw [← toFinset_factors, List.mem_toFinset, mem_primeFactorsList']
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ m.primeFactors ⊆ n.primeFactors
have simp : ∀ ⦃x : ℕ⦄, Prime x → x ∣ m → m ≠ 0 → Prime x ∧ x ∣ n ∧ n ≠ 0
Tactic: simp only [subset_iff, mem_primeFactors, and_imp]
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
⊢ primeFactors 0 = ∅
have h : ∀ (a : ℕ), a ∈ primeFactors 0 ↔ Membership.mem (γ := Finset ℕ) ∅ a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
⊢ primeFactors 1 = ∅
have h : ∀ (a : ℕ), a ∈ primeFactors 1 ↔ Membership.mem (γ := Finset ℕ) ∅ a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n : ℕ
⊢ n.primeFactors = ∅ ↔ n = 0 ∨ n = 1
have mp : n.primeFactors = ∅ → n = 0 ∨ n = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n : ℕ
mp : n.primeFactors = ∅ → n = 0 ∨ n = 1
⊢ n.primeFactors = ∅ ↔ n = 0 ∨ n = 1
have mpr : n = 0 ∨ n = 1 → n.primeFactors = ∅
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n : ℕ
⊢ n.primeFactors = ∅ → n = 0 ∨ n = 1
have mp : n ≠ 0 ∧ n ≠ 1 → n.primeFactors.Nonempty
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n : ℕ
hn : n ≠ 0 ∧ n ≠ 1
⊢ n.primeFactors.Nonempty
have mp : ∀ (p : ℕ) (hp : Prime p) (hpn : p ∣ n), n.primeFactors.Nonempty
Tactic: obtain ⟨p, hp, hpn⟩ := exists_prime_and_dvd hn.2
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n : ℕ
⊢ n.primeFactors.Nonempty ↔ 1 < n
have contrapose! : n.primeFactors = ∅ ↔ n ≤ 1
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n : ℕ
⊢ n.primeFactors = ∅ ↔ n ≤ 1
have rw : n = 0 ∨ n = 1 ↔ n ≤ 1
Tactic: rw [primeFactors_eq_empty, Nat.le_one_iff_eq_zero_or_eq_one]
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n : ℕ
rw : n = 0 ∨ n = 1 ↔ n ≤ 1
⊢ n.primeFactors = ∅ ↔ n ≤ 1
have rw₁ : n = 0 ∨ n = 1 ↔ n = 0 ∨ n = 1
Tactic: rw [primeFactors_eq_empty, Nat.le_one_iff_eq_zero_or_eq_one]
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b).primeFactors = a.primeFactors ∪ b.primeFactors
have h : ∀ (a_1 : ℕ), a_1 ∈ (a * b).primeFactors ↔ a_1 ∈ a.primeFactors ∪ b.primeFactors
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n k : ℕ
⊢ (n ^ (k + 1)).primeFactors = n.primeFactors
have inl : (HPow.hPow (α := ℕ) 0 (k + 1)).primeFactors = primeFactors 0
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n k : ℕ
inl : (HPow.hPow (α := ℕ) 0 (k + 1)).primeFactors = primeFactors 0
⊢ (n ^ (k + 1)).primeFactors = n.primeFactors
have inr : ∀ (hn : n ≠ 0), (n ^ (k + 1)).primeFactors = n.primeFactors
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
ih : (n ^ (k + 1)).primeFactors = n.primeFactors
⊢ (n ^ (k + 1 + 1)).primeFactors = n.primeFactors
have inr : (n * n ^ (k + 1)).primeFactors = n.primeFactors
Tactic: rw [pow_succ', primeFactors_mul hn (pow_ne_zero _ hn), ih, Finset.union_idempotent]
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
ih : (n ^ (k + 1)).primeFactors = n.primeFactors
inr : (n * n ^ (k + 1)).primeFactors = n.primeFactors
⊢ (n ^ (k + 1 + 1)).primeFactors = n.primeFactors
have inr₁ : n.primeFactors ∪ (n ^ (k + 1)).primeFactors = n.primeFactors
Tactic: rw [pow_succ', primeFactors_mul hn (pow_ne_zero _ hn), ih, Finset.union_idempotent]
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
ih : (n ^ (k + 1)).primeFactors = n.primeFactors
inr : (n * n ^ (k + 1)).primeFactors = n.primeFactors
inr₁ : n.primeFactors ∪ (n ^ (k + 1)).primeFactors = n.primeFactors
⊢ (n ^ (k + 1 + 1)).primeFactors = n.primeFactors
have inr₂ : n.primeFactors ∪ n.primeFactors = n.primeFactors
Tactic: rw [pow_succ', primeFactors_mul hn (pow_ne_zero _ hn), ih, Finset.union_idempotent]
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
ih : (n ^ (k + 1)).primeFactors = n.primeFactors
inr : (n * n ^ (k + 1)).primeFactors = n.primeFactors
inr₁ : n.primeFactors ∪ (n ^ (k + 1)).primeFactors = n.primeFactors
inr₂ : n.primeFactors ∪ n.primeFactors = n.primeFactors
⊢ (n ^ (k + 1 + 1)).primeFactors = n.primeFactors
have inr₃ : n.primeFactors = n.primeFactors
Tactic: rw [pow_succ', primeFactors_mul hn (pow_ne_zero _ hn), ih, Finset.union_idempotent]
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n k : ℕ
hn : n ≠ 0
⊢ (n ^ (k + 1)).primeFactors = n.primeFactors
have inr : (n ^ HAdd.hAdd (α := ℕ) 0 1).primeFactors = n.primeFactors
Tactic: induction k with
  | zero => simp
  | succ k ih => rw [pow_succ', primeFactors_mul hn (pow_ne_zero _ hn), ih, Finset.union_idempotent]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n k : ℕ
hn : n ≠ 0
inr : (n ^ HAdd.hAdd (α := ℕ) 0 1).primeFactors = n.primeFactors
⊢ (n ^ (k + 1)).primeFactors = n.primeFactors
have inr₁ : ∀ (k : ℕ) (ih : (n ^ (k + 1)).primeFactors = n.primeFactors), (n ^ (k + 1 + 1)).primeFactors = n.primeFactors
Tactic: induction k with
  | zero => simp
  | succ k ih => rw [pow_succ', primeFactors_mul hn (pow_ne_zero _ hn), ih, Finset.union_idempotent]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
k n : ℕ
hk : k ≠ 0
⊢ (n ^ k).primeFactors = n.primeFactors
have zero : ∀ (hk : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) n 0).primeFactors = n.primeFactors
Tactic: cases k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
k n : ℕ
hk : k ≠ 0
zero : ∀ (hk : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) n 0).primeFactors = n.primeFactors
⊢ (n ^ k).primeFactors = n.primeFactors
have succ : ∀ (n_1 : ℕ) (hk : n_1 + 1 ≠ 0), (n ^ (n_1 + 1)).primeFactors = n.primeFactors
Tactic: cases k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Data.Nat.PrimeFin (goal)
Goal:
n n_1 : ℕ
hk : n_1 + 1 ≠ 0
⊢ (n ^ (n_1 + 1)).primeFactors = n.primeFactors
have succ : n.primeFactors = n.primeFactors
Tactic: rw [primeFactors_pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Set (goal)
Goal:
⊢ {0} ∪ range succ = univ
have h : ∀ (n : ℕ), n ∈ {0} ∪ range succ ↔ Membership.mem (γ := Set ℕ) univ n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Data.Nat.Set (goal)
Goal:
n : ℕ
⊢ n ∈ {0} ∪ range succ ↔ Membership.mem (γ := Set ℕ) univ n
have h : 0 ∈ {0} ∪ range succ ↔ Membership.mem (γ := Set ℕ) univ 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Set (goal)
Goal:
n : ℕ
h : 0 ∈ {0} ∪ range succ ↔ Membership.mem (γ := Set ℕ) univ 0
⊢ n ∈ {0} ∪ range succ ↔ Membership.mem (γ := Set ℕ) univ n
have h₁ : ∀ (n : ℕ), n + 1 ∈ {0} ∪ range succ ↔ Membership.mem (γ := Set ℕ) univ (n + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Set (goal)
Goal:
⊢ range succ = {i : ℕ | 0 < i}
have h : 0 ∈ range succ ↔ Membership.mem (γ := Set ℕ) {i : ℕ | 0 < i} 0
Tactic: ext (_ | i)
-- Lean 4 proof step from Mathlib.Data.Nat.Set (goal)
Goal:
h : 0 ∈ range succ ↔ Membership.mem (γ := Set ℕ) {i : ℕ | 0 < i} 0
⊢ range succ = {i : ℕ | 0 < i}
have h₁ : ∀ (i : ℕ), i + 1 ∈ range succ ↔ Membership.mem (γ := Set ℕ) {i : ℕ | 0 < i} (i + 1)
Tactic: ext (_ | i)
-- Lean 4 proof step from Mathlib.Data.Nat.Set (goal)
Goal:
α : Type u_1
f : ℕ → α
⊢ {f 0} ∪ range (f ∘ succ) = range f
have rw : f '' {0} ∪ range (f ∘ succ) = range f
Tactic: rw [← image_singleton, range_comp, ← image_union, zero_union_range_succ, image_univ]
-- Lean 4 proof step from Mathlib.Data.Nat.Set (goal)
Goal:
α : Type u_1
f : ℕ → α
rw : f '' {0} ∪ range (f ∘ succ) = range f
⊢ {f 0} ∪ range (f ∘ succ) = range f
have rw₁ : f '' {0} ∪ f '' range succ = range f
Tactic: rw [← image_singleton, range_comp, ← image_union, zero_union_range_succ, image_univ]
-- Lean 4 proof step from Mathlib.Data.Nat.Set (goal)
Goal:
α : Type u_1
f : ℕ → α
rw : f '' {0} ∪ range (f ∘ succ) = range f
rw₁ : f '' {0} ∪ f '' range succ = range f
⊢ {f 0} ∪ range (f ∘ succ) = range f
have rw₂ : f '' ({0} ∪ range succ) = range f
Tactic: rw [← image_singleton, range_comp, ← image_union, zero_union_range_succ, image_univ]
-- Lean 4 proof step from Mathlib.Data.Nat.Set (goal)
Goal:
α : Type u_1
f : ℕ → α
rw : f '' {0} ∪ range (f ∘ succ) = range f
rw₁ : f '' {0} ∪ f '' range succ = range f
rw₂ : f '' ({0} ∪ range succ) = range f
⊢ {f 0} ∪ range (f ∘ succ) = range f
have rw₃ : f '' univ = range f
Tactic: rw [← image_singleton, range_comp, ← image_union, zero_union_range_succ, image_univ]
-- Lean 4 proof step from Mathlib.Data.Nat.Set (goal)
Goal:
α : Type u_1
f : ℕ → α
rw : f '' {0} ∪ range (f ∘ succ) = range f
rw₁ : f '' {0} ∪ f '' range succ = range f
rw₂ : f '' ({0} ∪ range succ) = range f
rw₃ : f '' univ = range f
⊢ {f 0} ∪ range (f ∘ succ) = range f
have rw₄ : range f = range f
Tactic: rw [← image_singleton, range_comp, ← image_union, zero_union_range_succ, image_univ]
-- Lean 4 proof step from Mathlib.Data.Nat.Set (goal)
Goal:
α : Type u_2
x : α
f : ℕ → α → α
⊢ Eq (α := Set α) (range fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ α) x f n)
    ({x} ∪ range fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) n)
have h : ∀ (x_1 : ℕ),
  rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) x_1 =
    ((fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ α) x f n) ∘ succ) x_1
Tactic: convert! (range_of_succ (fun n => Nat.rec x f n : ℕ → α)).symm using 4
-- Lean 4 proof step from Mathlib.Data.Nat.Set (goal)
Goal:
α : Type u_2
x : α
f : ℕ → α → α
x_1 : ℕ
⊢ rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) x_1 =
    ((fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ α) x f n) ∘ succ) x_1
have h : rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) x_1 = f x_1 (rec (motive := fun (x : ℕ) ↦ α) x f x_1)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.Nat.Set (goal)
Goal:
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) n = f n (rec (motive := fun (x : ℕ) ↦ α) x f n)
⊢ rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) (n + 1) = f (n + 1) (rec (motive := fun (x : ℕ) ↦ α) x f (n + 1))
have h : f (n + 1) (rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) n) =
  f (n + 1) (f n (rec (motive := fun (x : ℕ) ↦ α) x f n))
Tactic: dsimp at ihn ⊢
-- Lean 4 proof step from Mathlib.Data.Nat.Set (goal)
Goal:
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) n = f n (rec (motive := fun (x : ℕ) ↦ α) x f n)
⊢ f (n + 1) (rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) n) =
    f (n + 1) (f n (rec (motive := fun (x : ℕ) ↦ α) x f n))
have h : f (n + 1) (f n (rec (motive := fun (x : ℕ) ↦ α) x f n)) = f (n + 1) (f n (rec (motive := fun (x : ℕ) ↦ α) x f n))
Tactic: rw [ihn]
-- Lean 4 proof step from Mathlib.Data.Nat.Set (goal)
Goal:
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
⊢ rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) n = f n (rec (motive := fun (x : ℕ) ↦ α) x f n)
have h : rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) 0 = f 0 (rec (motive := fun (x : ℕ) ↦ α) x f 0)
Tactic: induction n with
  | zero => rfl
  | succ n ihn => dsimp at ihn ⊢; rw [ihn]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Set (goal)
Goal:
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
h : rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) 0 = f 0 (rec (motive := fun (x : ℕ) ↦ α) x f 0)
⊢ rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) n = f n (rec (motive := fun (x : ℕ) ↦ α) x f n)
have h₁ : ∀ (n : ℕ) (ihn : rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) n = f n (rec (motive := fun (x : ℕ) ↦ α) x f n)),
  rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) (n + 1) = f (n + 1) (rec (motive := fun (x : ℕ) ↦ α) x f (n + 1))
Tactic: induction n with
  | zero => rfl
  | succ n ihn => dsimp at ihn ⊢; rw [ihn]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
m k : ℕ
⊢ shiftLeft' true m (k + 1) + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
have rw : bit true (shiftLeft' true m k) + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
Tactic: rw [shiftLeft', bit_val, Bool.toNat_true, Nat.add_assoc, ← Nat.mul_add_one,
      shiftLeft'_true_eq_mul_pow m k, Nat.mul_left_comm, Nat.mul_comm 2, Nat.pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
m k : ℕ
rw : bit true (shiftLeft' true m k) + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
⊢ shiftLeft' true m (k + 1) + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
have rw₁ : 2 * shiftLeft' true m k + true.toNat + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
Tactic: rw [shiftLeft', bit_val, Bool.toNat_true, Nat.add_assoc, ← Nat.mul_add_one,
      shiftLeft'_true_eq_mul_pow m k, Nat.mul_left_comm, Nat.mul_comm 2, Nat.pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
m k : ℕ
rw : bit true (shiftLeft' true m k) + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₁ : 2 * shiftLeft' true m k + true.toNat + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
⊢ shiftLeft' true m (k + 1) + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
have rw₂ : 2 * shiftLeft' true m k + 1 + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
Tactic: rw [shiftLeft', bit_val, Bool.toNat_true, Nat.add_assoc, ← Nat.mul_add_one,
      shiftLeft'_true_eq_mul_pow m k, Nat.mul_left_comm, Nat.mul_comm 2, Nat.pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
m k : ℕ
rw : bit true (shiftLeft' true m k) + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₁ : 2 * shiftLeft' true m k + true.toNat + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₂ : 2 * shiftLeft' true m k + 1 + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₃ : 2 * shiftLeft' true m k + HAdd.hAdd (α := ℕ) 1 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
⊢ shiftLeft' true m (k + 1) + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
have rw₄ : 2 * (shiftLeft' true m k + 1) = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
Tactic: rw [shiftLeft', bit_val, Bool.toNat_true, Nat.add_assoc, ← Nat.mul_add_one,
      shiftLeft'_true_eq_mul_pow m k, Nat.mul_left_comm, Nat.mul_comm 2, Nat.pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
m k : ℕ
rw : bit true (shiftLeft' true m k) + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₁ : 2 * shiftLeft' true m k + true.toNat + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₂ : 2 * shiftLeft' true m k + 1 + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₃ : 2 * shiftLeft' true m k + HAdd.hAdd (α := ℕ) 1 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₄ : 2 * (shiftLeft' true m k + 1) = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
⊢ shiftLeft' true m (k + 1) + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
have rw₅ : 2 * ((m + 1) * HPow.hPow (α := ℕ) 2 k) = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
Tactic: rw [shiftLeft', bit_val, Bool.toNat_true, Nat.add_assoc, ← Nat.mul_add_one,
      shiftLeft'_true_eq_mul_pow m k, Nat.mul_left_comm, Nat.mul_comm 2, Nat.pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
m k : ℕ
rw : bit true (shiftLeft' true m k) + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₁ : 2 * shiftLeft' true m k + true.toNat + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₂ : 2 * shiftLeft' true m k + 1 + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₃ : 2 * shiftLeft' true m k + HAdd.hAdd (α := ℕ) 1 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₄ : 2 * (shiftLeft' true m k + 1) = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₅ : 2 * ((m + 1) * HPow.hPow (α := ℕ) 2 k) = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
⊢ shiftLeft' true m (k + 1) + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
have rw₆ : (m + 1) * (2 * HPow.hPow (α := ℕ) 2 k) = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
Tactic: rw [shiftLeft', bit_val, Bool.toNat_true, Nat.add_assoc, ← Nat.mul_add_one,
      shiftLeft'_true_eq_mul_pow m k, Nat.mul_left_comm, Nat.mul_comm 2, Nat.pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
m k : ℕ
rw : bit true (shiftLeft' true m k) + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₁ : 2 * shiftLeft' true m k + true.toNat + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₂ : 2 * shiftLeft' true m k + 1 + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₃ : 2 * shiftLeft' true m k + HAdd.hAdd (α := ℕ) 1 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₄ : 2 * (shiftLeft' true m k + 1) = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₅ : 2 * ((m + 1) * HPow.hPow (α := ℕ) 2 k) = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₆ : (m + 1) * (2 * HPow.hPow (α := ℕ) 2 k) = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
⊢ shiftLeft' true m (k + 1) + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
have rw₇ : (m + 1) * (HPow.hPow (α := ℕ) 2 k * 2) = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
Tactic: rw [shiftLeft', bit_val, Bool.toNat_true, Nat.add_assoc, ← Nat.mul_add_one,
      shiftLeft'_true_eq_mul_pow m k, Nat.mul_left_comm, Nat.mul_comm 2, Nat.pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
m k : ℕ
rw : bit true (shiftLeft' true m k) + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₁ : 2 * shiftLeft' true m k + true.toNat + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₂ : 2 * shiftLeft' true m k + 1 + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₃ : 2 * shiftLeft' true m k + HAdd.hAdd (α := ℕ) 1 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₄ : 2 * (shiftLeft' true m k + 1) = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₅ : 2 * ((m + 1) * HPow.hPow (α := ℕ) 2 k) = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₆ : (m + 1) * (2 * HPow.hPow (α := ℕ) 2 k) = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
rw₇ : (m + 1) * (HPow.hPow (α := ℕ) 2 k * 2) = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
⊢ shiftLeft' true m (k + 1) + 1 = (m + 1) * HPow.hPow (α := ℕ) 2 (k + 1)
have rw₈ : (m + 1) * (HPow.hPow (α := ℕ) 2 k * 2) = (m + 1) * (HPow.hPow (α := ℕ) 2 k * 2)
Tactic: rw [shiftLeft', bit_val, Bool.toNat_true, Nat.add_assoc, ← Nat.mul_add_one,
      shiftLeft'_true_eq_mul_pow m k, Nat.mul_left_comm, Nat.mul_comm 2, Nat.pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
b : Bool
m : ℕ
h : m ≠ 0
n : ℕ
⊢ shiftLeft' b m n ≠ 0
have zero : shiftLeft' b m 0 ≠ 0
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
b : Bool
m : ℕ
h : m ≠ 0
n : ℕ
zero : shiftLeft' b m 0 ≠ 0
⊢ shiftLeft' b m n ≠ 0
have succ : ∀ (n : ℕ), shiftLeft' b m n ≠ 0 → shiftLeft' b m (n + 1) ≠ 0
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
b : Bool
m n : ℕ
IH : ∀ (h : shiftLeft' b m n ≠ 0), (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
⊢ (bit b (shiftLeft' b m n)).size = m.size + (n + 1)
have succ : (shiftLeft' b m n).size.succ = (m.size + n).succ
Tactic: rw [size_bit h, Nat.add_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
b : Bool
m n : ℕ
IH : ∀ (h : shiftLeft' b m n ≠ 0), (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ
have pos : ∀ (s0 : shiftLeft' b m n = 0), (shiftLeft' b m n).size.succ = (m.size + n).succ
Tactic: by_cases s0 : shiftLeft' b m n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
b : Bool
m n : ℕ
IH : ∀ (h : shiftLeft' b m n ≠ 0), (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
pos : ∀ (s0 : shiftLeft' b m n = 0), (shiftLeft' b m n).size.succ = (m.size + n).succ
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ
have by_cases : ∀ (s0 : ¬shiftLeft' b m n = 0), (shiftLeft' b m n).size.succ = (m.size + n).succ
Tactic: by_cases s0 : shiftLeft' b m n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
b : Bool
m n : ℕ
IH : ∀ (h : shiftLeft' b m n ≠ 0), (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
s0 : ¬shiftLeft' b m n = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ
have rw : (m.size + n).succ = (m.size + n).succ
Tactic: rw [IH s0]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
b : Bool
m n : ℕ
IH : ∀ (h : shiftLeft' b m n ≠ 0), (shiftLeft' b m n).size = m.size + n
h : ¬bit b (shiftLeft' b m n) = 0
s0 : shiftLeft' b m n = 0
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ
have pos : ∀ (h : ¬bit b 0 = 0) (s0 : shiftLeft' b m n = 0), (size 0).succ = (m.size + n).succ
Tactic: rw [s0] at h ⊢
Cleared hypotheses: h, s0
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
b : Bool
m n : ℕ
IH : ∀ (h : shiftLeft' b m n ≠ 0), (shiftLeft' b m n).size = m.size + n
h : ¬bit b 0 = 0
s0 : shiftLeft' b m n = 0
⊢ (size 0).succ = (m.size + n).succ
have pos : ∀ (IH : ∀ (h : shiftLeft' false m n ≠ 0), (shiftLeft' false m n).size = m.size + n) (h : ¬bit false 0 = 0)
  (s0 : shiftLeft' false m n = 0), (size 0).succ = (m.size + n).succ
Tactic: cases b
Cleared hypotheses: b, IH, h, s0
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
b : Bool
m n : ℕ
IH : ∀ (h : shiftLeft' b m n ≠ 0), (shiftLeft' b m n).size = m.size + n
h : ¬bit b 0 = 0
s0 : shiftLeft' b m n = 0
pos :
  ∀ (IH : ∀ (h : shiftLeft' false m n ≠ 0), (shiftLeft' false m n).size = m.size + n) (h : ¬bit false 0 = 0)
    (s0 : shiftLeft' false m n = 0), (size 0).succ = (m.size + n).succ
⊢ (size 0).succ = (m.size + n).succ
have pos₁ : ∀ (IH : ∀ (h : shiftLeft' true m n ≠ 0), (shiftLeft' true m n).size = m.size + n) (h : ¬bit true 0 = 0)
  (s0 : shiftLeft' true m n = 0), (size 0).succ = (m.size + n).succ
Tactic: cases b
Cleared hypotheses: b, IH, h, s0