awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n p : ℕ
hp : Prime p
hdvd : p ∣ n
hn : n ≠ 0
⊢ p ∈ n.primeFactors

Tactic:
Nat.mem_primeFactors.mpr ⟨hp, hdvd, hn⟩

Premises used: Iff.mpr, And.intro, Nat.mem_primeFactors
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n p : ℕ
hp : Prime p
hdvd : p ∣ n
inst : NeZero n
⊢ p ∈ n.primeFactors

Tactic:
hp.mem_primeFactors hdvd (NeZero.ne n)

Premises used: Nat.Prime.mem_primeFactors, NeZero.ne
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
p : ℕ
hp : Prime p
⊢ p ∈ p.primeFactors

Tactic:
hp.mem_primeFactors p.dvd_refl hp.ne_zero

Premises used: Nat.Prime.mem_primeFactors, Nat.Prime.ne_zero, Nat.dvd_refl
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
simp : ∀ ⦃x : ℕ⦄, Prime x → x ∣ m → m ≠ 0 → Prime x ∧ x ∣ n ∧ n ≠ 0
⊢ m.primeFactors ⊆ n.primeFactors

Tactic:
simp only [subset_iff, mem_primeFactors, and_imp]

Premises used: and_imp, Finset.subset_iff, Nat.mem_primeFactors
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ ∀ ⦃x : ℕ⦄, Prime x → x ∣ m → m ≠ 0 → Prime x ∧ x ∣ n ∧ n ≠ 0

Tactic:
fun p hp hpm _ ↦ ⟨hp, hpm.trans hmn, hn⟩

Premises used: And.intro, Dvd.dvd.trans
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ ∀ ⦃x : ℕ⦄, Prime x → x ∣ m → m ≠ 0 → Prime x ∧ x ∣ n ∧ n ≠ 0

Tactic:
exact fun p hp hpm _ ↦ ⟨hp, hpm.trans hmn, hn⟩
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n p : ℕ
⊢ p ∈ n.primeFactors ↔ p ∈ n.primeFactorsList

Tactic:
simp only [primeFactors, List.mem_toFinset]

Premises used: List.mem_toFinset, Nat.primeFactors
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n p : ℕ
hp : p ∈ n.primeFactors
⊢ Prime p

Tactic:
(mem_primeFactors.1 hp).1

Premises used: And.left, Iff.mp, Nat.mem_primeFactors
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n p : ℕ
hp : p ∈ n.primeFactors
⊢ p ∣ n

Tactic:
(mem_primeFactors.1 hp).2.1

Premises used: And.right, And.left, Iff.mp, Nat.mem_primeFactors
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n p : ℕ
hp : p ∈ n.primeFactors
⊢ 0 < p

Tactic:
(prime_of_mem_primeFactors hp).pos

Premises used: Nat.Prime.pos, Nat.prime_of_mem_primeFactors
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n p : ℕ
h : p ∈ n.primeFactors
⊢ p ≤ n

Tactic:
le_of_dvd (mem_primeFactors.1 h).2.2.bot_lt <| dvd_of_mem_primeFactors h

Premises used: Nat.dvd_of_mem_primeFactors, And.right, Iff.mp, Nat.le_of_dvd, Nat.mem_primeFactors, Ne.bot_lt
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
h : ∀ (a : ℕ), a ∈ primeFactors 0 ↔ Membership.mem (γ := Finset ℕ) ∅ a
⊢ primeFactors 0 = ∅

Tactic:
ext
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
a : ℕ
⊢ a ∈ primeFactors 0 ↔ Membership.mem (γ := Finset ℕ) ∅ a

Tactic:
simp
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
h : ∀ (a : ℕ), a ∈ primeFactors 1 ↔ Membership.mem (γ := Finset ℕ) ∅ a
⊢ primeFactors 1 = ∅

Tactic:
ext
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
a : ℕ
⊢ a ∈ primeFactors 1 ↔ Membership.mem (γ := Finset ℕ) ∅ a

Tactic:
simpa using Prime.ne_one

Premises used: Nat.Prime.ne_one
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n : ℕ
mp : n.primeFactors = ∅ → n = 0 ∨ n = 1
mpr : n = 0 ∨ n = 1 → n.primeFactors = ∅
⊢ n.primeFactors = ∅ ↔ n = 0 ∨ n = 1

Tactic:
constructor
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n : ℕ
mp : n ≠ 0 ∧ n ≠ 1 → n.primeFactors.Nonempty
⊢ n.primeFactors = ∅ → n = 0 ∨ n = 1

Tactic:
contrapose!
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n : ℕ
hn : n ≠ 0 ∧ n ≠ 1
mp : ∀ (p : ℕ) (hp : Prime p) (hpn : p ∣ n), n.primeFactors.Nonempty
⊢ n.primeFactors.Nonempty

Tactic:
obtain ⟨p, hp, hpn⟩ := exists_prime_and_dvd hn.2

Premises used: Nat.exists_prime_and_dvd, And.right
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n : ℕ
hn : n ≠ 0 ∧ n ≠ 1
p : ℕ
hp : Prime p
hpn : p ∣ n
⊢ n.primeFactors.Nonempty

Tactic:
⟨_, mem_primeFactors.2 ⟨hp, hpn, hn.1⟩⟩

Premises used: Iff.mpr, And.left, And.intro, Exists.intro, Finset.Nonempty, Nat.mem_primeFactors
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n : ℕ
hn : n ≠ 0 ∧ n ≠ 1
p : ℕ
hp : Prime p
hpn : p ∣ n
⊢ n.primeFactors.Nonempty

Tactic:
exact ⟨_, mem_primeFactors.2 ⟨hp, hpn, hn.1⟩⟩
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
⊢ primeFactors 0 = ∅

Tactic:
simp
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
⊢ primeFactors 1 = ∅

Tactic:
simp
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n : ℕ
contrapose! : n.primeFactors = ∅ ↔ n ≤ 1
⊢ n.primeFactors.Nonempty ↔ 1 < n

Tactic:
contrapose!
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n : ℕ
rw : n = 0 ∨ n = 1 ↔ n ≤ 1
rw₁ rw₂ : n = 0 ∨ n = 1 ↔ n = 0 ∨ n = 1
⊢ n.primeFactors = ∅ ↔ n ≤ 1

Tactic:
rw [primeFactors_eq_empty, Nat.le_one_iff_eq_zero_or_eq_one]

Premises used: Nat.le_one_iff_eq_zero_or_eq_one, Nat.primeFactors_eq_empty
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
p : ℕ
hp : Prime p
⊢ p.primeFactors = {p}

Tactic:
simp [Nat.primeFactors, primeFactorsList_prime hp]

Premises used: Nat.primeFactorsList_prime, Nat.primeFactors
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (a_1 : ℕ), a_1 ∈ (a * b).primeFactors ↔ a_1 ∈ a.primeFactors ∪ b.primeFactors
⊢ (a * b).primeFactors = a.primeFactors ∪ b.primeFactors

Tactic:
ext
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a_1 : ℕ
⊢ a_1 ∈ (a * b).primeFactors ↔ a_1 ∈ a.primeFactors ∪ b.primeFactors

Tactic:
simp only [Finset.mem_union, mem_primeFactors_iff_mem_primeFactorsList,
    mem_primeFactorsList_mul ha hb]

Premises used: Nat.mem_primeFactors_iff_mem_primeFactorsList, Finset.mem_union, Nat.mem_primeFactorsList_mul
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
a b : ℕ
hab : a.Coprime b
⊢ (a * b).primeFactors = a.primeFactors ∪ b.primeFactors

Tactic:
(List.toFinset.ext <| mem_primeFactorsList_mul_of_coprime hab).trans <| List.toFinset_union _ _

Premises used: List.toFinset.ext, Nat.mem_primeFactorsList_mul_of_coprime, Nat.primeFactors, List.toFinset_union, Eq.trans
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.gcd b).primeFactors = a.primeFactors ∩ b.primeFactors

Tactic:
grind [dvd_gcd_iff]

Premises used: Nat.dvd_gcd_iff
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ Disjoint a.primeFactors b.primeFactors ↔ a.Coprime b

Tactic:
simp [disjoint_iff_inter_eq_empty, coprime_iff_gcd_eq_one, ← primeFactors_gcd,
    ha, hb]

Premises used: Nat.primeFactors_gcd, Finset.disjoint_iff_inter_eq_empty, Nat.coprime_iff_gcd_eq_one
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
a b : ℕ
hab : a.Coprime b
⊢ Disjoint a.primeFactors b.primeFactors

Tactic:
List.disjoint_toFinset_iff_disjoint.2 <| coprime_primeFactorsList_disjoint hab

Premises used: Iff.mpr, List.disjoint_toFinset_iff_disjoint, Nat.primeFactors, Nat.coprime_primeFactorsList_disjoint
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n k : ℕ
inl : (HPow.hPow (α := ℕ) 0 (k + 1)).primeFactors = primeFactors 0
inr : ∀ (hn : n ≠ 0), (n ^ (k + 1)).primeFactors = n.primeFactors
⊢ (n ^ (k + 1)).primeFactors = n.primeFactors

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
k : ℕ
⊢ (HPow.hPow (α := ℕ) 0 (k + 1)).primeFactors = primeFactors 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n : ℕ
hn : n ≠ 0
⊢ (n ^ HAdd.hAdd (α := ℕ) 0 1).primeFactors = n.primeFactors

Tactic:
simp
-- Module: Mathlib.Data.Nat.PrimeFin
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
inr₃ inr₄ : n.primeFactors = n.primeFactors
⊢ (n ^ (k + 1 + 1)).primeFactors = n.primeFactors

Tactic:
rw [pow_succ', primeFactors_mul hn (pow_ne_zero _ hn), ih, Finset.union_idempotent]

Premises used: Nat.pow_succ', pow_ne_zero, Finset.union_idempotent, Nat.primeFactors_mul
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n k : ℕ
hn : n ≠ 0
inr : (n ^ HAdd.hAdd (α := ℕ) 0 1).primeFactors = n.primeFactors
inr₁ : ∀ (k : ℕ) (ih : (n ^ (k + 1)).primeFactors = n.primeFactors), (n ^ (k + 1 + 1)).primeFactors = n.primeFactors
⊢ (n ^ (k + 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]

Premises used: Nat.pow_succ', pow_ne_zero, Finset.union_idempotent, Nat.zero, Nat.primeFactors_mul, Nat.succ
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
k n : ℕ
hk : k ≠ 0
zero : ∀ (hk : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) n 0).primeFactors = n.primeFactors
succ : ∀ (n_1 : ℕ) (hk : n_1 + 1 ≠ 0), (n ^ (n_1 + 1)).primeFactors = n.primeFactors
⊢ (n ^ k).primeFactors = n.primeFactors

Tactic:
cases k
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n : ℕ
hk : Ne (α := ℕ) 0 0
⊢ (HPow.hPow (β := ℕ) n 0).primeFactors = n.primeFactors

Tactic:
simp at hk
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
n n_1 : ℕ
hk : n_1 + 1 ≠ 0
succ succ₁ : n.primeFactors = n.primeFactors
⊢ (n ^ (n_1 + 1)).primeFactors = n.primeFactors

Tactic:
rw [primeFactors_pow_succ]

Premises used: Nat.primeFactors_pow_succ
-- Module: Mathlib.Data.Nat.PrimeFin
Goal:
k p : ℕ
hk : k ≠ 0
hp : Prime p
⊢ (p ^ k).primeFactors = {p}

Tactic:
simp [primeFactors_pow p hk, hp]

Premises used: Nat.primeFactors_pow
-- Module: Mathlib.Data.Nat.Set
Goal:
h : ∀ (n : ℕ), n ∈ {0} ∪ range succ ↔ Membership.mem (γ := Set ℕ) univ n
⊢ {0} ∪ range succ = univ

Tactic:
ext n
-- Module: Mathlib.Data.Nat.Set
Goal:
n : ℕ
h : 0 ∈ {0} ∪ range succ ↔ Membership.mem (γ := Set ℕ) univ 0
h₁ : ∀ (n : ℕ), n + 1 ∈ {0} ∪ range succ ↔ Membership.mem (γ := Set ℕ) univ (n + 1)
⊢ n ∈ {0} ∪ range succ ↔ Membership.mem (γ := Set ℕ) univ n

Tactic:
cases n
-- Module: Mathlib.Data.Nat.Set
Goal:
⊢ 0 ∈ {0} ∪ range succ ↔ Membership.mem (γ := Set ℕ) univ 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Set
Goal:
n : ℕ
⊢ n + 1 ∈ {0} ∪ range succ ↔ Membership.mem (γ := Set ℕ) univ (n + 1)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Set
Goal:
h : 0 ∈ range succ ↔ Membership.mem (γ := Set ℕ) {i : ℕ | 0 < i} 0
h₁ : ∀ (i : ℕ), i + 1 ∈ range succ ↔ Membership.mem (γ := Set ℕ) {i : ℕ | 0 < i} (i + 1)
⊢ range succ = {i : ℕ | 0 < i}

Tactic:
ext (_ | i)
-- Module: Mathlib.Data.Nat.Set
Goal:
⊢ 0 ∈ range succ ↔ Membership.mem (γ := Set ℕ) {i : ℕ | 0 < i} 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Set
Goal:
i : ℕ
⊢ i + 1 ∈ range succ ↔ Membership.mem (γ := Set ℕ) {i : ℕ | 0 < i} (i + 1)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Set
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
rw₄ rw₅ : range f = range f
⊢ {f 0} ∪ range (f ∘ succ) = range f

Tactic:
rw [← image_singleton, range_comp, ← image_union, zero_union_range_succ, image_univ]

Premises used: Set.range_comp, Set.image_univ, Set.image_singleton, Nat.zero_union_range_succ, Set.image_union
-- Module: Mathlib.Data.Nat.Set
Goal:
α : Type u_2
x : α
f : ℕ → α → α
⊢ Eq (α := Set α) (range fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ α) x f n)
    ({rec (motive := fun (x : ℕ) ↦ α) x f 0} ∪ range ((fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ α) x f n) ∘ succ))

Tactic:
(range_of_succ (fun n => Nat.rec x f n : ℕ → α)).symm

Premises used: Nat.rec, Nat.range_of_succ, Eq.symm
-- Module: Mathlib.Data.Nat.Set
Goal:
α : Type u_2
x : α
f : ℕ → α → α
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
⊢ 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)

Tactic:
convert! (range_of_succ (fun n => Nat.rec x f n : ℕ → α)).symm using 4

Premises used: Nat.rec, Nat.range_of_succ, Eq.symm
-- Module: Mathlib.Data.Nat.Set
Goal:
α : Type u_2
x : α
f : ℕ → α → α
x_1 : ℕ
h : rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) x_1 = f x_1 (rec (motive := fun (x : ℕ) ↦ α) 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

Tactic:
dsimp
-- Module: Mathlib.Data.Nat.Set
Goal:
α : Type u_2
x : α
f : ℕ → α → α
⊢ rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) 0 = f 0 (rec (motive := fun (x : ℕ) ↦ α) x f 0)

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Set
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)
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))
⊢ rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) (n + 1) = f (n + 1) (rec (motive := fun (x : ℕ) ↦ α) x f (n + 1))

Tactic:
dsimp at ihn ⊢
-- Module: Mathlib.Data.Nat.Set
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)
h 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))
⊢ 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:
rw [ihn]
-- Module: Mathlib.Data.Nat.Set
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)
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))
⊢ rec (motive := fun (x : ℕ) ↦ α) (f 0 x) (f ∘ succ) n = f n (rec (motive := fun (x : ℕ) ↦ α) x f n)

Tactic:
induction n with
  | zero => rfl
  | succ n ihn => dsimp at ihn ⊢; rw [ihn]

Premises used: Nat.zero, Nat.succ
-- Module: Mathlib.Data.Nat.Set
Goal:
α : Type u_2
x : α
f : ℕ → α
⊢ (range fun (n : ℕ) ↦ casesOn (motive := fun (x : ℕ) ↦ α) n x f) = {x} ∪ range f

Tactic:
(range_of_succ _).symm

Premises used: Nat.range_of_succ, Eq.symm
-- Module: Mathlib.Data.Nat.Size
Goal:
m : ℕ
⊢ ∀ (n : ℕ), m <<< n = m * HPow.hPow (α := ℕ) 2 n

Tactic:
shiftLeft_eq _

Premises used: Nat.shiftLeft_eq
-- Module: Mathlib.Data.Nat.Size
Goal:
m : ℕ
⊢ shiftLeft' true m 0 + 1 = (m + 1) * HPow.hPow (α := ℕ) (β := ℕ) 2 0

Tactic:
simp [shiftLeft', Nat.pow_zero]

Premises used: Nat.pow_zero, Nat.shiftLeft'
-- Module: Mathlib.Data.Nat.Size
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)
rw₈ rw₉ : (m + 1) * (HPow.hPow (α := ℕ) 2 k * 2) = (m + 1) * (HPow.hPow (α := ℕ) 2 k * 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]

Premises used: Nat.mul_left_comm, Nat.pow_succ, Nat.mul_comm, Nat.shiftLeft', Nat.bit_val, Nat.mul_add_one, Nat.add_assoc, OfNat.ofNat, Bool.toNat_true
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
m : ℕ
h : m ≠ 0
n : ℕ
zero : shiftLeft' b m 0 ≠ 0
succ : ∀ (n : ℕ), shiftLeft' b m n ≠ 0 → shiftLeft' b m (n + 1) ≠ 0
⊢ shiftLeft' b m n ≠ 0

Tactic:
induction n
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
m : ℕ
h : m ≠ 0
⊢ shiftLeft' b m 0 ≠ 0

Tactic:
simp [shiftLeft', *]

Premises used: Nat.shiftLeft'
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
m : ℕ
h : m ≠ 0
n : ℕ
h_1 : shiftLeft' b m n ≠ 0
⊢ shiftLeft' b m (n + 1) ≠ 0

Tactic:
simp [shiftLeft', *]

Premises used: Nat.shiftLeft'
-- Module: Mathlib.Data.Nat.Size
Goal:
m n : ℕ
h : n.succ ≠ 0
⊢ shiftLeft' true m n.succ ≠ 0

Tactic:
simp [shiftLeft', bit]

Premises used: Nat.bit, Nat.shiftLeft'
-- Module: Mathlib.Data.Nat.Size
Goal:
⊢ size 0 = 0

Tactic:
rfl

Premises used: WellFounded.Nat.fix, dite, WellFounded.Nat.fix.go, Nat.binaryRec, rfl, Nat.size
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ (bit b n).size = n.size.succ

Tactic:
Nat.binaryRec_eq _ _ (.inr <| Nat.bit_ne_zero_iff.mp h)

Premises used: Iff.mp, Nat.bit_ne_zero_iff, Or.inr, Nat.size, Nat.binaryRec_eq
-- Module: Mathlib.Data.Nat.Size
Goal:
⊢ size 1 = 1

Tactic:
rfl

Premises used: WellFounded.Nat.fix, dite, WellFounded.Nat.fix.go, Nat.binaryRec, rfl, Nat.size
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
m : ℕ
h : shiftLeft' b m 0 ≠ 0
⊢ (shiftLeft' b m 0).size = m.size + 0

Tactic:
simp [shiftLeft']

Premises used: Nat.shiftLeft'
-- Module: Mathlib.Data.Nat.Size
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
succ : (shiftLeft' b m n).size.succ = (m.size + n).succ
⊢ (bit b (shiftLeft' b m n)).size = m.size + (n + 1)

Tactic:
rw [size_bit h, Nat.add_succ]

Premises used: Nat.size_bit, Nat.add_succ
-- Module: Mathlib.Data.Nat.Size
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
by_cases : ∀ (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

Tactic:
by_cases s0 : shiftLeft' b m n = 0

Premises used: Nat.shiftLeft'
-- Module: Mathlib.Data.Nat.Size
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
rw rw₁ : (m.size + n).succ = (m.size + n).succ
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ

Tactic:
rw [IH s0]
-- Module: Mathlib.Data.Nat.Size
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

Tactic:
case neg => rw [IH s0]
-- Module: Mathlib.Data.Nat.Size
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
pos : ∀ (h : ¬bit b 0 = 0) (s0 : shiftLeft' b m n = 0), (size 0).succ = (m.size + n).succ
⊢ (shiftLeft' b m n).size.succ = (m.size + n).succ

Tactic:
rw [s0] at h ⊢
-- Module: Mathlib.Data.Nat.Size
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
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
⊢ (size 0).succ = (m.size + n).succ

Tactic:
cases b
-- Module: Mathlib.Data.Nat.Size
Goal:
m n : ℕ
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:
absurd rfl h

Premises used: absurd, rfl
-- Module: Mathlib.Data.Nat.Size
Goal:
m n : ℕ
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:
exact absurd rfl h

Premises used: absurd, rfl
-- Module: Mathlib.Data.Nat.Size
Goal:
m n : ℕ
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
⊢ shiftLeft' true m n + 1 = 1

Tactic:
have : shiftLeft' true m n + 1 = 1 := congr_arg (· + 1) s0
-- Module: Mathlib.Data.Nat.Size
Goal:
m n : ℕ
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
this : shiftLeft' true m n + 1 = 1
⊢ (m + 1) * HPow.hPow (α := ℕ) 2 n = 1

Tactic:
rw [shiftLeft'_true_eq_mul_pow] at this

Premises used: Nat.shiftLeft'_true_eq_mul_pow
-- Module: Mathlib.Data.Nat.Size
Goal:
m n : ℕ
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
this : (m + 1) * HPow.hPow (α := ℕ) 2 n = 1
pos :
  ∀ (IH : ∀ (h : shiftLeft' true 0 n ≠ 0), (shiftLeft' true 0 n).size = size 0 + n) (s0 : shiftLeft' true 0 n = 0)
    (this : HAdd.hAdd (α := ℕ) 0 1 * HPow.hPow (α := ℕ) 2 n = 1), (size 0).succ = (size 0 + n).succ
⊢ (size 0).succ = (m.size + n).succ

Tactic:
obtain rfl := succ.inj (eq_one_of_dvd_one ⟨_, this.symm⟩)

Premises used: Nat.succ.inj, Exists.intro, Eq.symm, Nat.eq_one_of_dvd_one, rfl
-- Module: Mathlib.Data.Nat.Size
Goal:
n : ℕ
h : ¬bit true 0 = 0
IH : ∀ (h : shiftLeft' true 0 n ≠ 0), (shiftLeft' true 0 n).size = size 0 + n
s0 : shiftLeft' true 0 n = 0
this : HAdd.hAdd (α := ℕ) 0 1 * HPow.hPow (α := ℕ) 2 n = 1
⊢ n = 0

Tactic:
simp only [Nat.zero_add, Nat.one_mul, Nat.pow_eq_one, succ_ne_self, false_or] at this

Premises used: Nat.succ_ne_self, Nat.pow_eq_one, false_or, Nat.zero_add, Nat.one_mul
-- Module: Mathlib.Data.Nat.Size
Goal:
n : ℕ
h : ¬bit true 0 = 0
IH : ∀ (h : shiftLeft' true 0 n ≠ 0), (shiftLeft' true 0 n).size = size 0 + n
s0 : shiftLeft' true 0 n = 0
this : n = 0
pos : (size 0).succ = (size 0 + 0).succ
pos₁ pos₂ : (size 0).succ = (size 0).succ
⊢ (size 0).succ = (size 0 + n).succ

Tactic:
rw [this, Nat.add_zero]

Premises used: Nat.add_zero
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
m n : ℕ
h : shiftLeft' b m n ≠ 0
zero : ∀ (h : shiftLeft' b m 0 ≠ 0), (shiftLeft' b m 0).size = m.size + 0
succ :
  ∀ (n : ℕ) (IH : ∀ (h : shiftLeft' b m n ≠ 0), (shiftLeft' b m n).size = m.size + n) (h : shiftLeft' b m (n + 1) ≠ 0),
    (shiftLeft' b m (n + 1)).size = m.size + (n + 1)
⊢ (shiftLeft' b m n).size = m.size + n

Tactic:
induction n with
  | zero => simp [shiftLeft']
  | succ n IH =>
    simp only [shiftLeft', ne_eq] at h ⊢
    rw [size_bit h, Nat.add_succ]
    by_cases s0 : shiftLeft' b m n = 0
    case neg => rw [IH s0]
    rw [s0] at h ⊢
    cases b; · exact absurd rfl h
    have : shiftLeft' true m n + 1 = 1 := congr_arg (· + 1) s0
    rw [shiftLeft'_true_eq_mul_pow] at this
    obtain rfl := succ.inj (eq_one_of_dvd_one ⟨_, this.symm⟩)
    simp only [Nat.zero_add, Nat.one_mul, Nat.pow_eq_one, succ_ne_self, false_or] at this
    rw [this, Nat.add_zero]

Premises used: Nat.succ_ne_self, Nat.pow_eq_one, false_or, ne_eq, absurd, Nat.shiftLeft', Nat.add_succ, Nat.zero, Nat.add_zero, Nat.shiftLeft'_true_eq_mul_pow, Nat.zero_add, Nat.succ, Nat.one_mul, rfl
-- Module: Mathlib.Data.Nat.Size
Goal:
m : ℕ
h : m ≠ 0
n : ℕ
⊢ (m <<< n).size = m.size + n

Tactic:
simp only [size_shiftLeft' (shiftLeft'_ne_zero_left _ h _), ← shiftLeft'_false]

Premises used: Nat.shiftLeft'_false, Nat.size_shiftLeft', Nat.shiftLeft'_ne_zero_left
-- Module: Mathlib.Data.Nat.Size
Goal:
⊢ 0 < HPow.hPow (α := ℕ) 2 (size 0)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
n : ℕ
h : n = 0 → b = true
IH : n < HPow.hPow (α := ℕ) 2 n.size
⊢ bit b n ≠ 0

Tactic:
rw [← Nat.bit_ne_zero_iff] at h

Premises used: Nat.bit_ne_zero_iff
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
n : ℕ
h : n = 0 → b = true
IH : n < HPow.hPow (α := ℕ) 2 n.size
h₁ : bit b n ≠ 0
⊢ n < HPow.hPow (α := ℕ) 2 n.size

Tactic:
rw [← Nat.bit_ne_zero_iff] at h

Premises used: Nat.bit_ne_zero_iff
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
n : ℕ
h : Nat.bit b n ≠ 0
IH : n < HPow.hPow (α := ℕ) 2 n.size
bit : Nat.bit b n < HPow.hPow (α := ℕ) 2 n.size.succ
bit₁ bit₂ bit₃ bit₄ : n < HPow.hPow (α := ℕ) 2 n.size
⊢ Nat.bit b n < HPow.hPow (α := ℕ) 2 (Nat.bit b n).size

Tactic:
rwa [size_bit h, bit_lt_two_pow_succ_iff]

Premises used: Nat.size_bit, Nat.bit_lt_two_pow_succ_iff