awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
inr : a ∣ HPow.hPow (α := ℕ) 0 n ↔ n.ceilRoot a ∣ 0
inr₁ : ∀ (hb : b ≠ 0), a ∣ b ^ n ↔ n.ceilRoot a ∣ b
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a n : ℕ
hn : n ≠ 0
ha : a ≠ 0
⊢ a ∣ HPow.hPow (α := ℕ) 0 n ↔ n.ceilRoot a ∣ 0

Tactic:
simp [hn]
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
hb : b ≠ 0
inr : a.factorization ≤ (b ^ n).factorization ↔ n.ceilRoot a ∣ b
inr₁ : a.factorization ≤ (b ^ n).factorization ↔ (n.ceilRoot a).factorization ≤ b.factorization
inr₂ : a.factorization ≤ n • b.factorization ↔ (n.ceilRoot a).factorization ≤ b.factorization
inr₃ :
  a.factorization ≤ n • b.factorization ↔
    @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
        a.factorization n ≤
      b.factorization
inr₄ inr₅ : a.factorization ≤ n • b.factorization ↔ a.factorization ≤ n • b.factorization
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b

Tactic:
rw [← factorization_le_iff_dvd ha (pow_ne_zero _ hb),
    ← factorization_le_iff_dvd (ceilRoot_ne_zero.2 ⟨hn, ha⟩) hb, factorization_pow,
    factorization_ceilRoot, ceilDiv_le_iff_le_smul (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)]

Premises used: Iff.mpr, ceilDiv_le_iff_le_smul, Nat.ceilRoot_ne_zero, pow_ne_zero, Nat.factorization_ceilRoot, Nat.factorization_le_iff_dvd, And.intro, Nat.factorization_pow, pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Factorization.Root
Goal:
a n : ℕ
hn : n ≠ 0
⊢ a ∣ n.ceilRoot a ^ n

Tactic:
(dvd_pow_iff_ceilRoot_dvd hn).2 dvd_rfl

Premises used: Iff.mpr, Nat.dvd_pow_iff_ceilRoot_dvd, dvd_rfl
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
⊢ fib 0 = 0

Tactic:
rfl

Premises used: Nat.fib, rfl
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
⊢ fib 1 = 1

Tactic:
rfl

Premises used: Nat.fib, rfl
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
⊢ fib 2 = 1

Tactic:
rfl

Premises used: Nat.fib, rfl
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
⊢ fib (n + 2) = fib n + fib (n + 1)

Tactic:
simp [fib, Function.iterate_succ_apply']

Premises used: Function.iterate_succ_apply', Nat.fib
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
zero : fib 0 ≤ fib (HAdd.hAdd (α := ℕ) 0 1)
succ : ∀ (n : ℕ), fib (n + 1) ≤ fib (n + 1 + 1)
⊢ fib n ≤ fib (n + 1)

Tactic:
cases n
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
⊢ fib 0 ≤ fib (HAdd.hAdd (α := ℕ) 0 1)

Tactic:
simp [fib_add_two]

Premises used: Nat.fib_add_two
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
⊢ fib (n + 1) ≤ fib (n + 1 + 1)

Tactic:
simp [fib_add_two]

Premises used: Nat.fib_add_two
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
⊢ Monotone fib

Tactic:
monotone_nat_of_le_succ fun _ => fib_le_fib_succ

Premises used: Nat.fib_le_fib_succ, monotone_nat_of_le_succ
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
⊢ fib (n + 2) = 0 ↔ n + 2 = 0

Tactic:
simp [fib_add_two, fib_eq_zero]

Premises used: Nat.fib_add_two
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
⊢ 0 < fib n ↔ 0 < n

Tactic:
simp [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
rw : fib n + fib (n + 1) - fib (n + 1) = fib n
rw₁ rw₂ : fib n = fib n
⊢ fib (n + 2) - fib (n + 1) = fib n

Tactic:
rw [fib_add_two, add_tsub_cancel_right]

Premises used: Nat.fib_add_two, add_tsub_cancel_right
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
hn : 2 ≤ n
rcases : ∀ (n : ℕ) (hn : 2 ≤ 2 + n), fib (2 + n) < fib (2 + n + 1)
⊢ fib n < fib (n + 1)

Tactic:
rcases exists_add_of_le hn with ⟨n, rfl⟩

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
hn : 2 ≤ 2 + n
rw : 0 < n + 1
⊢ fib (2 + n) < fib (2 + n + 1)

Tactic:
rw [← tsub_pos_iff_lt, add_comm 2, add_right_comm, fib_add_two, add_tsub_cancel_right, fib_pos]

Premises used: tsub_pos_iff_lt, Nat.fib_add_two, add_right_comm, Nat.fib_pos, add_comm, add_tsub_cancel_right, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
hn : 2 ≤ 2 + n
⊢ 0 < n + 1

Tactic:
succ_pos n

Premises used: Nat.succ_pos
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
hn : 2 ≤ 2 + n
⊢ 0 < n + 1

Tactic:
exact succ_pos n

Premises used: Nat.succ_pos
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
⊢ StrictMono (β := ℕ) fun (n : ℕ) ↦ fib (n + 2)

Tactic:
strictMono_nat_of_lt_succ fun n => ?_

Premises used: strictMono_nat_of_lt_succ
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
refine : ∀ (n : ℕ), fib (n + 2) < fib (n + 1 + 2)
⊢ StrictMono (β := ℕ) fun (n : ℕ) ↦ fib (n + 2)

Tactic:
refine strictMono_nat_of_lt_succ fun n => ?_

Premises used: strictMono_nat_of_lt_succ
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
⊢ fib (n + 2) < fib (n + 2 + 1)

Tactic:
fib_lt_fib_succ (self_le_add_left _ _)

Premises used: Nat.fib_lt_fib_succ, self_le_add_left
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
⊢ fib (n + 2) < fib (n + 2 + 1)

Tactic:
exact fib_lt_fib_succ (self_le_add_left _ _)

Premises used: Nat.fib_lt_fib_succ, self_le_add_left
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m : ℕ
hm : 2 ≤ m
⊢ fib m < fib 0 ↔ m < 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m : ℕ
hm : 2 ≤ m
⊢ fib m < fib 1 ↔ m < 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ Membership.mem (γ := Set ℕ) (Set.Ici 2) (n + 2)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
⊢ LE.le (α := ℕ) 5 5

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n_1 n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ n ≤ fib n

Tactic:
IH
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n_1 n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ LE.le (α := ℕ) 2 5

Tactic:
decide
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n_1 n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ n < fib n.succ

Tactic:
calc
      n ≤ fib n := IH
      _ < fib (n + 1) := fib_lt_fib_succ (le_trans (by decide) five_le_n)

Premises used: Nat.fib_lt_fib_succ, HAdd.hAdd, Nat.fib, OfNat.ofNat, le_trans
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
five_le_n : 5 ≤ n
refl : LE.le (α := ℕ) 5 5
step : ∀ {n : ℕ} (five_le_n : Nat.le 5 n) (IH : n ≤ fib n), n.succ ≤ fib n.succ
⊢ n ≤ fib n

Tactic:
induction five_le_n with
  | refl => rfl -- 5 ≤ fib 5
  | @step n five_le_n IH => -- n + 1 ≤ fib (n + 1) for 5 ≤ n
    rw [succ_le_iff]
    calc
      n ≤ fib n := IH
      _ < fib (n + 1) := fib_lt_fib_succ (le_trans (by decide) five_le_n)

Premises used: Nat.fib_lt_fib_succ, HAdd.hAdd, Nat.fib, OfNat.ofNat, Nat.succ_le_iff, refl, le_trans
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
⊢ (fib 0).Coprime (fib (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
simp
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
ih : (fib n).Coprime (fib (n + 1))
⊢ (fib (n + 1)).Coprime (fib (n + 1 + 1))

Tactic:
simp only [fib_add_two, coprime_add_self_right, Coprime, ih.symm]

Premises used: Nat.Coprime, Nat.Coprime.symm, Nat.fib_add_two, Nat.coprime_add_self_right
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
zero : (fib 0).Coprime (fib (HAdd.hAdd (α := ℕ) 0 1))
succ : ∀ (n : ℕ) (ih : (fib n).Coprime (fib (n + 1))), (fib (n + 1)).Coprime (fib (n + 1 + 1))
⊢ (fib n).Coprime (fib (n + 1))

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp only [fib_add_two, coprime_add_self_right, Coprime, ih.symm]

Premises used: Nat.Coprime, Nat.fib_add_two, Nat.coprime_add_self_right, Nat.zero, Nat.succ
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m : ℕ
⊢ fib (m + 0 + 1) = fib m * fib 0 + fib (m + 1) * fib (HAdd.hAdd (α := ℕ) 0 1)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
ih : ∀ (m : ℕ), fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
m : ℕ
⊢ fib (m + 1 + n + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)

Tactic:
specialize ih (m + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n m : ℕ
ih : fib (m + 1 + n + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + (n + 1) + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)

Tactic:
rw [add_assoc m 1 n, add_comm 1 n] at ih

Premises used: add_assoc, add_comm, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n m : ℕ
ih : fib (m + (n + 1) + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
succ :
  fib (m + 1) * fib n + (fib m + fib (m + 1)) * fib (n + 1) = fib m * fib (n + 1) + fib (m + 1) * (fib n + fib (n + 1))
⊢ fib (m + (n + 1) + 1) = fib m * fib (n + 1) + fib (m + 1) * fib (n + 1 + 1)

Tactic:
simp only [fib_add_two, ih]

Premises used: Nat.fib_add_two
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n m : ℕ
ih : fib (m + (n + 1) + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + 1) * fib n + (fib m + fib (m + 1)) * fib (n + 1) = fib m * fib (n + 1) + fib (m + 1) * (fib n + fib (n + 1))

Tactic:
ring
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m n : ℕ
zero : ∀ (m : ℕ), fib (m + 0 + 1) = fib m * fib 0 + fib (m + 1) * fib (HAdd.hAdd (α := ℕ) 0 1)
succ :
  ∀ (n : ℕ) (ih : ∀ (m : ℕ), fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)) (m : ℕ),
    fib (m + (n + 1) + 1) = fib m * fib (n + 1) + fib (m + 1) * fib (n + 1 + 1)
⊢ fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)

Tactic:
induction n generalizing m with
  | zero => simp
  | succ n ih =>
    specialize ih (m + 1)
    rw [add_assoc m 1 n, add_comm 1 n] at ih
    simp only [fib_add_two, ih]
    ring

Premises used: add_assoc, Nat.fib_add_two, add_comm, Nat.zero, OfNat.ofNat, Nat.succ
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
zero : fib (HMul.hMul (α := ℕ) 2 0) = fib 0 * (2 * fib (HAdd.hAdd (α := ℕ) 0 1) - fib 0)
succ : ∀ (n : ℕ), fib (2 * (n + 1)) = fib (n + 1) * (2 * fib (n + 1 + 1) - fib (n + 1))
⊢ fib (2 * n) = fib n * (2 * fib (n + 1) - fib n)

Tactic:
cases n
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
⊢ fib (HMul.hMul (α := ℕ) 2 0) = fib 0 * (2 * fib (HAdd.hAdd (α := ℕ) 0 1) - fib 0)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
succ :
  fib (n + 1) * fib n + (fib n + fib (n + 1)) * fib (n + 1) =
    fib (n + 1) * (fib n + fib (n + 1) + (fib n + fib (n + 1)) - fib (n + 1))
⊢ fib (2 * (n + 1)) = fib (n + 1) * (2 * fib (n + 1 + 1) - fib (n + 1))

Tactic:
rw [two_mul, ← add_assoc, fib_add, fib_add_two, two_mul]

Premises used: add_assoc, two_mul, Nat.fib_add_two, Nat.fib_add
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
succ : fib (n + 1) * fib n + (fib n + fib (n + 1)) * fib (n + 1) = fib (n + 1) * (fib n + fib (n + 1) + fib n)
⊢ fib (n + 1) * fib n + (fib n + fib (n + 1)) * fib (n + 1) =
    fib (n + 1) * (fib n + fib (n + 1) + (fib n + fib (n + 1)) - fib (n + 1))

Tactic:
simp only [← add_assoc, add_tsub_cancel_right]

Premises used: add_assoc, add_tsub_cancel_right
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
⊢ fib (n + 1) * fib n + (fib n + fib (n + 1)) * fib (n + 1) = fib (n + 1) * (fib n + fib (n + 1) + fib n)

Tactic:
ring
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
rw : fib n * fib n + fib (n + 1) * fib (n + 1) = HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2
⊢ fib (2 * n + 1) = HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2

Tactic:
rw [two_mul, fib_add]

Premises used: two_mul, Nat.fib_add
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
⊢ fib n * fib n + fib (n + 1) * fib (n + 1) = HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2

Tactic:
ring
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
rw :
  fib n * (2 * fib (n + 1) - fib n) + (HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2) =
    fib (n + 1) * (2 * fib n + fib (n + 1))
⊢ fib (2 * n + 2) = fib (n + 1) * (2 * fib n + fib (n + 1))

Tactic:
rw [fib_add_two, fib_two_mul, fib_two_mul_add_one]

Premises used: Nat.fib_add_two, Nat.fib_two_mul, Nat.fib_two_mul_add_one
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
⊢ fib n ≤ 2 * fib (n + 1)

Tactic:
have : fib n ≤ 2 * fib (n + 1) :=
    le_trans fib_le_fib_succ (mul_comm 2 _ ▸ Nat.le_mul_of_pos_right _ two_pos)
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
this : fib n ≤ 2 * fib (n + 1)
zify :
  (↑(fib n) : ℤ) * (HMul.hMul (α := ℤ) 2 (↑(fib (n + 1)) : ℤ) - (↑(fib n) : ℤ)) +
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(fib (n + 1)) : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑(fib n) : ℤ) 2) =
    (↑(fib (n + 1)) : ℤ) * (HMul.hMul (α := ℤ) 2 (↑(fib n) : ℤ) + (↑(fib (n + 1)) : ℤ))
⊢ fib n * (2 * fib (n + 1) - fib n) + (HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2) =
    fib (n + 1) * (2 * fib n + fib (n + 1))

Tactic:
zify [this]
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
this : fib n ≤ 2 * fib (n + 1)
⊢ (↑(fib n) : ℤ) * (HMul.hMul (α := ℤ) 2 (↑(fib (n + 1)) : ℤ) - (↑(fib n) : ℤ)) +
      (HPow.hPow (α := ℤ) (β := ℕ) (↑(fib (n + 1)) : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑(fib n) : ℤ) 2) =
    (↑(fib (n + 1)) : ℤ) * (HMul.hMul (α := ℤ) 2 (↑(fib n) : ℤ) + (↑(fib (n + 1)) : ℤ))

Tactic:
ring
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
⊢ (if false = true then
        (HPow.hPow (β := ℕ) (fib 0, fib 1).2 2 + HPow.hPow (β := ℕ) (fib 0, fib 1).1 2,
          (fib 0, fib 1).2 * (2 * (fib 0, fib 1).1 + (fib 0, fib 1).2))
      else
        ((fib 0, fib 1).1 * (2 * (fib 0, fib 1).2 - (fib 0, fib 1).1),
          HPow.hPow (β := ℕ) (fib 0, fib 1).2 2 + HPow.hPow (β := ℕ) (fib 0, fib 1).1 2)) =
      (fib 0, fib 1) ∨
    (n = 0 → false = true)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
⊢ (if false = true then
        (HPow.hPow (β := ℕ) (fib 0, fib 1).2 2 + HPow.hPow (β := ℕ) (fib 0, fib 1).1 2,
          (fib 0, fib 1).2 * (2 * (fib 0, fib 1).1 + (fib 0, fib 1).2))
      else
        ((fib 0, fib 1).1 * (2 * (fib 0, fib 1).2 - (fib 0, fib 1).1),
          HPow.hPow (β := ℕ) (fib 0, fib 1).2 2 + HPow.hPow (β := ℕ) (fib 0, fib 1).1 2)) =
      (fib 0, fib 1) ∨
    (n = 0 → true = true)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
⊢ n.fastFibAux = (fib n, fib (n + 1))

Tactic:
Nat.binaryRec ?_ ?_ n

Premises used: Nat.binaryRec
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
refine_1 : fastFibAux 0 = (fib 0, fib (HAdd.hAdd (α := ℕ) 0 1))
refine_2 :
  ∀ (b : Bool) (n : ℕ), n.fastFibAux = (fib n, fib (n + 1)) → (bit b n).fastFibAux = (fib (bit b n), fib (bit b n + 1))
⊢ n.fastFibAux = (fib n, fib (n + 1))

Tactic:
refine Nat.binaryRec ?_ ?_ n
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
⊢ fastFibAux 0 = (fib 0, fib (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
simp [fastFibAux]

Premises used: Nat.fastFibAux
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n n' : ℕ
ih : n'.fastFibAux = (fib n', fib (n' + 1))
refine_2 :
  fib n' * (2 * fib (n' + 1) - fib n') = fib (bit false n') ∧
    HPow.hPow (β := ℕ) (fib (n' + 1)) 2 + HPow.hPow (β := ℕ) (fib n') 2 = fib (bit false n' + 1)
⊢ (bit false n').fastFibAux = (fib (bit false n'), fib (bit false n' + 1))

Tactic:
simp only [fastFibAux_bit_false, fastFibAux_bit_true, congr_arg Prod.fst ih,
        congr_arg Prod.snd ih, Prod.mk_inj]

Premises used: Prod.mk_inj, Prod.fst, congr_arg, Nat.fastFibAux_bit_false, Prod.snd, Nat.fastFibAux_bit_true
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n n' : ℕ
ih : n'.fastFibAux = (fib n', fib (n' + 1))
refine_2 :
  HPow.hPow (β := ℕ) (fib (n' + 1)) 2 + HPow.hPow (β := ℕ) (fib n') 2 = fib (bit true n') ∧
    fib (n' + 1) * (2 * fib n' + fib (n' + 1)) = fib (bit true n' + 1)
⊢ (bit true n').fastFibAux = (fib (bit true n'), fib (bit true n' + 1))

Tactic:
simp only [fastFibAux_bit_false, fastFibAux_bit_true, congr_arg Prod.fst ih,
        congr_arg Prod.snd ih, Prod.mk_inj]

Premises used: Prod.mk_inj, Prod.fst, congr_arg, Nat.fastFibAux_bit_false, Prod.snd, Nat.fastFibAux_bit_true
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n n' : ℕ
ih : n'.fastFibAux = (fib n', fib (n' + 1))
⊢ fib n' * (2 * fib (n' + 1) - fib n') = fib (bit false n') ∧
    HPow.hPow (β := ℕ) (fib (n' + 1)) 2 + HPow.hPow (β := ℕ) (fib n') 2 = fib (bit false n' + 1)

Tactic:
simp [bit, fib_two_mul, fib_two_mul_add_one, fib_two_mul_add_two]

Premises used: Nat.bit, Nat.fib_two_mul, Nat.fib_two_mul_add_one, Nat.fib_two_mul_add_two
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n n' : ℕ
ih : n'.fastFibAux = (fib n', fib (n' + 1))
⊢ HPow.hPow (β := ℕ) (fib (n' + 1)) 2 + HPow.hPow (β := ℕ) (fib n') 2 = fib (bit true n') ∧
    fib (n' + 1) * (2 * fib n' + fib (n' + 1)) = fib (bit true n' + 1)

Tactic:
simp [bit, fib_two_mul, fib_two_mul_add_one, fib_two_mul_add_two]

Premises used: Nat.bit, Nat.fib_two_mul, Nat.fib_two_mul_add_one, Nat.fib_two_mul_add_two
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
rw : n.fastFibAux.1 = fib n
rw₁ rw₂ : (fib n, fib (n + 1)).1 = fib n
⊢ n.fastFib = fib n

Tactic:
rw [fastFib, fastFibAux_eq]

Premises used: Nat.fastFib, Nat.fastFibAux_eq
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
h : ∀ (x : ℕ), fib x = x.fastFib
⊢ fib = fastFib

Tactic:
ext
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
x : ℕ
h h₁ : fib x = fib x
⊢ fib x = x.fastFib

Tactic:
rw [fastFib_eq]

Premises used: Nat.fastFib_eq
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m n : ℕ
inl : (fib m).gcd (fib (0 + m)) = (fib m).gcd (fib 0)
inr : ∀ (h : n > 0), (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)

Tactic:
rcases Nat.eq_zero_or_pos n with rfl | h

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m : ℕ
⊢ (fib m).gcd (fib (0 + m)) = (fib m).gcd (fib 0)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m n : ℕ
h : n > 0
⊢ n.pred.succ = n

Tactic:
replace h := Nat.succ_pred_eq_of_pos h
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m n : ℕ
h : n.pred.succ = n
inr : (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib (n.pred + 1))
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)

Tactic:
rw [← h, succ_eq_add_one]

Premises used: Nat.succ_eq_add_one
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m n : ℕ
h : n.pred.succ = n
rw : (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib (n.pred + m + 1))
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1))

Tactic:
rw [← fib_add n.pred _]

Premises used: Nat.fib_add, Nat.pred
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib (n.pred + m + 1))

Tactic:
ring_nf
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m n : ℕ
h : n.pred.succ = n
rw : (fib m).gcd (fib (n.pred + 1) * fib (m + 1) + fib n.pred * fib m) = (fib m).gcd (fib (n.pred + 1) * fib (m + 1))
rw₁ rw₂ : (fib m).gcd (fib (n.pred + 1) * fib (m + 1)) = (fib m).gcd (fib (n.pred + 1) * fib (m + 1))
⊢ (fib m).gcd (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1)) = (fib m).gcd (fib (n.pred + 1) * fib (m + 1))

Tactic:
rw [add_comm, gcd_add_mul_right_right (fib m) _ (fib n.pred)]

Premises used: Nat.gcd_add_mul_right_right, add_comm, Nat.fib, Nat.pred
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred + 1) * fib (m + 1)) = (fib m).gcd (fib (n.pred + 1))

Tactic:
Coprime.gcd_mul_right_cancel_right (fib (n.pred + 1)) (Coprime.symm (fib_coprime_fib_succ m))

Premises used: Nat.Coprime.symm, Nat.Coprime.gcd_mul_right_cancel_right, Nat.fib_coprime_fib_succ, HAdd.hAdd, Nat.fib, OfNat.ofNat, Nat.pred
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m n : ℕ
h : n.pred.succ = n
gcd : (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1))
gcd₁ : (fib m).gcd (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1)) = (fib m).gcd (fib (n.pred + 1) * fib (m + 1))
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib (n.pred + 1))

Tactic:
calc
    gcd (fib m) (fib (n.pred + 1 + m)) =
        gcd (fib m) (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1)) := by
        rw [← fib_add n.pred _]
        ring_nf
    _ = gcd (fib m) (fib (n.pred + 1) * fib (m + 1)) := by
        rw [add_comm, gcd_add_mul_right_right (fib m) _ (fib n.pred)]
    _ = gcd (fib m) (fib (n.pred + 1)) :=
      Coprime.gcd_mul_right_cancel_right (fib (n.pred + 1)) (Coprime.symm (fib_coprime_fib_succ m))

Premises used: Nat.gcd, Nat.Coprime.symm, HMul.hMul, Nat.Coprime.gcd_mul_right_cancel_right, Nat.fib_coprime_fib_succ, HAdd.hAdd, Nat.fib, OfNat.ofNat, Nat.pred
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m n : ℕ
⊢ (fib m).gcd (fib (n + 0 * m)) = (fib m).gcd (fib n)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m n k : ℕ
rw : (fib m).gcd (fib (n + (k + 1) * m)) = (fib m).gcd (fib (n + k * m))
rw₁ : (fib m).gcd (fib (n + (k * m + 1 * m))) = (fib m).gcd (fib (n + k * m))
rw₂ : (fib m).gcd (fib (n + k * m + 1 * m)) = (fib m).gcd (fib (n + k * m))
rw₃ : (fib m).gcd (fib (n + k * m + m)) = (fib m).gcd (fib (n + k * m))
rw₄ rw₅ : (fib m).gcd (fib (n + k * m)) = (fib m).gcd (fib (n + k * m))
⊢ (fib m).gcd (fib (n + (k + 1) * m)) = (fib m).gcd (fib n)

Tactic:
rw [← gcd_fib_add_mul_self m n k, add_mul, ← add_assoc, one_mul, gcd_fib_add_self _ _]

Premises used: add_mul, add_assoc, Nat.gcd_fib_add_self, one_mul
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
⊢ fib (gcd 0 n) = (fib 0).gcd (fib n)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m n : ℕ
h : 0 < m
h' : fib ((n % m).gcd m) = (fib (n % m)).gcd (fib m)
⊢ fib (m.gcd n) = (fib (n % m)).gcd (fib m)

Tactic:
rw [← gcd_rec m n] at h'

Premises used: Nat.gcd_rec
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m n : ℕ
h : 0 < m
h' : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
rw : (fib m).gcd (fib (n % m + n / m * m))
| (fib m).gcd (fib n)

Tactic:
rw [← mod_add_div' n m]

Premises used: Nat.mod_add_div'
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m n : ℕ
h : 0 < m
h' : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
H1 : fib (m.gcd n) = (fib m).gcd (fib (n % m + n / m * m))
⊢ fib (m.gcd n) = (fib m).gcd (fib n)

Tactic:
conv_rhs => rw [← mod_add_div' n m]

Premises used: Nat.mod_add_div'
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m n : ℕ
h : 0 < m
h' : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
H1 : fib (m.gcd n) = (fib m).gcd (fib (n % m))
H1₁ H1₂ H1₃ H1₄ : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
⊢ fib (m.gcd n) = (fib m).gcd (fib (n % m + n / m * m))

Tactic:
rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]

Premises used: HDiv.hDiv, HMod.hMod, Nat.fib, Nat.gcd_comm, Nat.gcd_fib_add_mul_self
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m n : ℕ
H0 : ∀ (n : ℕ), fib (gcd 0 n) = (fib 0).gcd (fib n)
H1 : ∀ (m n : ℕ), 0 < m → ∀ (h' : fib ((n % m).gcd m) = (fib (n % m)).gcd (fib m)), fib (m.gcd n) = (fib m).gcd (fib n)
⊢ fib (m.gcd n) = (fib m).gcd (fib n)

Tactic:
induction m, n using Nat.gcd.induction with
  | H0 => simp
  | H1 m n _ h' =>
    rw [← gcd_rec m n] at h'
    conv_rhs => rw [← mod_add_div' n m]
    rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]

Premises used: HDiv.hDiv, HMod.hMod, Nat.fib, Nat.gcd_rec, Nat.gcd_comm, Nat.gcd_fib_add_mul_self, Nat.mod_add_div'
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
m n : ℕ
h : m ∣ n
rwa : (fib m).gcd (fib n) = fib m
rwa₁ : fib (m.gcd n) = fib m
rwa₂ : fib m = fib m
rwa₃ : m ∣ n
rwa₄ : fib m = fib m
rwa₅ rwa₆ rwa₇ : m ∣ n
⊢ fib m ∣ fib n

Tactic:
rwa [← gcd_eq_left_iff_dvd, ← fib_gcd, gcd_eq_left_iff_dvd.mpr]

Premises used: Iff.mpr, Nat.fib_gcd, Nat.gcd_eq_left_iff_dvd
-- Module: Mathlib.Data.Nat.Fib.Basic
Goal:
n : ℕ
h1 : fib (n + 1) = ∑ p ∈ @Finset.antidiagonal _ instAddMonoid _ n, p.1.choose p.2
h2 : fib (n + 1 + 1) = ∑ p ∈ @Finset.antidiagonal _ instAddMonoid _ (n + 1), p.1.choose p.2
rw :
  HAdd.hAdd (α := ℕ) (∑ p ∈ @Finset.antidiagonal _ instAddMonoid _ n, p.1.choose p.2)
      (∑
        p ∈
          Finset.cons (n + 1, 0)
            (Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := succ, inj' := succ_injective : ℕ ↪ ℕ })
              (@Finset.antidiagonal _ instAddMonoid _ n))
            ⋯,
        p.1.choose p.2) =
    ∑
      p ∈
        Finset.cons (0, n + 2)
          (Finset.cons (n + 2, 0)
            (Finset.map
              ({ toFun := succ, inj' := succ_injective : ℕ ↪ ℕ }.prodMap
                { toFun := succ, inj' := succ_injective : ℕ ↪ ℕ })
              (@Finset.antidiagonal _ instAddMonoid _ n))
            ⋯)
          ⋯,
      p.1.choose p.2
⊢ fib (n + 2 + 1) = ∑ p ∈ @Finset.antidiagonal _ instAddMonoid _ (n + 2), p.1.choose p.2

Tactic:
rw [fib_add_two, h1, h2, Finset.Nat.antidiagonal_succ_succ', Finset.Nat.antidiagonal_succ']

Premises used: Finset.Nat.antidiagonal_succ_succ', Nat.fib_add_two, Finset.Nat.antidiagonal_succ'