awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
⊢ fib (↑n : ℤ) = 0 ↔ Eq (α := ℤ) (↑n : ℤ) 0

Tactic:
simp [fib_neg_natCast]

Premises used: Int.fib_neg_natCast
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
⊢ fib (-(↑n : ℤ)) = 0 ↔ Eq (α := ℤ) (-(↑n : ℤ)) 0

Tactic:
simp [fib_neg_natCast]

Premises used: Int.fib_neg_natCast
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
x : ℤ
⊢ fib ((↑0 : ℤ) + x) = fib (HSub.hSub (α := ℤ) (↑0 : ℤ) 1) * fib x + fib (↑0 : ℤ) * fib (x + 1)

Tactic:
simp
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
x : ℤ
⊢ fib ((↑1 : ℤ) + x) = fib (HSub.hSub (α := ℤ) (↑1 : ℤ) 1) * fib x + fib (↑1 : ℤ) * fib (x + 1)

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m : ℕ
n : ℤ
⊢ fib ((↑(m + 2) : ℤ) + n) = fib ((↑m : ℤ) + n) + fib ((↑m : ℤ) + n + 1)

Tactic:
grind [fib_add_two]

Premises used: Int.fib_add_two
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m : ℕ
n : ℤ
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)
⊢ fib ((↑m : ℤ) + n) + 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]
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m : ℕ
n : ℤ
⊢ 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:
grind
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m : ℕ
n : ℤ
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)
⊢ 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:
rw [fib_natCast_add]
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m : ℕ
n : ℤ
⊢ 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:
grind
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m : ℕ
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 (HSub.hSub (α := ℤ) (↑(m + 2) : ℤ) 1) * fib n + fib (↑(m + 2) : ℤ) * fib (n + 1)

Tactic:
grind [fib_add_two]

Premises used: Int.fib_add_two
-- Module: Mathlib.Data.Int.Fib.Basic
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)
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)
⊢ fib ((↑(m + 2) : ℤ) + n) = 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]

Premises used: Int.fib, HSub.hSub, Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
x : ℤ
⊢ fib (x + (↑0 : ℤ)) = fib (x - 1) * fib (↑0 : ℤ) + fib x * fib (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1)

Tactic:
simp
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
x : ℤ
⊢ fib (x + (↑1 : ℤ)) = fib (x - 1) * fib (↑1 : ℤ) + fib x * fib (HAdd.hAdd (α := ℤ) (↑1 : ℤ) 1)

Tactic:
grind [fib_add_two, fib_two, fib_one]

Premises used: Int.fib_one, Int.fib_two, Int.fib_add_two
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
m : ℕ
⊢ fib (n + (↑(m + 2) : ℤ)) = fib ((↑m : ℤ) + n) + fib ((↑m : ℤ) + n + 1)

Tactic:
grind [fib_add_two]

Premises used: Int.fib_add_two
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
m : ℕ
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)
⊢ fib ((↑m : ℤ) + n) + 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]

Premises used: _private.0.Int.fib_natCast_add
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
m : ℕ
⊢ 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:
grind
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
m : ℕ
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)
⊢ 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:
rw [fib_natCast_add]

Premises used: _private.0.Int.fib_natCast_add
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
m : ℕ
⊢ 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:
grind
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
m : ℕ
⊢ 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 (n - 1) * fib (↑(m + 2) : ℤ) + fib n * fib (HAdd.hAdd (α := ℤ) (↑(m + 2) : ℤ) 1)

Tactic:
grind [fib_add_two]

Premises used: Int.fib_add_two
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
x : ℕ
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑x : ℤ)) (-(↑0 : ℤ))) =
    fib (HSub.hSub (α := ℤ) (-(↑x : ℤ)) 1) * fib (-(↑0 : ℤ)) + fib (-(↑x : ℤ)) * fib (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1)

Tactic:
simp
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
x : ℕ
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑x : ℤ)) (-(↑1 : ℤ))) =
    fib (HSub.hSub (α := ℤ) (-(↑x : ℤ)) 1) * fib (-(↑1 : ℤ)) + fib (-(↑x : ℤ)) * fib (HAdd.hAdd (α := ℤ) (-(↑1 : ℤ)) 1)

Tactic:
simp [sub_eq_neg_add, add_comm]

Premises used: sub_eq_neg_add, add_comm
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m n : ℕ
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) (-(↑(n + 2) : ℤ))) =
    fib (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) (-(↑n : ℤ))) - fib (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) (-(↑(n + 1) : ℤ)))

Tactic:
grind [fib_add_two]

Premises used: Int.fib_add_two
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m n : ℕ
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))
| fib (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) (-(↑n : ℤ))) - fib (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) (-(↑(n + 1) : ℤ)))

Tactic:
rw [fib_neg_natCast_add_neg_natCast, fib_neg_natCast_add_neg_natCast]
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m n : ℕ
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 : ℤ))
⊢ 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 : ℤ))

Tactic:
conv_lhs => rw [fib_neg_natCast_add_neg_natCast, fib_neg_natCast_add_neg_natCast]
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m n : ℕ
⊢ 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:
grind
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m n : ℕ
⊢ 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 : ℤ)) =
    fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib (-(↑(n + 2) : ℤ)) +
      fib (-(↑m : ℤ)) * fib (HAdd.hAdd (α := ℤ) (-(↑(n + 2) : ℤ)) 1)

Tactic:
grind [fib_add_two]

Premises used: Int.fib_add_two
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m n : ℤ
inl : ∀ (m : ℕ), fib ((↑m : ℤ) + n) = fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1)
inr : ∀ (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)

Tactic:
obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
m : ℕ
⊢ fib ((↑m : ℤ) + n) = fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1)

Tactic:
fib_natCast_add _ _

Premises used: _private.0.Int.fib_natCast_add
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
m : ℕ
⊢ fib ((↑m : ℤ) + n) = fib (HSub.hSub (α := ℤ) (↑m : ℤ) 1) * fib n + fib (↑m : ℤ) * fib (n + 1)

Tactic:
exact fib_natCast_add _ _

Premises used: _private.0.Int.fib_natCast_add
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
m : ℕ
inr :
  ∀ (n : ℕ),
    fib (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) (↑n : ℤ)) =
      fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib (↑n : ℤ) + fib (-(↑m : ℤ)) * fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
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)

Tactic:
obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m n : ℕ
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) (↑n : ℤ)) =
    fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib (↑n : ℤ) + fib (-(↑m : ℤ)) * fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)

Tactic:
fib_add_natCast _ _

Premises used: _private.0.Int.fib_add_natCast
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m n : ℕ
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) (↑n : ℤ)) =
    fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib (↑n : ℤ) + fib (-(↑m : ℤ)) * fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)

Tactic:
exact fib_add_natCast _ _

Premises used: _private.0.Int.fib_add_natCast
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m n : ℕ
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) (-(↑n : ℤ))) =
    fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib (-(↑n : ℤ)) + fib (-(↑m : ℤ)) * fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)

Tactic:
fib_neg_natCast_add_neg_natCast _ _

Premises used: _private.0.Int.fib_neg_natCast_add_neg_natCast
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m n : ℕ
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) (-(↑n : ℤ))) =
    fib (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * fib (-(↑n : ℤ)) + fib (-(↑m : ℤ)) * fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)

Tactic:
exact fib_neg_natCast_add_neg_natCast _ _

Premises used: _private.0.Int.fib_neg_natCast_add_neg_natCast
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
rw : fib (n - 1) * fib n + fib n * fib (n + 1) = fib n * (2 * fib (n + 1) - fib n)
⊢ fib (2 * n) = fib n * (2 * fib (n + 1) - fib n)

Tactic:
rw [two_mul, fib_add]

Premises used: two_mul, Int.fib_add
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
⊢ fib (n - 1) * fib n + fib n * fib (n + 1) = fib n * (2 * fib (n + 1) - fib n)

Tactic:
grind [fib_add_two]

Premises used: Int.fib_add_two
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
⊢ fib (n + 1 + n) = fib (n + 1 - 1) * fib n + fib (n + 1) * fib (n + 1)

Tactic:
have := fib_add (n + 1) n
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
this : fib (n + 1 + n) = fib (n + 1 - 1) * fib n + fib (n + 1) * fib (n + 1)
⊢ fib (2 * n + 1) = HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2

Tactic:
grind
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
rw : fib (n + 1) * (2 * fib (n + 1 + 1) - fib (n + 1)) = fib (n + 1) * (2 * fib n + fib (n + 1))
⊢ fib (2 * n + 2) = fib (n + 1) * (2 * fib n + fib (n + 1))

Tactic:
rw [← mul_add_one, fib_two_mul]

Premises used: Int.fib_two_mul, mul_add_one
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
⊢ fib (n + 1) * (2 * fib (n + 1 + 1) - fib (n + 1)) = fib (n + 1) * (2 * fib n + fib (n + 1))

Tactic:
grind [fib_add_two]

Premises used: Int.fib_add_two
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m n : ℤ
inl : ∀ (m : ℕ), (fib (↑m : ℤ)).gcd (fib n) = Nat.fib (gcd (↑m : ℤ) n)
inr : ∀ (m : ℕ), (fib (-(↑m : ℤ))).gcd (fib n) = Nat.fib (gcd (-(↑m : ℤ)) n)
⊢ (fib m).gcd (fib n) = Nat.fib (m.gcd n)

Tactic:
obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
m : ℕ
inl : ∀ (n : ℕ), (fib (↑m : ℤ)).gcd (fib (↑n : ℤ)) = Nat.fib (gcd (↑m : ℤ) (↑n : ℤ))
inl₁ : ∀ (n : ℕ), (fib (↑m : ℤ)).gcd (fib (-(↑n : ℤ))) = Nat.fib (gcd (↑m : ℤ) (-(↑n : ℤ)))
⊢ (fib (↑m : ℤ)).gcd (fib n) = Nat.fib (gcd (↑m : ℤ) n)

Tactic:
obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
m : ℕ
inr : ∀ (n : ℕ), (fib (-(↑m : ℤ))).gcd (fib (↑n : ℤ)) = Nat.fib (gcd (-(↑m : ℤ)) (↑n : ℤ))
inr₁ : ∀ (n : ℕ), (fib (-(↑m : ℤ))).gcd (fib (-(↑n : ℤ))) = Nat.fib (gcd (-(↑m : ℤ)) (-(↑n : ℤ)))
⊢ (fib (-(↑m : ℤ))).gcd (fib n) = Nat.fib (gcd (-(↑m : ℤ)) n)

Tactic:
obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m n : ℕ
⊢ (fib (↑m : ℤ)).gcd (fib (↑n : ℤ)) = Nat.fib (gcd (↑m : ℤ) (↑n : ℤ))

Tactic:
simp [fib_neg, Nat.fib_gcd, apply_ite, apply_ite_left]

Premises used: apply_ite, Nat.fib_gcd, apply_ite_left, Int.fib_neg
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m n : ℕ
⊢ (fib (↑m : ℤ)).gcd (fib (-(↑n : ℤ))) = Nat.fib (gcd (↑m : ℤ) (-(↑n : ℤ)))

Tactic:
simp [fib_neg, Nat.fib_gcd, apply_ite, apply_ite_left]

Premises used: apply_ite, Nat.fib_gcd, apply_ite_left, Int.fib_neg
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m n : ℕ
⊢ (fib (-(↑m : ℤ))).gcd (fib (↑n : ℤ)) = Nat.fib (gcd (-(↑m : ℤ)) (↑n : ℤ))

Tactic:
simp [fib_neg, Nat.fib_gcd, apply_ite, apply_ite_left]

Premises used: apply_ite, Nat.fib_gcd, apply_ite_left, Int.fib_neg
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m n : ℕ
⊢ (fib (-(↑m : ℤ))).gcd (fib (-(↑n : ℤ))) = Nat.fib (gcd (-(↑m : ℤ)) (-(↑n : ℤ)))

Tactic:
simp [fib_neg, Nat.fib_gcd, apply_ite, apply_ite_left]

Premises used: apply_ite, Nat.fib_gcd, apply_ite_left, Int.fib_neg
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m n : ℤ
⊢ fib (↑(m.gcd n) : ℤ) = (↑((fib m).gcd (fib n)) : ℤ)

Tactic:
simpa using (gcd_fib m n).symm

Premises used: Eq.symm, Int.gcd_fib
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m : ℕ
n : ℤ
h : (↑m : ℤ) ∣ n
⊢ 0 ≤ fib (↑m : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m : ℕ
n : ℤ
h : (↑m : ℤ) ∣ n
⊢ LE.le (α := ℤ) 0 (↑m : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Int.Fib.Basic
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 : ℤ)
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 (by simp), gcd_fib, ← fib_natCast, (gcd_eq_left_iff_dvd (by simp)).mpr]

Premises used: Iff.mpr, Int.gcd_eq_left_iff_dvd, Int.fib_natCast, Int.gcd_fib
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
m n : ℤ
h : m ∣ n
inl : ∀ (m : ℕ) (h : (↑m : ℤ) ∣ n), fib (↑m : ℤ) ∣ fib n
inr : ∀ (m : ℕ) (h : -(↑m : ℤ) ∣ n), fib (-(↑m : ℤ)) ∣ fib n
⊢ fib m ∣ fib n

Tactic:
obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
m : ℕ
h : (↑m : ℤ) ∣ n
⊢ fib (↑m : ℤ) ∣ fib n

Tactic:
fib_natCast_dvd h

Premises used: _private.0.Int.fib_natCast_dvd
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
m : ℕ
h : (↑m : ℤ) ∣ n
⊢ fib (↑m : ℤ) ∣ fib n

Tactic:
exact fib_natCast_dvd h

Premises used: _private.0.Int.fib_natCast_dvd
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
m : ℕ
h : -(↑m : ℤ) ∣ n
⊢ fib (-(↑m : ℤ)) ∣ fib n

Tactic:
simp [fib_neg_natCast, ← fib_natCast, fib_natCast_dvd <| Int.neg_dvd.mp h]

Premises used: Int.fib_neg_natCast, Int.fib_natCast, _private.0.Int.fib_natCast_dvd, Int.neg_dvd, Iff.mp
-- Module: Mathlib.Data.Int.Fib.Lemmas
Goal:
⊢ fib (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * fib (HSub.hSub (α := ℤ) (↑0 : ℤ) 1) - HPow.hPow (β := ℕ) (fib (↑0 : ℤ)) 2 =
    HPow.hPow (α := ℤ) (β := ℕ) (-1) 0

Tactic:
simp
-- Module: Mathlib.Data.Int.Fib.Lemmas
Goal:
n : ℕ
h :
  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:
grind [fib_add_two]

Premises used: Int.fib_add_two
-- Module: Mathlib.Data.Int.Fib.Lemmas
Goal:
n : ℕ
zero :
  fib (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * fib (HSub.hSub (α := ℤ) (↑0 : ℤ) 1) - HPow.hPow (β := ℕ) (fib (↑0 : ℤ)) 2 =
    HPow.hPow (α := ℤ) (β := ℕ) (-1) 0
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)
⊢ fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * fib (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - HPow.hPow (β := ℕ) (fib (↑n : ℤ)) 2 =
    HPow.hPow (α := ℤ) (-1) n

Tactic:
induction n with
  | zero => simp
  | succ _ _ => grind [fib_add_two]

Premises used: Int.succ, Int.fib_add_two
-- Module: Mathlib.Data.Int.Fib.Lemmas
Goal:
n : ℤ
inl :
  ∀ (n : ℕ),
    fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * fib (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - HPow.hPow (β := ℕ) (fib (↑n : ℤ)) 2 =
      HPow.hPow (α := ℤ) (-1) (natAbs (↑n : ℤ))
inr :
  ∀ (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

Tactic:
obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Data.Int.Fib.Lemmas
Goal:
n : ℕ
⊢ fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * fib (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - HPow.hPow (β := ℕ) (fib (↑n : ℤ)) 2 =
    HPow.hPow (α := ℤ) (-1) (natAbs (↑n : ℤ))

Tactic:
fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq n

Premises used: _private.0.Int.fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq, Int.natAbs
-- Module: Mathlib.Data.Int.Fib.Lemmas
Goal:
n : ℕ
⊢ fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * fib (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - HPow.hPow (β := ℕ) (fib (↑n : ℤ)) 2 =
    HPow.hPow (α := ℤ) (-1) (natAbs (↑n : ℤ))

Tactic:
exact fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq n

Premises used: _private.0.Int.fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq
-- Module: Mathlib.Data.Int.Fib.Lemmas
Goal:
n : ℕ
hn : n = 0
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) * fib (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) -
      HPow.hPow (β := ℕ) (fib (-(↑n : ℤ))) 2 =
    HPow.hPow (α := ℤ) (-1) (natAbs (-(↑n : ℤ)))

Tactic:
simp [hn]
-- Module: Mathlib.Data.Int.Fib.Lemmas
Goal:
n : ℕ
hn : ¬n = 0
obtain :
  ∀ (i : ℕ) (hn : ¬i + 1 = 0),
    fib (HAdd.hAdd (α := ℤ) (-(↑(i + 1) : ℤ)) 1) * fib (HSub.hSub (α := ℤ) (-(↑(i + 1) : ℤ)) 1) -
        HPow.hPow (β := ℕ) (fib (-(↑(i + 1) : ℤ))) 2 =
      HPow.hPow (α := ℤ) (-1) (natAbs (-(↑(i + 1) : ℤ)))
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) * fib (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) -
      HPow.hPow (β := ℕ) (fib (-(↑n : ℤ))) 2 =
    HPow.hPow (α := ℤ) (-1) (natAbs (-(↑n : ℤ)))

Tactic:
obtain ⟨i, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn

Premises used: Nat.exists_eq_add_one_of_ne_zero, rfl
-- Module: Mathlib.Data.Int.Fib.Lemmas
Goal:
i : ℕ
hn : ¬i + 1 = 0
⊢ HAdd.hAdd (α := ℤ) (-(↑(i + 1) : ℤ)) 1 = -(↑i : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Int.Fib.Lemmas
Goal:
i : ℕ
hn : ¬i + 1 = 0
simp_rw :
  ((if Even (α := ℤ) (↑i : ℤ) then -fib (↑i : ℤ) else fib (↑i : ℤ)) *
        if Even (HAdd.hAdd (α := ℤ) (↑(i + 1) : ℤ) 1) then -fib (HAdd.hAdd (α := ℤ) (↑(i + 1) : ℤ) 1)
        else fib (HAdd.hAdd (α := ℤ) (↑(i + 1) : ℤ) 1)) +
      -HPow.hPow (β := ℕ) (if Even (α := ℤ) (↑(i + 1) : ℤ) then -fib (↑(i + 1) : ℤ) else fib (↑(i + 1) : ℤ)) 2 =
    fib (HAdd.hAdd (α := ℤ) (↑(i + 1) : ℤ) 1) * fib (HSub.hSub (α := ℤ) (↑(i + 1) : ℤ) 1) -
      HPow.hPow (β := ℕ) (fib (↑(i + 1) : ℤ)) 2
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑(i + 1) : ℤ)) 1) * fib (HSub.hSub (α := ℤ) (-(↑(i + 1) : ℤ)) 1) -
      HPow.hPow (β := ℕ) (fib (-(↑(i + 1) : ℤ))) 2 =
    HPow.hPow (α := ℤ) (-1) (natAbs (-(↑(i + 1) : ℤ)))

Tactic:
simp_rw [show -((i + 1 : ℕ) : ℤ) + 1 = -i by simp, sub_eq_add_neg, ← neg_add, fib_neg,
      natAbs_neg, natAbs_natCast, ← fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq]

Premises used: sub_eq_add_neg, neg_add, Int.fib_neg, _private.0.Int.fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq, Int.natAbs_natCast, Int.natAbs_neg