awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
M : Type u_5
inst : Monoid M
f g : ℤ →* M
h_neg_one : Eq (α := M) ((f : (a : ℤ) → M) (-1) : M) ((g : (a : ℤ) → M) (-1) : M)
h_nat : f.comp (↑ofNatHom : ℕ →* ℤ) = g.comp (↑ofNatHom : ℕ →* ℤ)
x : ℕ
⊢ Eq (α := M) ((f : (a : ℤ) → M) -[x+1] : M) ((g : (a : ℤ) → M) -[x+1] : M)
have h : HMul.hMul (α := M) (β := M) ((f : (a : ℤ) → M) (-1) : M) ((f : (a : ℤ) → M) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : M) =
  HMul.hMul (α := M) (β := M) ((g : (a : ℤ) → M) (-1) : M) ((g : (a : ℤ) → M) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : M)
Tactic: rw [Int.negSucc_eq, ← neg_one_mul, f.map_mul, g.map_mul]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
M : Type u_5
inst : Monoid M
f g : ℤ →* M
h_neg_one : Eq (α := M) ((f : (a : ℤ) → M) (-1) : M) ((g : (a : ℤ) → M) (-1) : M)
h_nat : f.comp (↑ofNatHom : ℕ →* ℤ) = g.comp (↑ofNatHom : ℕ →* ℤ)
x : ℕ
⊢ HMul.hMul (α := M) (β := M) ((f : (a : ℤ) → M) (-1) : M) ((f : (a : ℤ) → M) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : M) =
    HMul.hMul (α := M) (β := M) ((g : (a : ℤ) → M) (-1) : M) ((g : (a : ℤ) → M) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : M)
have h : Eq (α := M) ((f : (a : ℤ) → M) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : M)
  ((g : (a : ℤ) → M) (HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : M)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : Group α
f : Multiplicative ℤ →* α
n : Multiplicative ℤ
⊢ (f : (a : Multiplicative ℤ) → α) n =
    HPow.hPow (α := α) (β := ℤ)
      ((f : (a : Multiplicative ℤ) → α) ((ofAdd : (a : ℤ) → Multiplicative ℤ) 1 : Multiplicative ℤ) : α)
      ((toAdd : (a : Multiplicative ℤ) → ℤ) n : ℤ)
have rw : (f : (a : Multiplicative ℤ) → α) n =
  HPow.hPow (α := α) (β := ℤ) ((Equiv.symm (zpowersHom α) : (a : Multiplicative ℤ →* α) → α) f : α)
    ((toAdd : (a : Multiplicative ℤ) → ℤ) n : ℤ)
Tactic: rw [← zpowersHom_symm_apply, ← zpowersHom_apply, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : Group α
f : Multiplicative ℤ →* α
n : Multiplicative ℤ
rw :
  (f : (a : Multiplicative ℤ) → α) n =
    HPow.hPow (α := α) (β := ℤ) ((Equiv.symm (zpowersHom α) : (a : Multiplicative ℤ →* α) → α) f : α)
      ((toAdd : (a : Multiplicative ℤ) → ℤ) n : ℤ)
⊢ (f : (a : Multiplicative ℤ) → α) n =
    HPow.hPow (α := α) (β := ℤ)
      ((f : (a : Multiplicative ℤ) → α) ((ofAdd : (a : ℤ) → Multiplicative ℤ) 1 : Multiplicative ℤ) : α)
      ((toAdd : (a : Multiplicative ℤ) → ℤ) n : ℤ)
have rw₁ : Eq (α := α) ((f : (a : Multiplicative ℤ) → α) n : α)
  ((((zpowersHom α : (a : α) → Multiplicative ℤ →* α)
            ((Equiv.symm (zpowersHom α) : (a : Multiplicative ℤ →* α) → α) f) :
          Multiplicative ℤ →* α) :
        (a : Multiplicative ℤ) → α)
      n :
    α)
Tactic: rw [← zpowersHom_symm_apply, ← zpowersHom_apply, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : Group α
f : Multiplicative ℤ →* α
n : Multiplicative ℤ
rw :
  (f : (a : Multiplicative ℤ) → α) n =
    HPow.hPow (α := α) (β := ℤ) ((Equiv.symm (zpowersHom α) : (a : Multiplicative ℤ →* α) → α) f : α)
      ((toAdd : (a : Multiplicative ℤ) → ℤ) n : ℤ)
rw₁ :
  Eq (α := α) ((f : (a : Multiplicative ℤ) → α) n : α)
    ((((zpowersHom α : (a : α) → Multiplicative ℤ →* α)
              ((Equiv.symm (zpowersHom α) : (a : Multiplicative ℤ →* α) → α) f) :
            Multiplicative ℤ →* α) :
          (a : Multiplicative ℤ) → α)
        n :
      α)
⊢ (f : (a : Multiplicative ℤ) → α) n =
    HPow.hPow (α := α) (β := ℤ)
      ((f : (a : Multiplicative ℤ) → α) ((ofAdd : (a : ℤ) → Multiplicative ℤ) 1 : Multiplicative ℤ) : α)
      ((toAdd : (a : Multiplicative ℤ) → ℤ) n : ℤ)
have rw₂ : Eq (α := α) ((f : (a : Multiplicative ℤ) → α) n : α) ((f : (a : Multiplicative ℤ) → α) n : α)
Tactic: rw [← zpowersHom_symm_apply, ← zpowersHom_apply, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
β : Type u_4
inst : AddGroup β
f : ℤ →+ β
n : ℤ
⊢ (f : (a : ℤ) → β) n = HSMul.hSMul (β := β) n ((f : (a : ℤ) → β) 1 : β)
have rw : (f : (a : ℤ) → β) n = HSMul.hSMul (β := β) n ((Equiv.symm (zmultiplesHom β) : (a : ℤ →+ β) → β) f : β)
Tactic: rw [← zmultiplesHom_symm_apply, ← zmultiplesHom_apply, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
β : Type u_4
inst : AddGroup β
f : ℤ →+ β
n : ℤ
rw : (f : (a : ℤ) → β) n = HSMul.hSMul (β := β) n ((Equiv.symm (zmultiplesHom β) : (a : ℤ →+ β) → β) f : β)
⊢ (f : (a : ℤ) → β) n = HSMul.hSMul (β := β) n ((f : (a : ℤ) → β) 1 : β)
have rw₁ : Eq (α := β) ((f : (a : ℤ) → β) n : β)
  ((((zmultiplesHom β : (a : β) → ℤ →+ β) ((Equiv.symm (zmultiplesHom β) : (a : ℤ →+ β) → β) f) : ℤ →+ β) : (a : ℤ) → β)
      n :
    β)
Tactic: rw [← zmultiplesHom_symm_apply, ← zmultiplesHom_apply, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
β : Type u_4
inst : AddGroup β
f : ℤ →+ β
n : ℤ
rw : (f : (a : ℤ) → β) n = HSMul.hSMul (β := β) n ((Equiv.symm (zmultiplesHom β) : (a : ℤ →+ β) → β) f : β)
rw₁ :
  Eq (α := β) ((f : (a : ℤ) → β) n : β)
    ((((zmultiplesHom β : (a : β) → ℤ →+ β) ((Equiv.symm (zmultiplesHom β) : (a : ℤ →+ β) → β) f) : ℤ →+ β) :
          (a : ℤ) → β)
        n :
      β)
⊢ (f : (a : ℤ) → β) n = HSMul.hSMul (β := β) n ((f : (a : ℤ) → β) 1 : β)
have rw₂ : Eq (α := β) ((f : (a : ℤ) → β) n : β) ((f : (a : ℤ) → β) n : β)
Tactic: rw [← zmultiplesHom_symm_apply, ← zmultiplesHom_apply, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : AddGroupWithOne α
inst_1 : AddGroupWithOne β
x : ℕ
⊢ Eq (α := α × β) ((↑(↑x : ℤ) : α), (↑(↑x : ℤ) : β)) (↑x : α × β)
have fst : Eq.{u_1 + 1} (α := α) ((↑(↑x : ℤ) : α), (↑(↑x : ℤ) : β)).1 (↑x : α × β).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : AddGroupWithOne α
inst_1 : AddGroupWithOne β
x : ℕ
fst : Eq.{u_1 + 1} (α := α) ((↑(↑x : ℤ) : α), (↑(↑x : ℤ) : β)).1 (↑x : α × β).1
⊢ Eq (α := α × β) ((↑(↑x : ℤ) : α), (↑(↑x : ℤ) : β)) (↑x : α × β)
have snd : Eq.{u_2 + 1} (α := β) ((↑(↑x : ℤ) : α), (↑(↑x : ℤ) : β)).2 (↑x : α × β).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : AddGroupWithOne α
inst_1 : AddGroupWithOne β
x : ℕ
⊢ Eq (α := α × β) ((↑(Int.negSucc x) : α), (↑(Int.negSucc x) : β)) (-(↑(x + 1) : α × β))
have fst : Eq.{u_1 + 1} (α := α) ((↑(Int.negSucc x) : α), (↑(Int.negSucc x) : β)).1 (-(↑(x + 1) : α × β)).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : AddGroupWithOne α
inst_1 : AddGroupWithOne β
x : ℕ
fst : Eq.{u_1 + 1} (α := α) ((↑(Int.negSucc x) : α), (↑(Int.negSucc x) : β)).1 (-(↑(x + 1) : α × β)).1
⊢ Eq (α := α × β) ((↑(Int.negSucc x) : α), (↑(Int.negSucc x) : β)) (-(↑(x + 1) : α × β))
have snd : Eq.{u_2 + 1} (α := β) ((↑(Int.negSucc x) : α), (↑(Int.negSucc x) : β)).2 (-(↑(x + 1) : α × β)).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Int.CharZero (goal)
Goal:
k : Type u_3
inst : DivisionRing k
inst_1 : CharZero k
m n : ℤ
n_dvd : n ∣ m
⊢ (↑(m / n) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)
have inl : ∀ (n_dvd : 0 ∣ m), (↑(m / 0) : k) = HDiv.hDiv (α := k) (↑m : k) (↑0 : k)
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n, n_dvd
-- Lean 4 proof step from Mathlib.Data.Int.CharZero (goal)
Goal:
k : Type u_3
inst : DivisionRing k
inst_1 : CharZero k
m n : ℤ
n_dvd : n ∣ m
inl : ∀ (n_dvd : 0 ∣ m), (↑(m / 0) : k) = HDiv.hDiv (α := k) (↑m : k) (↑0 : k)
⊢ (↑(m / n) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)
have inr : ∀ (hn : n ≠ 0), (↑(m / n) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
-- Lean 4 proof step from Mathlib.Data.Int.CharZero (goal)
Goal:
k : Type u_3
inst : DivisionRing k
inst_1 : CharZero k
m n : ℕ
n_dvd : n ∣ m
⊢ (↑(HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑n : ℤ)) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)
have rw : HDiv.hDiv (α := k) (↑(↑m : ℤ) : k) (↑(↑n : ℤ) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)
Tactic: rw [cast_div_charZero (Int.ofNat_dvd.mpr n_dvd), cast_natCast, cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Int.CharZero (goal)
Goal:
k : Type u_3
inst : DivisionRing k
inst_1 : CharZero k
m n : ℕ
n_dvd : n ∣ m
rw : HDiv.hDiv (α := k) (↑(↑m : ℤ) : k) (↑(↑n : ℤ) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)
⊢ (↑(HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑n : ℤ)) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)
have rw₁ : HDiv.hDiv (α := k) (↑m : k) (↑(↑n : ℤ) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)
Tactic: rw [cast_div_charZero (Int.ofNat_dvd.mpr n_dvd), cast_natCast, cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Int.CharZero (goal)
Goal:
k : Type u_3
inst : DivisionRing k
inst_1 : CharZero k
m n : ℕ
n_dvd : n ∣ m
rw : HDiv.hDiv (α := k) (↑(↑m : ℤ) : k) (↑(↑n : ℤ) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)
rw₁ : HDiv.hDiv (α := k) (↑m : k) (↑(↑n : ℤ) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)
⊢ (↑(HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑n : ℤ)) : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)
have rw₂ : HDiv.hDiv (α := k) (↑m : k) (↑n : k) = HDiv.hDiv (α := k) (↑m : k) (↑n : k)
Tactic: rw [cast_div_charZero (Int.ofNat_dvd.mpr n_dvd), cast_natCast, cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Int.ConditionallyCompleteOrder (goal)
Goal:
x : Set ℤ
hn : x.Nonempty
hb : BddAbove x
⊢ IsLUB x
    (if h : x.Nonempty ∧ BddAbove x then
      (↑((Classical.choose (p := Membership.mem (upperBounds x)) ⋯).greatestOfBdd (P := Membership.mem x) ⋯ ⋯) : ℤ)
    else 0)
have rw : IsLUB x (↑((Classical.choose (p := Membership.mem (upperBounds x)) sorry).greatestOfBdd (P := Membership.mem x) sorry sorry) : ℤ)
Tactic: rw [dif_pos ⟨hn, hb⟩]
-- Lean 4 proof step from Mathlib.Data.Int.ConditionallyCompleteOrder (goal)
Goal:
x : Set ℤ
hn : x.Nonempty
hb : BddBelow x
⊢ IsGLB x
    (if h : x.Nonempty ∧ BddBelow x then
      (↑((Classical.choose (p := Membership.mem (lowerBounds x)) ⋯).leastOfBdd (P := Membership.mem x) ⋯ ⋯) : ℤ)
    else 0)
have rw : IsGLB x (↑((Classical.choose (p := Membership.mem (lowerBounds x)) sorry).leastOfBdd (P := Membership.mem x) sorry sorry) : ℤ)
Tactic: rw [dif_pos ⟨hn, hb⟩]
-- Lean 4 proof step from Mathlib.Data.Int.ConditionallyCompleteOrder (hypothesis)
Goal:
s : Set ℤ
inst : DecidablePred fun (x : ℤ) ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, z ≤ b
Hinh : ∃ (z : ℤ), z ∈ s
⊢ sSup s = (↑(b.greatestOfBdd (P := Membership.mem s) Hb Hinh) : ℤ)
have this : s.Nonempty ∧ BddAbove s
Tactic: have : s.Nonempty ∧ BddAbove s := ⟨Hinh, b, Hb⟩
-- Lean 4 proof step from Mathlib.Data.Int.ConditionallyCompleteOrder (goal)
Goal:
s : Set ℤ
inst : DecidablePred fun (x : ℤ) ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, z ≤ b
Hinh : ∃ (z : ℤ), z ∈ s
this : s.Nonempty ∧ BddAbove s
⊢ sSup s = (↑(b.greatestOfBdd (P := Membership.mem s) Hb Hinh) : ℤ)
have simp : (↑((Classical.choose (p := Membership.mem (upperBounds s)) sorry).greatestOfBdd (P := Membership.mem s) sorry sorry) : ℤ) =
  (↑(b.greatestOfBdd (P := Membership.mem s) Hb Hinh) : ℤ)
Tactic: simp only [sSup, dif_pos this]
-- Lean 4 proof step from Mathlib.Data.Int.ConditionallyCompleteOrder (hypothesis)
Goal:
s : Set ℤ
inst : DecidablePred fun (x : ℤ) ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, b ≤ z
Hinh : ∃ (z : ℤ), z ∈ s
⊢ sInf s = (↑(b.leastOfBdd (P := Membership.mem s) Hb Hinh) : ℤ)
have this : s.Nonempty ∧ BddBelow s
Tactic: have : s.Nonempty ∧ BddBelow s := ⟨Hinh, b, Hb⟩
-- Lean 4 proof step from Mathlib.Data.Int.ConditionallyCompleteOrder (goal)
Goal:
s : Set ℤ
inst : DecidablePred fun (x : ℤ) ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, b ≤ z
Hinh : ∃ (z : ℤ), z ∈ s
this : s.Nonempty ∧ BddBelow s
⊢ sInf s = (↑(b.leastOfBdd (P := Membership.mem s) Hb Hinh) : ℤ)
have simp : (↑((Classical.choose (p := Membership.mem (lowerBounds s)) sorry).leastOfBdd (P := Membership.mem s) sorry sorry) : ℤ) =
  (↑(b.leastOfBdd (P := Membership.mem s) Hb Hinh) : ℤ)
Tactic: simp only [sInf, dif_pos this]
-- Lean 4 proof step from Mathlib.Data.Int.ConditionallyCompleteOrder (goal)
Goal:
s : Set ℤ
h1 : s.Nonempty
h2 : BddAbove s
⊢ sSup s ∈ s
have h : sSup s = (↑((Classical.choose (p := Membership.mem (upperBounds s)) h2).greatestOfBdd (P := Membership.mem s) sorry h1) : ℤ)
Tactic: convert! (greatestOfBdd _ (Classical.choose_spec h2) h1).2.1
-- Lean 4 proof step from Mathlib.Data.Int.ConditionallyCompleteOrder (goal)
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) : ℤ)
⊢ sSup s ∈ s
have convert! : DecidablePred (Membership.mem s)
Tactic: convert! (greatestOfBdd _ (Classical.choose_spec h2) h1).2.1
-- Lean 4 proof step from Mathlib.Data.Int.ConditionallyCompleteOrder (goal)
Goal:
s : Set ℤ
h1 : s.Nonempty
h2 : BddBelow s
⊢ sInf s ∈ s
have h : sInf s = (↑((Classical.choose (p := Membership.mem (lowerBounds s)) h2).leastOfBdd (P := Membership.mem s) sorry h1) : ℤ)
Tactic: convert! (leastOfBdd _ (Classical.choose_spec h2) h1).2.1
-- Lean 4 proof step from Mathlib.Data.Int.ConditionallyCompleteOrder (goal)
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) : ℤ)
⊢ sInf s ∈ s
have convert! : DecidablePred (Membership.mem s)
Tactic: convert! (leastOfBdd _ (Classical.choose_spec h2) h1).2.1
-- Lean 4 proof step from Mathlib.Data.Int.DivMod (goal)
Goal:
a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
⊢ a * (b / c) ≤ a * b / c
have inl : ∀ (hc : LE.le (α := Int) 0 0), a * (b / 0) ≤ a * b / 0
Tactic: obtain rfl | hlt : c = 0 ∨ 0 < c := by lia
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Data.Int.DivMod (goal)
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
⊢ a * (b / c) ≤ a * b / c
have inr : ∀ (hlt : 0 < c), a * (b / c) ≤ a * b / c
Tactic: obtain rfl | hlt : c = 0 ∨ 0 < c := by lia
-- Lean 4 proof step from Mathlib.Data.Int.DivMod (goal)
Goal:
a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
hlt : 0 < c
⊢ a * (b / c) ≤ a * b / c
have inr : a * (b / c * c) ≤ a * b
Tactic: rw [Int.le_ediv_iff_mul_le hlt, Int.mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Int.DivMod (goal)
Goal:
m n k : Int
hn : 0 ≤ n
hk : 0 ≤ k
⊢ (m.fdiv n).fdiv k = m.fdiv (n * k)
have rw : (m / 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]
-- Lean 4 proof step from Mathlib.Data.Int.DivMod (goal)
Goal:
m n k : Int
hn : 0 ≤ n
hk : 0 ≤ k
rw : (m / n).fdiv k = m.fdiv (n * k)
⊢ (m.fdiv n).fdiv k = m.fdiv (n * k)
have rw₁ : m / n / 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]
-- Lean 4 proof step from Mathlib.Data.Int.DivMod (goal)
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)
⊢ (m.fdiv n).fdiv k = m.fdiv (n * k)
have rw₂ : m / n / k = m / (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]
-- Lean 4 proof step from Mathlib.Data.Int.DivMod (goal)
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)
⊢ (m.fdiv n).fdiv k = m.fdiv (n * k)
have rw₃ : m / (n * k) = m / (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]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℕ
⊢ fib (-(↑n : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ)
have inl : ∀ (hn : Even n), fib (-(↑n : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ)
Tactic: rcases n.even_or_odd with (hn | hn)
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℕ
inl : ∀ (hn : Even n), fib (-(↑n : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ)
⊢ fib (-(↑n : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ)
have inr : ∀ (hn : Odd n), fib (-(↑n : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ)
Tactic: rcases n.even_or_odd with (hn | hn)
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℤ
⊢ fib (-n) = if Even n then -fib n else fib n
have obtain : ∀ (n_1 : ℕ), n = (↑n_1 : ℤ) ∨ n = -(↑n_1 : ℤ) → fib (-n) = if Even n then -fib n else fib n
Tactic: obtain ⟨n, _⟩ := n.eq_nat_or_neg
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℤ
⊢ fib (n + 2) = fib n + fib (n + 1)
have ofNat : ∀ (n : ℕ), fib (ofNat n + 2) = fib (ofNat n) + fib (ofNat n + 1)
Tactic: rcases n with (n | n)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℤ
ofNat : ∀ (n : ℕ), fib (Int.ofNat n + 2) = fib (Int.ofNat n) + fib (Int.ofNat n + 1)
⊢ fib (n + 2) = fib n + fib (n + 1)
have negSucc : ∀ (n : ℕ), fib (-[n+1] + 2) = fib -[n+1] + fib (-[n+1] + 1)
Tactic: rcases n with (n | n)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℕ
⊢ fib (ofNat n + 2) = fib (ofNat n) + fib (ofNat n + 1)
have ofNat : fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = (↑(Nat.fib n) : ℤ) + fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℕ
⊢ fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = (↑(Nat.fib n) : ℤ) + fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
have ofNat : 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]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℕ
ofNat : fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑2 : ℤ)) = (↑(Nat.fib n) : ℤ) + fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = (↑(Nat.fib n) : ℤ) + fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
have ofNat₁ : fib (↑(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]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
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)
⊢ fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = (↑(Nat.fib n) : ℤ) + fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
have ofNat₂ : fib (↑(n + 2) : ℤ) = (↑(Nat.fib n) : ℤ) + fib (↑(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]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
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) : ℤ)
⊢ fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = (↑(Nat.fib n) : ℤ) + fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
have ofNat₃ : (↑(Nat.fib (n + 2)) : ℤ) = (↑(Nat.fib n) : ℤ) + fib (↑(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]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
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) : ℤ)
⊢ fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = (↑(Nat.fib n) : ℤ) + fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
have ofNat₄ : (↑(Nat.fib (n + 2)) : ℤ) = HAdd.hAdd (α := ℤ) (↑(Nat.fib n) : ℤ) (↑(Nat.fib (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]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
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)) : ℤ)
⊢ fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = (↑(Nat.fib n) : ℤ) + fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
have ofNat₅ : (↑(Nat.fib n + Nat.fib (n + 1)) : ℤ) = HAdd.hAdd (α := ℤ) (↑(Nat.fib n) : ℤ) (↑(Nat.fib (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]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
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)) : ℤ)
⊢ fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = (↑(Nat.fib n) : ℤ) + fib (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
have ofNat₆ : HAdd.hAdd (α := ℤ) (↑(Nat.fib n) : ℤ) (↑(Nat.fib (n + 1)) : ℤ) =
  HAdd.hAdd (α := ℤ) (↑(Nat.fib n) : ℤ) (↑(Nat.fib (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]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℕ
⊢ fib (-[n+1] + 2) = fib -[n+1] + fib (-[n+1] + 1)
have negSucc : fib (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 2) =
  HPow.hPow (α := ℤ) (-1) (n + 1 + 1) * (↑(Nat.fib (n + 1)) : ℤ) + fib (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 1)
Tactic: rw [negSucc_eq, ← Nat.cast_add_one, fib_neg_natCast]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
Goal:
n : ℕ
⊢ fib (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 2) =
    HPow.hPow (α := ℤ) (-1) (n + 1 + 1) * (↑(Nat.fib (n + 1)) : ℤ) + fib (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 1)
have negSucc : 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 only [Nat.cast_add, Nat.cast_one, neg_add_rev, reduceNeg, add_comm,
      add_assoc, reduceAdd, add_neg_cancel_comm_assoc, fib_neg_natCast]
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (goal)
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)) : ℤ)
have symm : HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(Nat.fib n) : ℤ) +
    HPow.hPow (α := ℤ) (-1) (1 + (n + 1)) * (↑(Nat.fib (n + 1)) : ℤ) =
  fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.Int.Fib.Basic (hypothesis)
Goal:
n : ℕ
hn0 : ¬n = 0
⊢ HPow.hPow (α := ℤ) (-1) (n + 1) * HSub.hSub (α := ℤ) (↑(Nat.fib n) : ℤ) (↑(Nat.fib (n + 1)) : ℤ) =
    fib (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
have this : HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 = -(↑(n - 1) : ℤ)
Tactic: have : -(n : ℤ) + 1 = -((n - 1 : ℕ) : ℤ) := by grind