awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
x : Set ℤ
hn : x.Nonempty
hb : BddAbove x
⊢ IsLUB x (↑((Classical.choose (p := Membership.mem (upperBounds x)) ⋯).greatestOfBdd (P := Membership.mem x) ⋯ ⋯) : ℤ)

Tactic:
exact (isGreatest_coe_greatestOfBdd ..).isLUB

Premises used: Int.isGreatest_coe_greatestOfBdd, IsGreatest.isLUB
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
x : Set ℤ
hn : x.Nonempty
hb : BddBelow x
rw : IsGLB x (↑((Classical.choose (p := Membership.mem (lowerBounds x)) ⋯).leastOfBdd (P := Membership.mem x) ⋯ ⋯) : ℤ)
⊢ IsGLB x
    (if h : x.Nonempty ∧ BddBelow x then
      (↑((Classical.choose (p := Membership.mem (lowerBounds x)) ⋯).leastOfBdd (P := Membership.mem x) ⋯ ⋯) : ℤ)
    else 0)

Tactic:
rw [dif_pos ⟨hn, hb⟩]

Premises used: dif_pos
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
x : Set ℤ
hn : x.Nonempty
hb : BddBelow x
⊢ IsGLB x (↑((Classical.choose (p := Membership.mem (lowerBounds x)) ⋯).leastOfBdd (P := Membership.mem x) ⋯ ⋯) : ℤ)

Tactic:
(isLeast_coe_leastOfBdd ..).isGLB

Premises used: Set.Mem, setOf, IsLeast.isGLB, Int.isLeast_coe_leastOfBdd
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
x : Set ℤ
hn : x.Nonempty
hb : BddBelow x
⊢ IsGLB x (↑((Classical.choose (p := Membership.mem (lowerBounds x)) ⋯).leastOfBdd (P := Membership.mem x) ⋯ ⋯) : ℤ)

Tactic:
exact (isLeast_coe_leastOfBdd ..).isGLB

Premises used: IsLeast.isGLB, Int.isLeast_coe_leastOfBdd
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
hs : ¬BddAbove s
⊢ Eq (α := ℤ)
    (if h : s.Nonempty ∧ BddAbove s then
      (↑((Classical.choose (p := Membership.mem (upperBounds s)) ⋯).greatestOfBdd (P := Membership.mem s) ⋯ ⋯) : ℤ)
    else 0)
    (if h : Set.Nonempty (α := ℤ) ∅ ∧ BddAbove (α := ℤ) ∅ then
      (↑((Classical.choose (p := Membership.mem (γ := Set ℤ) (upperBounds ∅)) ⋯).greatestOfBdd (P :=
            Membership.mem (γ := Set ℤ) ∅) ⋯ ⋯) :
        ℤ)
    else 0)

Tactic:
simp [hs]
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
hs : ¬BddBelow s
⊢ Eq (α := ℤ)
    (if h : s.Nonempty ∧ BddBelow s then
      (↑((Classical.choose (p := Membership.mem (lowerBounds s)) ⋯).leastOfBdd (P := Membership.mem s) ⋯ ⋯) : ℤ)
    else 0)
    (if h : Set.Nonempty (α := ℤ) ∅ ∧ BddBelow (α := ℤ) ∅ then
      (↑((Classical.choose (p := Membership.mem (γ := Set ℤ) (lowerBounds ∅)) ⋯).leastOfBdd (P :=
            Membership.mem (γ := Set ℤ) ∅) ⋯ ⋯) :
        ℤ)
    else 0)

Tactic:
simp [hs]
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
inst : DecidablePred fun (x : ℤ) ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, z ≤ b
Hinh : ∃ (z : ℤ), z ∈ s
⊢ s.Nonempty ∧ BddAbove s

Tactic:
have : s.Nonempty ∧ BddAbove s := ⟨Hinh, b, Hb⟩
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
inst : DecidablePred fun (x : ℤ) ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, z ≤ b
Hinh : ∃ (z : ℤ), z ∈ s
this : s.Nonempty ∧ BddAbove s
simp :
  (↑((Classical.choose (p := Membership.mem (upperBounds s)) ⋯).greatestOfBdd (P := Membership.mem s) ⋯ ⋯) : ℤ) =
    (↑(b.greatestOfBdd (P := Membership.mem s) Hb Hinh) : ℤ)
⊢ sSup s = (↑(b.greatestOfBdd (P := Membership.mem s) Hb Hinh) : ℤ)

Tactic:
simp only [sSup, dif_pos this]

Premises used: dif_pos, SupSet.sSup
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
inst : DecidablePred fun (x : ℤ) ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, z ≤ b
Hinh : ∃ (z : ℤ), z ∈ s
this : s.Nonempty ∧ BddAbove s
⊢ (↑((Classical.choose (p := Membership.mem (upperBounds s)) ⋯).greatestOfBdd (P := Membership.mem s) ⋯ Hinh) : ℤ) =
    (↑(b.greatestOfBdd (P := Membership.mem s) Hb Hinh) : ℤ)

Tactic:
(coe_greatestOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddAbove s)) Hinh).symm

Premises used: Int.coe_greatestOfBdd_eq, Classical.choose_spec, Exists.intro, Eq.symm
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
inst : DecidablePred fun (x : ℤ) ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, z ≤ b
Hinh : ∃ (z : ℤ), z ∈ s
this : s.Nonempty ∧ BddAbove s
⊢ (↑((Classical.choose (p := Membership.mem (upperBounds s)) ⋯).greatestOfBdd (P := Membership.mem s) ⋯ ⋯) : ℤ) =
    (↑(b.greatestOfBdd (P := Membership.mem s) Hb Hinh) : ℤ)

Tactic:
convert! (coe_greatestOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddAbove s)) Hinh).symm

Premises used: Int.coe_greatestOfBdd_eq, Classical.choose_spec, Exists.intro, Eq.symm
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
⊢ ¬(Set.Nonempty (α := ℤ) ∅ ∧ BddAbove (α := ℤ) ∅)

Tactic:
simp
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
h : ¬BddAbove s
⊢ ¬(s.Nonempty ∧ BddAbove s)

Tactic:
simp [h]
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
inst : DecidablePred fun (x : ℤ) ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, b ≤ z
Hinh : ∃ (z : ℤ), z ∈ s
⊢ s.Nonempty ∧ BddBelow s

Tactic:
have : s.Nonempty ∧ BddBelow s := ⟨Hinh, b, Hb⟩
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
inst : DecidablePred fun (x : ℤ) ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, b ≤ z
Hinh : ∃ (z : ℤ), z ∈ s
this : s.Nonempty ∧ BddBelow s
simp :
  (↑((Classical.choose (p := Membership.mem (lowerBounds s)) ⋯).leastOfBdd (P := Membership.mem s) ⋯ ⋯) : ℤ) =
    (↑(b.leastOfBdd (P := Membership.mem s) Hb Hinh) : ℤ)
⊢ sInf s = (↑(b.leastOfBdd (P := Membership.mem s) Hb Hinh) : ℤ)

Tactic:
simp only [sInf, dif_pos this]

Premises used: dif_pos, InfSet.sInf
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
inst : DecidablePred fun (x : ℤ) ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, b ≤ z
Hinh : ∃ (z : ℤ), z ∈ s
this : s.Nonempty ∧ BddBelow s
⊢ (↑((Classical.choose (p := Membership.mem (lowerBounds s)) ⋯).leastOfBdd (P := Membership.mem s) ⋯ Hinh) : ℤ) =
    (↑(b.leastOfBdd (P := Membership.mem s) Hb Hinh) : ℤ)

Tactic:
(coe_leastOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddBelow s)) Hinh).symm

Premises used: Int.coe_leastOfBdd_eq, Classical.choose_spec, Exists.intro, Eq.symm
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
inst : DecidablePred fun (x : ℤ) ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, b ≤ z
Hinh : ∃ (z : ℤ), z ∈ s
this : s.Nonempty ∧ BddBelow s
⊢ (↑((Classical.choose (p := Membership.mem (lowerBounds s)) ⋯).leastOfBdd (P := Membership.mem s) ⋯ ⋯) : ℤ) =
    (↑(b.leastOfBdd (P := Membership.mem s) Hb Hinh) : ℤ)

Tactic:
convert! (coe_leastOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddBelow s)) Hinh).symm

Premises used: Int.coe_leastOfBdd_eq, Classical.choose_spec, Exists.intro, Eq.symm
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
⊢ ¬(Set.Nonempty (α := ℤ) ∅ ∧ BddBelow (α := ℤ) ∅)

Tactic:
simp
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
h : ¬BddBelow s
⊢ ¬(s.Nonempty ∧ BddBelow s)

Tactic:
simp [h]
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
h1 : s.Nonempty
h2 : BddAbove s
⊢ (↑((Classical.choose (p := Membership.mem (upperBounds s)) h2).greatestOfBdd (P := Membership.mem s) ⋯ h1) : ℤ) ∈ s

Tactic:
(greatestOfBdd _ (Classical.choose_spec h2) h1).2.1

Premises used: Classical.choose_spec, And.left, Int.greatestOfBdd, Subtype.property
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
h1 : s.Nonempty
h2 : BddAbove s
h :
  sSup s =
    (↑((Classical.choose (p := Membership.mem (upperBounds s)) h2).greatestOfBdd (P := Membership.mem s) ⋯ h1) : ℤ)
convert! : DecidablePred (Membership.mem s)
⊢ sSup s ∈ s

Tactic:
convert! (greatestOfBdd _ (Classical.choose_spec h2) h1).2.1
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
h1 : s.Nonempty
h2 : BddAbove s
⊢ sSup s =
    (↑((Classical.choose (p := Membership.mem (upperBounds s)) h2).greatestOfBdd (P := Membership.mem s) ⋯ h1) : ℤ)

Tactic:
dif_pos ⟨h1, h2⟩

Premises used: dif_pos
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
h1 : s.Nonempty
h2 : BddBelow s
⊢ (↑((Classical.choose (p := Membership.mem (lowerBounds s)) h2).leastOfBdd (P := Membership.mem s) ⋯ h1) : ℤ) ∈ s

Tactic:
(leastOfBdd _ (Classical.choose_spec h2) h1).2.1

Premises used: Int.leastOfBdd, Classical.choose_spec, And.left, Subtype.property
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
h1 : s.Nonempty
h2 : BddBelow s
h :
  sInf s = (↑((Classical.choose (p := Membership.mem (lowerBounds s)) h2).leastOfBdd (P := Membership.mem s) ⋯ h1) : ℤ)
convert! : DecidablePred (Membership.mem s)
⊢ sInf s ∈ s

Tactic:
convert! (leastOfBdd _ (Classical.choose_spec h2) h1).2.1
-- Module: Mathlib.Data.Int.ConditionallyCompleteOrder
Goal:
s : Set ℤ
h1 : s.Nonempty
h2 : BddBelow s
⊢ sInf s = (↑((Classical.choose (p := Membership.mem (lowerBounds s)) h2).leastOfBdd (P := Membership.mem s) ⋯ h1) : ℤ)

Tactic:
dif_pos ⟨h1, h2⟩

Premises used: dif_pos
-- Module: Mathlib.Data.Int.DivMod
Goal:
a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
⊢ c = 0 ∨ 0 < c

Tactic:
lia
-- Module: Mathlib.Data.Int.DivMod
Goal:
a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
inl : ∀ (hc : LE.le (α := Int) 0 0), a * (b / 0) ≤ a * b / 0
inr : ∀ (hlt : 0 < c), a * (b / c) ≤ a * b / c
⊢ a * (b / c) ≤ a * b / c

Tactic:
obtain rfl | hlt : c = 0 ∨ 0 < c := by lia

Premises used: rfl
-- Module: Mathlib.Data.Int.DivMod
Goal:
a : Int
ha : 0 ≤ a
b : Int
hc : LE.le (α := Int) 0 0
⊢ a * (b / 0) ≤ a * b / 0

Tactic:
simp
-- Module: Mathlib.Data.Int.DivMod
Goal:
a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
hlt : 0 < c
inr : a * (b / c * c) ≤ a * b
⊢ a * (b / c) ≤ a * b / c

Tactic:
rw [Int.le_ediv_iff_mul_le hlt, Int.mul_assoc]

Premises used: Int.mul_assoc, Int.le_ediv_iff_mul_le
-- Module: Mathlib.Data.Int.DivMod
Goal:
a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
hlt : 0 < c
⊢ a * (b / c * c) ≤ a * b

Tactic:
Int.mul_le_mul_of_nonneg_left (Int.ediv_mul_le b (Int.ne_of_gt hlt)) ha

Premises used: Int.ediv_mul_le, Int.ne_of_gt, Int.mul_le_mul_of_nonneg_left
-- Module: Mathlib.Data.Int.DivMod
Goal:
a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
hlt : 0 < c
⊢ a * (b / c * c) ≤ a * b

Tactic:
exact Int.mul_le_mul_of_nonneg_left (Int.ediv_mul_le b (Int.ne_of_gt hlt)) ha

Premises used: Int.ediv_mul_le, Int.ne_of_gt, Int.mul_le_mul_of_nonneg_left
-- Module: Mathlib.Data.Int.DivMod
Goal:
m n k : Int
hn : 0 ≤ n
hk : 0 ≤ k
rw : (m / n).fdiv k = m.fdiv (n * k)
rw₁ : m / n / k = m.fdiv (n * k)
rw₂ : m / n / k = m / (n * k)
rw₃ rw₄ : m / (n * k) = m / (n * k)
⊢ (m.fdiv n).fdiv k = m.fdiv (n * k)

Tactic:
rw [Int.fdiv_eq_ediv_of_nonneg _ hn,
    Int.fdiv_eq_ediv_of_nonneg _ hk,
    Int.fdiv_eq_ediv_of_nonneg _ (Int.mul_nonneg hn hk),
    ediv_ediv_of_nonneg hn]

Premises used: Int.ediv_ediv_of_nonneg, Int.fdiv_eq_ediv_of_nonneg, Int.mul_nonneg
-- Module: Mathlib.Data.Int.DivMod
Goal:
a b : Int
⊢ a % b = (a - b) % b

Tactic:
(sub_emod_right a b).symm

Premises used: Int.sub_emod_right, Eq.symm
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
⊢ fib (↑n : ℤ) = (↑(Nat.fib n) : ℤ)

Tactic:
rfl

Premises used: Int.fib, Int.toNat, rfl, ite
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
⊢ fib 0 = 0

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: Int.fib, Nat.fib, rfl, ite
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
hn : 0 ≤ n
⊢ fib n = (↑(Nat.fib n.toNat) : ℤ)

Tactic:
simp [fib, hn]

Premises used: Int.fib
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
hn : Odd n
⊢ fib n = (↑(Nat.fib n.natAbs) : ℤ)

Tactic:
grind [fib]

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

Tactic:
fib_of_odd <| odd_two_mul_add_one n

Premises used: odd_two_mul_add_one, Int.fib_of_odd
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
⊢ 0 < fib (2 * n + 1)

Tactic:
grind [fib_two_mul_add_one_eq_natFib_natAbs, Nat.fib_pos]

Premises used: Nat.fib_pos, Int.fib_two_mul_add_one_eq_natFib_natAbs
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
inl : ∀ (hn : Even n), fib (-(↑n : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ)
inr : ∀ (hn : Odd n), fib (-(↑n : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ)
⊢ fib (-(↑n : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ)

Tactic:
rcases n.even_or_odd with (hn | hn)

Premises used: Nat.even_or_odd
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
hn : Even n
⊢ fib (-(↑n : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ)

Tactic:
simp [fib, hn, pow_add]

Premises used: Int.fib, pow_add
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
hn : Odd n
⊢ fib (-(↑n : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ)

Tactic:
simp [fib_of_odd, hn]

Premises used: Int.fib_of_odd
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
obtain : ∀ (n_1 : ℕ), n = (↑n_1 : ℤ) ∨ n = -(↑n_1 : ℤ) → fib (-n) = if Even n then -fib n else fib n
⊢ fib (-n) = if Even n then -fib n else fib n

Tactic:
obtain ⟨n, _⟩ := n.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n_1 : ℤ
n : ℕ
h : n_1 = (↑n : ℤ) ∨ n_1 = -(↑n : ℤ)
⊢ fib (-n_1) = if Even n_1 then -fib n_1 else fib n_1

Tactic:
aesop (add safe (by rw [fib_neg_natCast]))
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
⊢ (↑(fib (-n)) : ℚ) = HPow.hPow (α := ℚ) (-1) (n + 1) * (↑(fib n) : ℚ)

Tactic:
aesop (add safe (by rw [fib_neg, neg_one_zpow_eq_ite]))
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
ofNat : ∀ (n : ℕ), fib (Int.ofNat n + 2) = fib (Int.ofNat n) + fib (Int.ofNat n + 1)
negSucc : ∀ (n : ℕ), fib (-[n+1] + 2) = fib -[n+1] + fib (-[n+1] + 1)
⊢ fib (n + 2) = fib n + fib (n + 1)

Tactic:
rcases n with (n | n)
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
ofNat : fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = (↑(Nat.fib n) : ℤ) + fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ fib (Int.ofNat n + 2) = fib (Int.ofNat n) + fib (Int.ofNat n + 1)

Tactic:
dsimp
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
ofNat : fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑2 : ℤ)) = (↑(Nat.fib n) : ℤ) + fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ofNat₁ : fib (↑(n + 2) : ℤ) = (↑(Nat.fib n) : ℤ) + fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ofNat₂ : fib (↑(n + 2) : ℤ) = (↑(Nat.fib n) : ℤ) + fib (↑(n + 1) : ℤ)
ofNat₃ : (↑(Nat.fib (n + 2)) : ℤ) = (↑(Nat.fib n) : ℤ) + fib (↑(n + 1) : ℤ)
ofNat₄ : (↑(Nat.fib (n + 2)) : ℤ) = HAdd.hAdd (α := ℤ) (↑(Nat.fib n) : ℤ) (↑(Nat.fib (n + 1)) : ℤ)
ofNat₅ : (↑(Nat.fib n + Nat.fib (n + 1)) : ℤ) = HAdd.hAdd (α := ℤ) (↑(Nat.fib n) : ℤ) (↑(Nat.fib (n + 1)) : ℤ)
ofNat₆ ofNat₇ :
  HAdd.hAdd (α := ℤ) (↑(Nat.fib n) : ℤ) (↑(Nat.fib (n + 1)) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑(Nat.fib n) : ℤ) (↑(Nat.fib (n + 1)) : ℤ)
⊢ fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = (↑(Nat.fib n) : ℤ) + fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)

Tactic:
rw [← Nat.cast_ofNat, ← Nat.cast_add, ← Nat.cast_add_one, fib_natCast, fib_natCast,
      Nat.fib_add_two, Nat.cast_add]

Premises used: Nat.cast_ofNat, Int.fib_natCast, Nat.fib_add_two, Nat.cast_add, Nat.cast_add_one
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
negSucc :
  fib (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 2) =
    HPow.hPow (α := ℤ) (-1) (n + 1 + 1) * (↑(Nat.fib (n + 1)) : ℤ) + fib (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 1)
⊢ fib (-[n+1] + 2) = fib -[n+1] + fib (-[n+1] + 1)

Tactic:
rw [negSucc_eq, ← Nat.cast_add_one, fib_neg_natCast]

Premises used: Int.fib_neg_natCast, Int.negSucc_eq, Nat.cast_add_one
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
negSucc :
  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) : ℤ)) 2) =
    HPow.hPow (α := ℤ) (-1) (n + 1 + 1) * (↑(Nat.fib (n + 1)) : ℤ) + fib (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 1)

Tactic:
simp only [Nat.cast_add, Nat.cast_one, neg_add_rev, reduceNeg, add_comm,
      add_assoc, reduceAdd, add_neg_cancel_comm_assoc, fib_neg_natCast]

Premises used: neg_add_rev, Int.reduceAdd, Int.fib_neg_natCast, Int.reduceNeg, add_assoc, add_comm, Nat.cast_add, add_neg_cancel_comm_assoc, Nat.cast_one
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
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:
simp [hn0]
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
hn0 : ¬n = 0
symm :
  HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ) +
      HPow.hPow (α := ℤ) (-1) (1 + (n + 1)) * (↑(Nat.fib (n + 1)) : ℤ) =
    fib (HAdd.hAdd (α := ℤ) (-(↑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)) : ℤ)

Tactic:
symm
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
hn0 : ¬n = 0
⊢ 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:
grind
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
hn0 : ¬n = 0
⊢ HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 = -(↑(n - 1) : ℤ)

Tactic:
grind
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
hn0 : ¬n = 0
⊢ HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 = -(↑(n - 1) : ℤ)

Tactic:
have : -(n : ℤ) + 1 = -((n - 1 : ℕ) : ℤ) := by grind
-- Module: Mathlib.Data.Int.Fib.Basic
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)
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)
⊢ HPow.hPow (α := ℤ) (-1) (n + 1) * HSub.hSub (α := ℤ) (↑(Nat.fib n) : ℤ) (↑(Nat.fib (n + 1)) : ℤ) =
    fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)

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

Premises used: Nat.even_or_odd, rfl
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
hn0 : ¬n + n = 0
this : HAdd.hAdd (α := ℤ) (-(↑(n + n) : ℤ)) 1 = -(↑(n + n - 1) : ℤ)
⊢ 1 ≤ 2 * n

Tactic:
grind
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
hn0 : ¬n + n = 0
this : HAdd.hAdd (α := ℤ) (-(↑(n + n) : ℤ)) 1 = -(↑(n + n - 1) : ℤ)
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)) : ℤ)
⊢ HPow.hPow (α := ℤ) (-1) (n + n + 1) * HSub.hSub (α := ℤ) (↑(Nat.fib (n + n)) : ℤ) (↑(Nat.fib (n + n + 1)) : ℤ) =
    fib (HAdd.hAdd (α := ℤ) (-(↑(n + n) : ℤ)) 1)

Tactic:
rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add, ← two_mul,
            Nat.sub_add_cancel (by grind)]

Premises used: Int.fib_neg_natCast, two_mul, pow_add, Nat.sub_add_cancel, Nat.fib_add_one
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
hn0 : ¬n + n = 0
this : HAdd.hAdd (α := ℤ) (-(↑(n + n) : ℤ)) 1 = -(↑(n + n - 1) : ℤ)
⊢ 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:
simp
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
hn0 : ¬2 * n + 1 = 0
this : HAdd.hAdd (α := ℤ) (-(↑(2 * n + 1) : ℤ)) 1 = -(↑(2 * n + 1 - 1) : ℤ)
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)) : ℤ)
⊢ 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:
rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add]

Premises used: Int.fib_neg_natCast, pow_add, Nat.fib_add_one
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℕ
hn0 : ¬2 * n + 1 = 0
this : HAdd.hAdd (α := ℤ) (-(↑(2 * n + 1) : ℤ)) 1 = -(↑(2 * n + 1 - 1) : ℤ)
⊢ 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:
simp
-- Module: Mathlib.Data.Int.Fib.Basic
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)) : ℤ)
calc₁ :
  HPow.hPow (α := ℤ) (-1) (n + 1) * HSub.hSub (α := ℤ) (↑(Nat.fib n) : ℤ) (↑(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)) : ℤ) =
    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

Premises used: HSub.hSub, Nat.cast, HAdd.hAdd, Nat.fib, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Data.Int.Fib.Basic
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)) : ℤ)
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)) : ℤ)
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)) : ℤ)
if₃ 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)) : ℤ)

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

Premises used: HSub.hSub, Nat.cast, HAdd.hAdd, Nat.fib, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
⊢ fib n = fib (n + 2) - fib (n + 1)

Tactic:
simp only [fib_add_two, add_sub_cancel_right]

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

Tactic:
simp only [fib_add_two, add_sub_cancel_left]

Premises used: add_sub_cancel_left, Int.fib_add_two
-- Module: Mathlib.Data.Int.Fib.Basic
Goal:
n : ℤ
inl : ∀ (n : ℕ), fib (↑n : ℤ) = 0 ↔ Eq (α := ℤ) (↑n : ℤ) 0
inr : ∀ (n : ℕ), fib (-(↑n : ℤ)) = 0 ↔ Eq (α := ℤ) (-(↑n : ℤ)) 0
⊢ fib n = 0 ↔ n = 0

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

Premises used: Int.eq_nat_or_neg, rfl