awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
this : HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 = -(↑(n - 1) : ℤ)
⊢ HPow.hPow (α := ℤ) (-1) (n + 1) * HSub.hSub (α := ℤ) (↑(Nat.fib n) : ℤ) (↑(Nat.fib (n + 1)) : ℤ) =
    fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
have inl : ∀ (n : ℕ) (hn0 : ¬n + n = 0) (this : HAdd.hAdd (α := ℤ) (-(↑(n + n) : ℤ)) 1 = -(↑(n + n - 1) : ℤ)),
  HPow.hPow (α := ℤ) (-1) (n + n + 1) * HSub.hSub (α := ℤ) (↑(Nat.fib (n + n)) : ℤ) (↑(Nat.fib (n + n + 1)) : ℤ) =
    fib (HAdd.hAdd (α := ℤ) (-(↑(n + n) : ℤ)) 1)
Tactic: obtain (⟨n, rfl⟩ | ⟨n, rfl⟩) := n.even_or_odd
Cleared hypotheses: n, hn0, this
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
this : HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 = -(↑(n - 1) : ℤ)
inl :
  ∀ (n : ℕ) (hn0 : ¬n + n = 0) (this : HAdd.hAdd (α := ℤ) (-(↑(n + n) : ℤ)) 1 = -(↑(n + n - 1) : ℤ)),
    HPow.hPow (α := ℤ) (-1) (n + n + 1) * HSub.hSub (α := ℤ) (↑(Nat.fib (n + n)) : ℤ) (↑(Nat.fib (n + n + 1)) : ℤ) =
      fib (HAdd.hAdd (α := ℤ) (-(↑(n + n) : ℤ)) 1)
⊢ HPow.hPow (α := ℤ) (-1) (n + 1) * HSub.hSub (α := ℤ) (↑(Nat.fib n) : ℤ) (↑(Nat.fib (n + 1)) : ℤ) =
    fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
have inr : ∀ (n : ℕ) (hn0 : ¬2 * n + 1 = 0) (this : HAdd.hAdd (α := ℤ) (-(↑(2 * n + 1) : ℤ)) 1 = -(↑(2 * n + 1 - 1) : ℤ)),
  HPow.hPow (α := ℤ) (-1) (2 * n + 1 + 1) *
      HSub.hSub (α := ℤ) (↑(Nat.fib (2 * n + 1)) : ℤ) (↑(Nat.fib (2 * n + 1 + 1)) : ℤ) =
    fib (HAdd.hAdd (α := ℤ) (-(↑(2 * n + 1) : ℤ)) 1)
Tactic: obtain (⟨n, rfl⟩ | ⟨n, rfl⟩) := n.even_or_odd
Cleared hypotheses: n, hn0, this
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℕ
hn0 : ¬n + n = 0
this : HAdd.hAdd (α := ℤ) (-(↑(n + n) : ℤ)) 1 = -(↑(n + n - 1) : ℤ)
⊢ HPow.hPow (α := ℤ) (-1) (n + n + 1) * HSub.hSub (α := ℤ) (↑(Nat.fib (n + n)) : ℤ) (↑(Nat.fib (n + n + 1)) : ℤ) =
    fib (HAdd.hAdd (α := ℤ) (-(↑(n + n) : ℤ)) 1)
have inl : HPow.hPow (α := ℤ) (-1) (2 * n) * HPow.hPow (α := ℤ) (β := ℕ) (-1) 1 *
    HSub.hSub (α := ℤ) (↑(Nat.fib (2 * n)) : ℤ) (↑(Nat.fib (2 * n - 1) + Nat.fib (2 * n)) : ℤ) =
  HPow.hPow (α := ℤ) (-1) (2 * n) * (↑(Nat.fib (2 * n - 1)) : ℤ)
Tactic: rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add, ← two_mul,
            Nat.sub_add_cancel (by grind)]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℕ
hn0 : ¬2 * n + 1 = 0
this : HAdd.hAdd (α := ℤ) (-(↑(2 * n + 1) : ℤ)) 1 = -(↑(2 * n + 1 - 1) : ℤ)
⊢ HPow.hPow (α := ℤ) (-1) (2 * n + 1 + 1) *
      HSub.hSub (α := ℤ) (↑(Nat.fib (2 * n + 1)) : ℤ) (↑(Nat.fib (2 * n + 1 + 1)) : ℤ) =
    fib (HAdd.hAdd (α := ℤ) (-(↑(2 * n + 1) : ℤ)) 1)
have inr : HPow.hPow (α := ℤ) (-1) (2 * n + 1) * HPow.hPow (α := ℤ) (β := ℕ) (-1) 1 *
    HSub.hSub (α := ℤ) (↑(Nat.fib (2 * n + 1)) : ℤ) (↑(Nat.fib (2 * n + 1 - 1) + Nat.fib (2 * n + 1)) : ℤ) =
  HPow.hPow (α := ℤ) (-1) (2 * n + 1 - 1 + 1) * (↑(Nat.fib (2 * n + 1 - 1)) : ℤ)
Tactic: rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
⊢ HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ) +
      HPow.hPow (α := ℤ) (-1) (1 + (n + 1)) * (↑(Nat.fib (n + 1)) : ℤ) =
    fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
have calc : HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ) +
    HPow.hPow (α := ℤ) (-1) (1 + (n + 1)) * (↑(Nat.fib (n + 1)) : ℤ) =
  HPow.hPow (α := ℤ) (-1) (n + 1) * HSub.hSub (α := ℤ) (↑(Nat.fib n) : ℤ) (↑(Nat.fib (n + 1)) : ℤ)
Tactic: calc _ = (-1) ^ (n + 1) * ((n.fib - (n + 1).fib : ℤ)) := by grind
      _ = _ := by
        have : -(n : ℤ) + 1 = -((n - 1 : ℕ) : ℤ) := by grind
        obtain (⟨n, rfl⟩ | ⟨n, rfl⟩) := n.even_or_odd
        · rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add, ← two_mul,
            Nat.sub_add_cancel (by grind)]
          simp
        · rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add]
          simp
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℕ
hn0 : ¬n = 0
calc :
  HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ) +
      HPow.hPow (α := ℤ) (-1) (1 + (n + 1)) * (↑(Nat.fib (n + 1)) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * HSub.hSub (α := ℤ) (↑(Nat.fib n) : ℤ) (↑(Nat.fib (n + 1)) : ℤ)
⊢ HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ) +
      HPow.hPow (α := ℤ) (-1) (1 + (n + 1)) * (↑(Nat.fib (n + 1)) : ℤ) =
    fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
have calc₁ : HPow.hPow (α := ℤ) (-1) (n + 1) * HSub.hSub (α := ℤ) (↑(Nat.fib n) : ℤ) (↑(Nat.fib (n + 1)) : ℤ) =
  fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: calc _ = (-1) ^ (n + 1) * ((n.fib - (n + 1).fib : ℤ)) := by grind
      _ = _ := by
        have : -(n : ℤ) + 1 = -((n - 1 : ℕ) : ℤ) := by grind
        obtain (⟨n, rfl⟩ | ⟨n, rfl⟩) := n.even_or_odd
        · rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add, ← two_mul,
            Nat.sub_add_cancel (by grind)]
          simp
        · rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add]
          simp
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℕ
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ) +
      HPow.hPow (α := ℤ) (-1) (1 + (n + 1)) * (↑(Nat.fib (n + 1)) : ℤ)
have if : ∀ (hn0 : n = 0),
  fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ) +
      HPow.hPow (α := ℤ) (-1) (1 + (n + 1)) * (↑(Nat.fib (n + 1)) : ℤ)
Tactic: if hn0 : n = 0 then simp [hn0] else
    symm
    calc _ = (-1) ^ (n + 1) * ((n.fib - (n + 1).fib : ℤ)) := by grind
      _ = _ := by
        have : -(n : ℤ) + 1 = -((n - 1 : ℕ) : ℤ) := by grind
        obtain (⟨n, rfl⟩ | ⟨n, rfl⟩) := n.even_or_odd
        · rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add, ← two_mul,
            Nat.sub_add_cancel (by grind)]
          simp
        · rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add]
          simp
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℕ
if :
  ∀ (hn0 : n = 0),
    fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
      HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ) +
        HPow.hPow (α := ℤ) (-1) (1 + (n + 1)) * (↑(Nat.fib (n + 1)) : ℤ)
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ) +
      HPow.hPow (α := ℤ) (-1) (1 + (n + 1)) * (↑(Nat.fib (n + 1)) : ℤ)
have if₁ : ∀ (hn0 : ¬n = 0),
  fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ) +
      HPow.hPow (α := ℤ) (-1) (1 + (n + 1)) * (↑(Nat.fib (n + 1)) : ℤ)
Tactic: if hn0 : n = 0 then simp [hn0] else
    symm
    calc _ = (-1) ^ (n + 1) * ((n.fib - (n + 1).fib : ℤ)) := by grind
      _ = _ := by
        have : -(n : ℤ) + 1 = -((n - 1 : ℕ) : ℤ) := by grind
        obtain (⟨n, rfl⟩ | ⟨n, rfl⟩) := n.even_or_odd
        · rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add, ← two_mul,
            Nat.sub_add_cancel (by grind)]
          simp
        · rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add]
          simp
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℤ
⊢ fib n = 0 ↔ n = 0
have inl : ∀ (n : ℕ), fib (↑n : ℤ) = 0 ↔ Eq (α := ℤ) (↑n : ℤ) 0
Tactic: obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℤ
inl : ∀ (n : ℕ), fib (↑n : ℤ) = 0 ↔ Eq (α := ℤ) (↑n : ℤ) 0
⊢ fib n = 0 ↔ n = 0
have inr : ∀ (n : ℕ), fib (-(↑n : ℤ)) = 0 ↔ Eq (α := ℤ) (-(↑n : ℤ)) 0
Tactic: obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
m : ℕ
n : ℤ
⊢ fib ((↑m : ℤ) + n) + fib ((↑m : ℤ) + n + 1) =
    fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib ((↑(m + 1) : ℤ) + n)
have rw : fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib ((↑m : ℤ) + n + 1) =
  fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib ((↑(m + 1) : ℤ) + n)
Tactic: rw [fib_natCast_add]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
m : ℕ
n : ℤ
⊢ fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib ((↑(m + 1) : ℤ) + n) =
    fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib (↑m : ℤ) * fib n +
      fib (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) * fib (n + 1)
have rw : fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) +
    (fib (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 1) * fib n + fib (↑(m + 1) : ℤ) * fib (n + 1)) =
  fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib (↑m : ℤ) * fib n +
    fib (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) * fib (n + 1)
Tactic: rw [fib_natCast_add]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
m : ℕ
n : ℤ
⊢ fib ((↑(m + 2) : ℤ) + n) = fib (HSub.hSub (α := ℤ) (↑(m + 2) : ℤ) 1) * fib n + fib (↑(m + 2) : ℤ) * fib (n + 1)
have calc : fib ((↑(m + 2) : ℤ) + n) = fib ((↑m : ℤ) + n) + fib ((↑m : ℤ) + n + 1)
Tactic: calc _ = fib (m + n) + fib (m + n + 1) := by grind [fib_add_two]
      _ = fib (m - 1) * fib n + fib m * fib (n + 1) + fib ((m + 1 : ℕ) + n) := by
        rw [fib_natCast_add]; grind
      _ = fib (m - 1) * fib n + fib m * fib (n + 1) + fib m * fib n +
          fib (m + 1) * fib (n + 1) := by rw [fib_natCast_add]; grind
      _ = _ := by grind [fib_add_two]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
m : ℕ
n : ℤ
calc : fib ((↑(m + 2) : ℤ) + n) = fib ((↑m : ℤ) + n) + fib ((↑m : ℤ) + n + 1)
⊢ fib ((↑(m + 2) : ℤ) + n) = fib (HSub.hSub (α := ℤ) (↑(m + 2) : ℤ) 1) * fib n + fib (↑(m + 2) : ℤ) * fib (n + 1)
have calc₁ : fib ((↑m : ℤ) + n) + fib ((↑m : ℤ) + n + 1) =
  fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib ((↑(m + 1) : ℤ) + n)
Tactic: calc _ = fib (m + n) + fib (m + n + 1) := by grind [fib_add_two]
      _ = fib (m - 1) * fib n + fib m * fib (n + 1) + fib ((m + 1 : ℕ) + n) := by
        rw [fib_natCast_add]; grind
      _ = fib (m - 1) * fib n + fib m * fib (n + 1) + fib m * fib n +
          fib (m + 1) * fib (n + 1) := by rw [fib_natCast_add]; grind
      _ = _ := by grind [fib_add_two]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
m : ℕ
n : ℤ
calc : fib ((↑(m + 2) : ℤ) + n) = fib ((↑m : ℤ) + n) + fib ((↑m : ℤ) + n + 1)
calc₁ :
  fib ((↑m : ℤ) + n) + fib ((↑m : ℤ) + n + 1) =
    fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib ((↑(m + 1) : ℤ) + n)
⊢ fib ((↑(m + 2) : ℤ) + n) = fib (HSub.hSub (α := ℤ) (↑(m + 2) : ℤ) 1) * fib n + fib (↑(m + 2) : ℤ) * fib (n + 1)
have calc₂ : fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib ((↑(m + 1) : ℤ) + n) =
  fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib (↑m : ℤ) * fib n +
    fib (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) * fib (n + 1)
Tactic: calc _ = fib (m + n) + fib (m + n + 1) := by grind [fib_add_two]
      _ = fib (m - 1) * fib n + fib m * fib (n + 1) + fib ((m + 1 : ℕ) + n) := by
        rw [fib_natCast_add]; grind
      _ = fib (m - 1) * fib n + fib m * fib (n + 1) + fib m * fib n +
          fib (m + 1) * fib (n + 1) := by rw [fib_natCast_add]; grind
      _ = _ := by grind [fib_add_two]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
m : ℕ
n : ℤ
calc : fib ((↑(m + 2) : ℤ) + n) = fib ((↑m : ℤ) + n) + fib ((↑m : ℤ) + n + 1)
calc₁ :
  fib ((↑m : ℤ) + n) + fib ((↑m : ℤ) + n + 1) =
    fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib ((↑(m + 1) : ℤ) + n)
calc₂ :
  fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib ((↑(m + 1) : ℤ) + n) =
    fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib (↑m : ℤ) * fib n +
      fib (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) * fib (n + 1)
⊢ fib ((↑(m + 2) : ℤ) + n) = fib (HSub.hSub (α := ℤ) (↑(m + 2) : ℤ) 1) * fib n + fib (↑(m + 2) : ℤ) * fib (n + 1)
have calc₃ : fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib (↑m : ℤ) * fib n +
    fib (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) * fib (n + 1) =
  fib (HSub.hSub (α := ℤ) (↑(m + 2) : ℤ) 1) * fib n + fib (↑(m + 2) : ℤ) * fib (n + 1)
Tactic: calc _ = fib (m + n) + fib (m + n + 1) := by grind [fib_add_two]
      _ = fib (m - 1) * fib n + fib m * fib (n + 1) + fib ((m + 1 : ℕ) + n) := by
        rw [fib_natCast_add]; grind
      _ = fib (m - 1) * fib n + fib m * fib (n + 1) + fib m * fib n +
          fib (m + 1) * fib (n + 1) := by rw [fib_natCast_add]; grind
      _ = _ := by grind [fib_add_two]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℤ
m : ℕ
⊢ fib ((↑m : ℤ) + n) + fib ((↑m : ℤ) + n + 1) =
    fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib ((↑(m + 1) : ℤ) + n)
have rw : fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib ((↑m : ℤ) + n + 1) =
  fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib ((↑(m + 1) : ℤ) + n)
Tactic: rw [fib_natCast_add]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℤ
m : ℕ
⊢ fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib ((↑(m + 1) : ℤ) + n) =
    fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib (↑m : ℤ) * fib n +
      fib (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) * fib (n + 1)
have rw : fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) +
    (fib (HSub.hSub (α := ℤ) (↑(m + 1) : ℤ) 1) * fib n + fib (↑(m + 1) : ℤ) * fib (n + 1)) =
  fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1) + fib (↑m : ℤ) * fib n +
    fib (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) * fib (n + 1)
Tactic: rw [fib_natCast_add]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
m n : ℕ
| fib (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) (-(↑n : ℤ))) - fib (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) (-(↑(n + 1) : ℤ)))
have rw : fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib (-(↑n : ℤ)) + fib (-(↑m : ℤ)) * fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) -
  (fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib (-(↑(n + 1) : ℤ)) +
    fib (-(↑m : ℤ)) * fib (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 1))
Tactic: rw [fib_neg_natCast_add_neg_natCast, fib_neg_natCast_add_neg_natCast]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
m n : ℕ
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) (-(↑n : ℤ))) - fib (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) (-(↑(n + 1) : ℤ))) =
    fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib (-(↑n : ℤ)) +
          fib (-(↑m : ℤ)) * fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) -
        fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) -
      fib (-(↑m : ℤ)) * fib (-(↑n : ℤ))
have conv_lhs : fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib (-(↑n : ℤ)) + fib (-(↑m : ℤ)) * fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) -
    (fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib (-(↑(n + 1) : ℤ)) +
      fib (-(↑m : ℤ)) * fib (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 1)) =
  fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib (-(↑n : ℤ)) + fib (-(↑m : ℤ)) * fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) -
      fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) -
    fib (-(↑m : ℤ)) * fib (-(↑n : ℤ))
Tactic: conv_lhs => rw [fib_neg_natCast_add_neg_natCast, fib_neg_natCast_add_neg_natCast]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
m n : ℤ
⊢ fib (m + n) = fib (m - 1) * fib n + fib m * fib (n + 1)
have inl : ∀ (m : ℕ), fib ((↑m : ℤ) + n) = fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1)
Tactic: obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
m n : ℤ
inl : ∀ (m : ℕ), fib ((↑m : ℤ) + n) = fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1)
⊢ fib (m + n) = fib (m - 1) * fib n + fib m * fib (n + 1)
have inr : ∀ (m : ℕ), fib (-(↑m : ℤ) + n) = fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib n + fib (-(↑m : ℤ)) * fib (n + 1)
Tactic: obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℤ
m : ℕ
⊢ fib (-(↑m : ℤ) + n) = fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib n + fib (-(↑m : ℤ)) * fib (n + 1)
have inr : ∀ (n : ℕ),
  fib (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) (↑n : ℤ)) =
    fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib (↑n : ℤ) + fib (-(↑m : ℤ)) * fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
Tactic: obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℤ
m : ℕ
inr :
  ∀ (n : ℕ),
    fib (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) (↑n : ℤ)) =
      fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib (↑n : ℤ) + fib (-(↑m : ℤ)) * fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ fib (-(↑m : ℤ) + n) = fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib n + fib (-(↑m : ℤ)) * fib (n + 1)
have inr₁ : ∀ (n : ℕ),
  fib (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) (-(↑n : ℤ))) =
    fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib (-(↑n : ℤ)) + fib (-(↑m : ℤ)) * fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℤ
⊢ fib (2 * n) = fib n * (2 * fib (n + 1) - fib n)
have rw : fib (n - 1) * fib n + fib n * fib (n + 1) = fib n * (2 * fib (n + 1) - fib n)
Tactic: rw [two_mul, fib_add]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (hypothesis)
Goal:
n : ℤ
⊢ fib (2 * n + 1) = HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2
have this : fib (n + 1 + n) = fib (n + 1 - 1) * fib n + fib (n + 1) * fib (n + 1)
Tactic: have := fib_add (n + 1) n
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℤ
⊢ fib (2 * n + 2) = fib (n + 1) * (2 * fib n + fib (n + 1))
have rw : fib (n + 1) * (2 * fib (n + 1 + 1) - fib (n + 1)) = fib (n + 1) * (2 * fib n + fib (n + 1))
Tactic: rw [← mul_add_one, fib_two_mul]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
m n : ℤ
⊢ (fib m).gcd (fib n) = Nat.fib (m.gcd n)
have inl : ∀ (m : ℕ), (fib (↑m : ℤ)).gcd (fib n) = Nat.fib (gcd (↑m : ℤ) n)
Tactic: obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
m n : ℤ
inl : ∀ (m : ℕ), (fib (↑m : ℤ)).gcd (fib n) = Nat.fib (gcd (↑m : ℤ) n)
⊢ (fib m).gcd (fib n) = Nat.fib (m.gcd n)
have inr : ∀ (m : ℕ), (fib (-(↑m : ℤ))).gcd (fib n) = Nat.fib (gcd (-(↑m : ℤ)) n)
Tactic: obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℤ
m : ℕ
⊢ (fib (↑m : ℤ)).gcd (fib n) = Nat.fib (gcd (↑m : ℤ) n)
have inl : ∀ (n : ℕ), (fib (↑m : ℤ)).gcd (fib (↑n : ℤ)) = Nat.fib (gcd (↑m : ℤ) (↑n : ℤ))
Tactic: obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℤ
m : ℕ
inl : ∀ (n : ℕ), (fib (↑m : ℤ)).gcd (fib (↑n : ℤ)) = Nat.fib (gcd (↑m : ℤ) (↑n : ℤ))
⊢ (fib (↑m : ℤ)).gcd (fib n) = Nat.fib (gcd (↑m : ℤ) n)
have inl₁ : ∀ (n : ℕ), (fib (↑m : ℤ)).gcd (fib (-(↑n : ℤ))) = Nat.fib (gcd (↑m : ℤ) (-(↑n : ℤ)))
Tactic: obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℤ
m : ℕ
⊢ (fib (-(↑m : ℤ))).gcd (fib n) = Nat.fib (gcd (-(↑m : ℤ)) n)
have inr : ∀ (n : ℕ), (fib (-(↑m : ℤ))).gcd (fib (↑n : ℤ)) = Nat.fib (gcd (-(↑m : ℤ)) (↑n : ℤ))
Tactic: obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℤ
m : ℕ
inr : ∀ (n : ℕ), (fib (-(↑m : ℤ))).gcd (fib (↑n : ℤ)) = Nat.fib (gcd (-(↑m : ℤ)) (↑n : ℤ))
⊢ (fib (-(↑m : ℤ))).gcd (fib n) = Nat.fib (gcd (-(↑m : ℤ)) n)
have inr₁ : ∀ (n : ℕ), (fib (-(↑m : ℤ))).gcd (fib (-(↑n : ℤ))) = Nat.fib (gcd (-(↑m : ℤ)) (-(↑n : ℤ)))
Tactic: obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.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 (by simp), gcd_fib, ← fib_natCast, (gcd_eq_left_iff_dvd (by simp)).mpr]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
m : ℕ
n : ℤ
h : (↑m : ℤ) ∣ n
rwa : (↑((fib (↑m : ℤ)).gcd (fib n)) : ℤ) = fib (↑m : ℤ)
⊢ fib (↑m : ℤ) ∣ fib n
have rwa₁ : (↑(Nat.fib (gcd (↑m : ℤ) n)) : ℤ) = fib (↑m : ℤ)
Tactic: rwa [← gcd_eq_left_iff_dvd (by simp), gcd_fib, ← fib_natCast, (gcd_eq_left_iff_dvd (by simp)).mpr]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
m : ℕ
n : ℤ
h : (↑m : ℤ) ∣ n
rwa : (↑((fib (↑m : ℤ)).gcd (fib n)) : ℤ) = fib (↑m : ℤ)
rwa₁ : (↑(Nat.fib (gcd (↑m : ℤ) n)) : ℤ) = fib (↑m : ℤ)
⊢ fib (↑m : ℤ) ∣ fib n
have rwa₂ : fib (↑(gcd (↑m : ℤ) n) : ℤ) = fib (↑m : ℤ)
Tactic: rwa [← gcd_eq_left_iff_dvd (by simp), gcd_fib, ← fib_natCast, (gcd_eq_left_iff_dvd (by simp)).mpr]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
m : ℕ
n : ℤ
h : (↑m : ℤ) ∣ n
rwa : (↑((fib (↑m : ℤ)).gcd (fib n)) : ℤ) = fib (↑m : ℤ)
rwa₁ : (↑(Nat.fib (gcd (↑m : ℤ) n)) : ℤ) = fib (↑m : ℤ)
rwa₂ : fib (↑(gcd (↑m : ℤ) n) : ℤ) = fib (↑m : ℤ)
⊢ fib (↑m : ℤ) ∣ fib n
have rwa₃ : fib (↑m : ℤ) = fib (↑m : ℤ)
Tactic: rwa [← gcd_eq_left_iff_dvd (by simp), gcd_fib, ← fib_natCast, (gcd_eq_left_iff_dvd (by simp)).mpr]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
m n : ℤ
h : m ∣ n
⊢ fib m ∣ fib n
have inl : ∀ (m : ℕ) (h : (↑m : ℤ) ∣ n), fib (↑m : ℤ) ∣ fib n
Tactic: obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
m n : ℤ
h : m ∣ n
inl : ∀ (m : ℕ) (h : (↑m : ℤ) ∣ n), fib (↑m : ℤ) ∣ fib n
⊢ fib m ∣ fib n
have inr : ∀ (m : ℕ) (h : -(↑m : ℤ) ∣ n), fib (-(↑m : ℤ)) ∣ fib n
Tactic: obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Lemmas (goal)
Goal:
n : ℕ
⊢ fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * fib (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - HPow.hPow (β := ℕ) (fib (↑n : ℤ)) 2 =
    HPow.hPow (α := ℤ) (-1) n
have zero : fib (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * fib (HSub.hSub (α := ℤ) (↑0 : ℤ) 1) - HPow.hPow (β := ℕ) (fib (↑0 : ℤ)) 2 =
  HPow.hPow (α := ℤ) (β := ℕ) (-1) 0
Tactic: induction n with
  | zero => simp
  | succ _ _ => grind [fib_add_two]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Lemmas (goal)
Goal:
n : ℕ
zero :
  fib (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * fib (HSub.hSub (α := ℤ) (↑0 : ℤ) 1) - HPow.hPow (β := ℕ) (fib (↑0 : ℤ)) 2 =
    HPow.hPow (α := ℤ) (β := ℕ) (-1) 0
⊢ fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * fib (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - HPow.hPow (β := ℕ) (fib (↑n : ℤ)) 2 =
    HPow.hPow (α := ℤ) (-1) n
have succ : ∀ (n : ℕ),
  fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * fib (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - HPow.hPow (β := ℕ) (fib (↑n : ℤ)) 2 =
      HPow.hPow (α := ℤ) (-1) n →
    fib (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) * fib (HSub.hSub (α := ℤ) (↑(n + 1) : ℤ) 1) -
        HPow.hPow (β := ℕ) (fib (↑(n + 1) : ℤ)) 2 =
      HPow.hPow (α := ℤ) (-1) (n + 1)
Tactic: induction n with
  | zero => simp
  | succ _ _ => grind [fib_add_two]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Lemmas (goal)
Goal:
n : ℤ
⊢ fib (n + 1) * fib (n - 1) - HPow.hPow (β := ℕ) (fib n) 2 = HPow.hPow (α := ℤ) (-1) n.natAbs
have inl : ∀ (n : ℕ),
  fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * fib (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - HPow.hPow (β := ℕ) (fib (↑n : ℤ)) 2 =
    HPow.hPow (α := ℤ) (-1) (natAbs (↑n : ℤ))
Tactic: obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Lemmas (goal)
Goal:
n : ℤ
inl :
  ∀ (n : ℕ),
    fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * fib (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - HPow.hPow (β := ℕ) (fib (↑n : ℤ)) 2 =
      HPow.hPow (α := ℤ) (-1) (natAbs (↑n : ℤ))
⊢ fib (n + 1) * fib (n - 1) - HPow.hPow (β := ℕ) (fib n) 2 = HPow.hPow (α := ℤ) (-1) n.natAbs
have inr : ∀ (n : ℕ),
  fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) * fib (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) -
      HPow.hPow (β := ℕ) (fib (-(↑n : ℤ))) 2 =
    HPow.hPow (α := ℤ) (-1) (natAbs (-(↑n : ℤ)))
Tactic: obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
Cleared hypotheses: n