awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
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
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b
have inr₃ : a.factorization ≤ n • b.factorization ↔
  @CeilDiv.ceilDiv _ _ instAddCommMonoid instPartialOrder Finsupp.instAddCommMonoid partialorder smulZeroClass _
      a.factorization n ≤
    b.factorization
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)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.Root (goal)
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
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b
have inr₄ : a.factorization ≤ n • b.factorization ↔ a.factorization ≤ n • b.factorization
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)]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
⊢ fib n ≤ fib (n + 1)
have zero : fib 0 ≤ fib (HAdd.hAdd (α := ℕ) 0 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
zero : fib 0 ≤ fib (HAdd.hAdd (α := ℕ) 0 1)
⊢ fib n ≤ fib (n + 1)
have succ : ∀ (n : ℕ), fib (n + 1) ≤ fib (n + 1 + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
⊢ fib (n + 2) - fib (n + 1) = fib n
have rw : fib n + fib (n + 1) - fib (n + 1) = fib n
Tactic: rw [fib_add_two, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
rw : fib n + fib (n + 1) - fib (n + 1) = fib n
⊢ fib (n + 2) - fib (n + 1) = fib n
have rw₁ : fib n = fib n
Tactic: rw [fib_add_two, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
hn : 2 ≤ n
⊢ fib n < fib (n + 1)
have rcases : ∀ (n : ℕ) (hn : 2 ≤ 2 + n), fib (2 + n) < fib (2 + n + 1)
Tactic: rcases exists_add_of_le hn with ⟨n, rfl⟩
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
hn : 2 ≤ 2 + n
⊢ fib (2 + n) < fib (2 + n + 1)
have rw : 0 < n + 1
Tactic: rw [← tsub_pos_iff_lt, add_comm 2, add_right_comm, fib_add_two, add_tsub_cancel_right, fib_pos]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
⊢ StrictMono (β := ℕ) fun (n : ℕ) ↦ fib (n + 2)
have refine : ∀ (n : ℕ), fib (n + 2) < fib (n + 1 + 2)
Tactic: refine strictMono_nat_of_lt_succ fun n => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
five_le_n : 5 ≤ n
⊢ n ≤ fib n
have refl : LE.le (α := ℕ) 5 5
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)
Cleared hypotheses: five_le_n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
five_le_n : 5 ≤ n
refl : LE.le (α := ℕ) 5 5
⊢ n ≤ fib n
have step : ∀ {n : ℕ} (five_le_n : Nat.le 5 n) (IH : n ≤ fib n), n.succ ≤ fib n.succ
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)
Cleared hypotheses: five_le_n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
⊢ (fib n).Coprime (fib (n + 1))
have zero : (fib 0).Coprime (fib (HAdd.hAdd (α := ℕ) 0 1))
Tactic: induction n with
  | zero => simp
  | succ n ih => simp only [fib_add_two, coprime_add_self_right, Coprime, ih.symm]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
zero : (fib 0).Coprime (fib (HAdd.hAdd (α := ℕ) 0 1))
⊢ (fib n).Coprime (fib (n + 1))
have succ : ∀ (n : ℕ) (ih : (fib n).Coprime (fib (n + 1))), (fib (n + 1)).Coprime (fib (n + 1 + 1))
Tactic: induction n with
  | zero => simp
  | succ n ih => simp only [fib_add_two, coprime_add_self_right, Coprime, ih.symm]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (hypothesis)
Goal:
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)
have ih₁ : fib (m + 1 + n + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
Tactic: specialize ih (m + 1)
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (hypothesis)
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 * fib (n + 1) + fib (m + 1) * fib (n + 1 + 1)
have ih₁ : 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
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n m : ℕ
ih : fib (m + (n + 1) + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + (n + 1) + 1) = fib m * fib (n + 1) + fib (m + 1) * fib (n + 1 + 1)
have 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))
Tactic: simp only [fib_add_two, ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n : ℕ
⊢ fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
have zero : ∀ (m : ℕ), fib (m + 0 + 1) = fib m * fib 0 + fib (m + 1) * fib (HAdd.hAdd (α := ℕ) 0 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
Cleared hypotheses: m, n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n : ℕ
zero : ∀ (m : ℕ), fib (m + 0 + 1) = fib m * fib 0 + fib (m + 1) * fib (HAdd.hAdd (α := ℕ) 0 1)
⊢ fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
have 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)
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
Cleared hypotheses: m, n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
⊢ fib (2 * n) = fib n * (2 * fib (n + 1) - fib n)
have zero : fib (HMul.hMul (α := ℕ) 2 0) = fib 0 * (2 * fib (HAdd.hAdd (α := ℕ) 0 1) - fib 0)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
zero : fib (HMul.hMul (α := ℕ) 2 0) = fib 0 * (2 * fib (HAdd.hAdd (α := ℕ) 0 1) - fib 0)
⊢ fib (2 * n) = fib n * (2 * fib (n + 1) - fib n)
have succ : ∀ (n : ℕ), fib (2 * (n + 1)) = fib (n + 1) * (2 * fib (n + 1 + 1) - fib (n + 1))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
⊢ fib (2 * (n + 1)) = fib (n + 1) * (2 * fib (n + 1 + 1) - fib (n + 1))
have 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))
Tactic: rw [two_mul, ← add_assoc, fib_add, fib_add_two, two_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
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 + fib (n + 1)) - fib (n + 1))
have succ : fib (n + 1) * fib n + (fib n + fib (n + 1)) * fib (n + 1) = fib (n + 1) * (fib n + fib (n + 1) + fib n)
Tactic: simp only [← add_assoc, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
⊢ fib (2 * n + 1) = HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2
have rw : fib n * fib n + fib (n + 1) * fib (n + 1) = HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2
Tactic: rw [two_mul, fib_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
⊢ fib (2 * n + 2) = fib (n + 1) * (2 * fib n + fib (n + 1))
have 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))
Tactic: rw [fib_add_two, fib_two_mul, fib_two_mul_add_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (hypothesis)
Goal:
n : ℕ
⊢ 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))
have this : 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)
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
this : fib n ≤ 2 * 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))
have 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)) : ℤ))
Tactic: zify [this]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
⊢ n.fastFibAux = (fib n, fib (n + 1))
have refine_1 : fastFibAux 0 = (fib 0, fib (HAdd.hAdd (α := ℕ) 0 1))
Tactic: refine Nat.binaryRec ?_ ?_ n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
refine_1 : fastFibAux 0 = (fib 0, fib (HAdd.hAdd (α := ℕ) 0 1))
⊢ n.fastFibAux = (fib n, fib (n + 1))
have 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))
Tactic: refine Nat.binaryRec ?_ ?_ n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n n' : ℕ
ih : n'.fastFibAux = (fib n', fib (n' + 1))
⊢ (bit false n').fastFibAux = (fib (bit false n'), fib (bit false n' + 1))
have 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)
Tactic: simp only [fastFibAux_bit_false, fastFibAux_bit_true, congr_arg Prod.fst ih,
        congr_arg Prod.snd ih, Prod.mk_inj]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n n' : ℕ
ih : n'.fastFibAux = (fib n', fib (n' + 1))
⊢ (bit true n').fastFibAux = (fib (bit true n'), fib (bit true n' + 1))
have 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)
Tactic: simp only [fastFibAux_bit_false, fastFibAux_bit_true, congr_arg Prod.fst ih,
        congr_arg Prod.snd ih, Prod.mk_inj]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
⊢ n.fastFib = fib n
have rw : n.fastFibAux.1 = fib n
Tactic: rw [fastFib, fastFibAux_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
rw : n.fastFibAux.1 = fib n
⊢ n.fastFib = fib n
have rw₁ : (fib n, fib (n + 1)).1 = fib n
Tactic: rw [fastFib, fastFibAux_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
⊢ fib = fastFib
have h : ∀ (x : ℕ), fib x = x.fastFib
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
x : ℕ
⊢ fib x = x.fastFib
have h : fib x = fib x
Tactic: rw [fastFib_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n : ℕ
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)
have inl : (fib m).gcd (fib (0 + m)) = (fib m).gcd (fib 0)
Tactic: rcases Nat.eq_zero_or_pos n with rfl | h
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n : ℕ
inl : (fib m).gcd (fib (0 + m)) = (fib m).gcd (fib 0)
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)
have inr : ∀ (h : n > 0), (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)
Tactic: rcases Nat.eq_zero_or_pos n with rfl | h
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (hypothesis)
Goal:
m n : ℕ
h : n > 0
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)
have h₁ : n.pred.succ = n
Tactic: replace h := Nat.succ_pred_eq_of_pos h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)
have inr : (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib (n.pred + 1))
Tactic: rw [← h, succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1))
have rw : (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib (n.pred + m + 1))
Tactic: rw [← fib_add n.pred _]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n : ℕ
h : n.pred.succ = n
⊢ (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))
have 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))
Tactic: rw [add_comm, gcd_add_mul_right_right (fib m) _ (fib n.pred)]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
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))
⊢ (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))
have rw₁ : (fib m).gcd (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)]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib (n.pred + 1))
have gcd : (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 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))
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
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))
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib (n.pred + 1))
have 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))
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))
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n k : ℕ
⊢ (fib m).gcd (fib (n + (k + 1) * m)) = (fib m).gcd (fib n)
have rw : (fib m).gcd (fib (n + (k + 1) * m)) = (fib m).gcd (fib (n + k * m))
Tactic: rw [← gcd_fib_add_mul_self m n k, add_mul, ← add_assoc, one_mul, gcd_fib_add_self _ _]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n k : ℕ
rw : (fib m).gcd (fib (n + (k + 1) * m)) = (fib m).gcd (fib (n + k * m))
⊢ (fib m).gcd (fib (n + (k + 1) * m)) = (fib m).gcd (fib n)
have rw₁ : (fib m).gcd (fib (n + (k * m + 1 * m))) = (fib m).gcd (fib (n + k * m))
Tactic: rw [← gcd_fib_add_mul_self m n k, add_mul, ← add_assoc, one_mul, gcd_fib_add_self _ _]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
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))
⊢ (fib m).gcd (fib (n + (k + 1) * m)) = (fib m).gcd (fib n)
have rw₂ : (fib m).gcd (fib (n + k * m + 1 * m)) = (fib m).gcd (fib (n + k * m))
Tactic: rw [← gcd_fib_add_mul_self m n k, add_mul, ← add_assoc, one_mul, gcd_fib_add_self _ _]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
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))
⊢ (fib m).gcd (fib (n + (k + 1) * m)) = (fib m).gcd (fib n)
have rw₃ : (fib m).gcd (fib (n + k * m + m)) = (fib m).gcd (fib (n + k * m))
Tactic: rw [← gcd_fib_add_mul_self m n k, add_mul, ← add_assoc, one_mul, gcd_fib_add_self _ _]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
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))
⊢ (fib m).gcd (fib (n + (k + 1) * m)) = (fib m).gcd (fib n)
have rw₄ : (fib m).gcd (fib (n + k * m)) = (fib m).gcd (fib (n + k * m))
Tactic: rw [← gcd_fib_add_mul_self m n k, add_mul, ← add_assoc, one_mul, gcd_fib_add_self _ _]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (hypothesis)
Goal:
m n : ℕ
h : 0 < m
h' : fib ((n % m).gcd m) = (fib (n % m)).gcd (fib m)
⊢ fib (m.gcd n) = (fib m).gcd (fib n)
have h'₁ : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
Tactic: rw [← gcd_rec m n] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n : ℕ
h : 0 < m
h' : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
| (fib m).gcd (fib n)
have rw : (fib m).gcd (fib (n % m + n / m * m))
Tactic: rw [← mod_add_div' n m]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n : ℕ
h : 0 < m
h' : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
⊢ fib (m.gcd n) = (fib m).gcd (fib n)
have H1 : fib (m.gcd n) = (fib m).gcd (fib (n % m + n / m * m))
Tactic: conv_rhs => rw [← mod_add_div' n m]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n : ℕ
h : 0 < m
h' : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
⊢ fib (m.gcd n) = (fib m).gcd (fib (n % m + n / m * m))
have H1 : fib (m.gcd n) = (fib m).gcd (fib (n % m))
Tactic: rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n : ℕ
⊢ fib (m.gcd n) = (fib m).gcd (fib n)
have H0 : ∀ (n : ℕ), fib (gcd 0 n) = (fib 0).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) _]
Cleared hypotheses: m, n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n : ℕ
H0 : ∀ (n : ℕ), fib (gcd 0 n) = (fib 0).gcd (fib n)
⊢ fib (m.gcd n) = (fib m).gcd (fib n)
have 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)
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) _]
Cleared hypotheses: m, n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n : ℕ
h : m ∣ n
⊢ fib m ∣ fib n
have rwa : (fib m).gcd (fib n) = fib m
Tactic: rwa [← gcd_eq_left_iff_dvd, ← fib_gcd, gcd_eq_left_iff_dvd.mpr]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n : ℕ
h : m ∣ n
rwa : (fib m).gcd (fib n) = fib m
⊢ fib m ∣ fib n
have rwa₁ : fib (m.gcd n) = fib m
Tactic: rwa [← gcd_eq_left_iff_dvd, ← fib_gcd, gcd_eq_left_iff_dvd.mpr]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
m n : ℕ
h : m ∣ n
rwa : (fib m).gcd (fib n) = fib m
rwa₁ : fib (m.gcd n) = fib m
⊢ fib m ∣ fib n
have rwa₂ : fib m = fib m
Tactic: rwa [← gcd_eq_left_iff_dvd, ← fib_gcd, gcd_eq_left_iff_dvd.mpr]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
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
⊢ fib (n + 2 + 1) = ∑ p ∈ @Finset.antidiagonal _ instAddMonoid _ (n + 2), p.1.choose p.2
have 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))
          sorry,
      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))
          sorry)
        sorry,
    p.1.choose p.2
Tactic: rw [fib_add_two, h1, h2, Finset.Nat.antidiagonal_succ_succ', Finset.Nat.antidiagonal_succ']
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
ih : fib (n + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1
⊢ fib n + fib (n + 1) = fib n + ∑ k ∈ Finset.range n, fib k + 1
have rw : fib n + HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1 = fib n + ∑ k ∈ Finset.range n, fib k + 1
Tactic: rw [ih, add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
ih : fib (n + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1
rw : fib n + HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1 = fib n + ∑ k ∈ Finset.range n, fib k + 1
⊢ fib n + fib (n + 1) = fib n + ∑ k ∈ Finset.range n, fib k + 1
have rw₁ : fib n + HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1 = fib n + HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1
Tactic: rw [ih, add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
ih : fib (n + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1
⊢ fib (n + 1 + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range (n + 1), fib k) 1
have fib : fib n + fib (n + 1) = fib n + ∑ k ∈ Finset.range n, fib k + 1
Tactic: calc
      fib (n + 2) = fib n + fib (n + 1) := fib_add_two
      _ = (fib n + ∑ k ∈ Finset.range n, fib k) + 1 := by rw [ih, add_assoc]
      _ = (∑ k ∈ Finset.range (n + 1), fib k) + 1 := by simp [Finset.range_add_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
ih : Nat.fib (n + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, Nat.fib k) 1
fib : Nat.fib n + Nat.fib (n + 1) = Nat.fib n + ∑ k ∈ Finset.range n, Nat.fib k + 1
⊢ Nat.fib (n + 1 + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range (n + 1), Nat.fib k) 1
have fib₁ : Nat.fib n + ∑ k ∈ Finset.range n, Nat.fib k + 1 = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range (n + 1), Nat.fib k) 1
Tactic: calc
      fib (n + 2) = fib n + fib (n + 1) := fib_add_two
      _ = (fib n + ∑ k ∈ Finset.range n, fib k) + 1 := by rw [ih, add_assoc]
      _ = (∑ k ∈ Finset.range (n + 1), fib k) + 1 := by simp [Finset.range_add_one]