awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
rw : Eq (α := ℤ) (↑(max a b + 1 - min a b).toNat : ℤ) (↑((b - a).natAbs + 1) : ℤ)
⊢ Eq (α := ℤ) (↑(#(range (max a b + 1 - min a b).toNat)) : ℤ) (↑((b - a).natAbs + 1) : ℤ)
have rw₁ : max a b + 1 - min a b = (↑((b - a).natAbs + 1) : ℤ)
Tactic: rw [card_range,
        Int.toNat_of_nonneg (sub_nonneg_of_le <| le_add_one min_le_max), Int.natCast_add,
        Int.natCast_natAbs, add_comm, add_sub_assoc, max_sub_min_eq_abs, add_comm, Int.ofNat_one]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
rw : Eq (α := ℤ) (↑(max a b + 1 - min a b).toNat : ℤ) (↑((b - a).natAbs + 1) : ℤ)
rw₁ : max a b + 1 - min a b = (↑((b - a).natAbs + 1) : ℤ)
⊢ Eq (α := ℤ) (↑(#(range (max a b + 1 - min a b).toNat)) : ℤ) (↑((b - a).natAbs + 1) : ℤ)
have rw₂ : max a b + 1 - min a b = HAdd.hAdd (α := ℤ) (↑(b - a).natAbs : ℤ) (↑1 : ℤ)
Tactic: rw [card_range,
        Int.toNat_of_nonneg (sub_nonneg_of_le <| le_add_one min_le_max), Int.natCast_add,
        Int.natCast_natAbs, add_comm, add_sub_assoc, max_sub_min_eq_abs, add_comm, Int.ofNat_one]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
rw : Eq (α := ℤ) (↑(max a b + 1 - min a b).toNat : ℤ) (↑((b - a).natAbs + 1) : ℤ)
rw₁ : max a b + 1 - min a b = (↑((b - a).natAbs + 1) : ℤ)
rw₂ : max a b + 1 - min a b = HAdd.hAdd (α := ℤ) (↑(b - a).natAbs : ℤ) (↑1 : ℤ)
⊢ Eq (α := ℤ) (↑(#(range (max a b + 1 - min a b).toNat)) : ℤ) (↑((b - a).natAbs + 1) : ℤ)
have rw₃ : max a b + 1 - min a b = |b - a| + (↑1 : ℤ)
Tactic: rw [card_range,
        Int.toNat_of_nonneg (sub_nonneg_of_le <| le_add_one min_le_max), Int.natCast_add,
        Int.natCast_natAbs, add_comm, add_sub_assoc, max_sub_min_eq_abs, add_comm, Int.ofNat_one]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
rw : Eq (α := ℤ) (↑(max a b + 1 - min a b).toNat : ℤ) (↑((b - a).natAbs + 1) : ℤ)
rw₁ : max a b + 1 - min a b = (↑((b - a).natAbs + 1) : ℤ)
rw₂ : max a b + 1 - min a b = HAdd.hAdd (α := ℤ) (↑(b - a).natAbs : ℤ) (↑1 : ℤ)
rw₃ : max a b + 1 - min a b = |b - a| + (↑1 : ℤ)
⊢ Eq (α := ℤ) (↑(#(range (max a b + 1 - min a b).toNat)) : ℤ) (↑((b - a).natAbs + 1) : ℤ)
have rw₄ : 1 + max a b - min a b = |b - a| + (↑1 : ℤ)
Tactic: rw [card_range,
        Int.toNat_of_nonneg (sub_nonneg_of_le <| le_add_one min_le_max), Int.natCast_add,
        Int.natCast_natAbs, add_comm, add_sub_assoc, max_sub_min_eq_abs, add_comm, Int.ofNat_one]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
rw : Eq (α := ℤ) (↑(max a b + 1 - min a b).toNat : ℤ) (↑((b - a).natAbs + 1) : ℤ)
rw₁ : max a b + 1 - min a b = (↑((b - a).natAbs + 1) : ℤ)
rw₂ : max a b + 1 - min a b = HAdd.hAdd (α := ℤ) (↑(b - a).natAbs : ℤ) (↑1 : ℤ)
rw₃ : max a b + 1 - min a b = |b - a| + (↑1 : ℤ)
rw₄ : 1 + max a b - min a b = |b - a| + (↑1 : ℤ)
⊢ Eq (α := ℤ) (↑(#(range (max a b + 1 - min a b).toNat)) : ℤ) (↑((b - a).natAbs + 1) : ℤ)
have rw₅ : 1 + (max a b - min a b) = |b - a| + (↑1 : ℤ)
Tactic: rw [card_range,
        Int.toNat_of_nonneg (sub_nonneg_of_le <| le_add_one min_le_max), Int.natCast_add,
        Int.natCast_natAbs, add_comm, add_sub_assoc, max_sub_min_eq_abs, add_comm, Int.ofNat_one]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
rw : Eq (α := ℤ) (↑(max a b + 1 - min a b).toNat : ℤ) (↑((b - a).natAbs + 1) : ℤ)
rw₁ : max a b + 1 - min a b = (↑((b - a).natAbs + 1) : ℤ)
rw₂ : max a b + 1 - min a b = HAdd.hAdd (α := ℤ) (↑(b - a).natAbs : ℤ) (↑1 : ℤ)
rw₃ : max a b + 1 - min a b = |b - a| + (↑1 : ℤ)
rw₄ : 1 + max a b - min a b = |b - a| + (↑1 : ℤ)
rw₅ : 1 + (max a b - min a b) = |b - a| + (↑1 : ℤ)
⊢ Eq (α := ℤ) (↑(#(range (max a b + 1 - min a b).toNat)) : ℤ) (↑((b - a).natAbs + 1) : ℤ)
have rw₆ : 1 + |b - a| = |b - a| + (↑1 : ℤ)
Tactic: rw [card_range,
        Int.toNat_of_nonneg (sub_nonneg_of_le <| le_add_one min_le_max), Int.natCast_add,
        Int.natCast_natAbs, add_comm, add_sub_assoc, max_sub_min_eq_abs, add_comm, Int.ofNat_one]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
rw : Eq (α := ℤ) (↑(max a b + 1 - min a b).toNat : ℤ) (↑((b - a).natAbs + 1) : ℤ)
rw₁ : max a b + 1 - min a b = (↑((b - a).natAbs + 1) : ℤ)
rw₂ : max a b + 1 - min a b = HAdd.hAdd (α := ℤ) (↑(b - a).natAbs : ℤ) (↑1 : ℤ)
rw₃ : max a b + 1 - min a b = |b - a| + (↑1 : ℤ)
rw₄ : 1 + max a b - min a b = |b - a| + (↑1 : ℤ)
rw₅ : 1 + (max a b - min a b) = |b - a| + (↑1 : ℤ)
rw₆ : 1 + |b - a| = |b - a| + (↑1 : ℤ)
⊢ Eq (α := ℤ) (↑(#(range (max a b + 1 - min a b).toNat)) : ℤ) (↑((b - a).natAbs + 1) : ℤ)
have rw₇ : |b - a| + 1 = |b - a| + (↑1 : ℤ)
Tactic: rw [card_range,
        Int.toNat_of_nonneg (sub_nonneg_of_le <| le_add_one min_le_max), Int.natCast_add,
        Int.natCast_natAbs, add_comm, add_sub_assoc, max_sub_min_eq_abs, add_comm, Int.ofNat_one]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
rw : Eq (α := ℤ) (↑(max a b + 1 - min a b).toNat : ℤ) (↑((b - a).natAbs + 1) : ℤ)
rw₁ : max a b + 1 - min a b = (↑((b - a).natAbs + 1) : ℤ)
rw₂ : max a b + 1 - min a b = HAdd.hAdd (α := ℤ) (↑(b - a).natAbs : ℤ) (↑1 : ℤ)
rw₃ : max a b + 1 - min a b = |b - a| + (↑1 : ℤ)
rw₄ : 1 + max a b - min a b = |b - a| + (↑1 : ℤ)
rw₅ : 1 + (max a b - min a b) = |b - a| + (↑1 : ℤ)
rw₆ : 1 + |b - a| = |b - a| + (↑1 : ℤ)
rw₇ : |b - a| + 1 = |b - a| + (↑1 : ℤ)
⊢ Eq (α := ℤ) (↑(#(range (max a b + 1 - min a b).toNat)) : ℤ) (↑((b - a).natAbs + 1) : ℤ)
have rw₈ : |b - a| + 1 = |b - a| + 1
Tactic: rw [card_range,
        Int.toNat_of_nonneg (sub_nonneg_of_le <| le_add_one min_le_max), Int.natCast_add,
        Int.natCast_natAbs, add_comm, add_sub_assoc, max_sub_min_eq_abs, add_comm, Int.ofNat_one]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
h : a ≤ b + 1
⊢ (↑(#(Icc a b)) : ℤ) = b + 1 - a
have rw : (↑(b + 1 - a).toNat : ℤ) = b + 1 - a
Tactic: rw [card_Icc, toNat_sub_of_le h]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
h : a ≤ b + 1
rw : (↑(b + 1 - a).toNat : ℤ) = b + 1 - a
⊢ (↑(#(Icc a b)) : ℤ) = b + 1 - a
have rw₁ : b + 1 - a = b + 1 - a
Tactic: rw [card_Icc, toNat_sub_of_le h]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
h : a ≤ b
⊢ (↑(#(Ico a b)) : ℤ) = b - a
have rw : (↑(b - a).toNat : ℤ) = b - a
Tactic: rw [card_Ico, toNat_sub_of_le h]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
h : a ≤ b
rw : (↑(b - a).toNat : ℤ) = b - a
⊢ (↑(#(Ico a b)) : ℤ) = b - a
have rw₁ : b - a = b - a
Tactic: rw [card_Ico, toNat_sub_of_le h]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
h : a ≤ b
⊢ (↑(#(Ioc a b)) : ℤ) = b - a
have rw : (↑(b - a).toNat : ℤ) = b - a
Tactic: rw [card_Ioc, toNat_sub_of_le h]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
h : a ≤ b
rw : (↑(b - a).toNat : ℤ) = b - a
⊢ (↑(#(Ioc a b)) : ℤ) = b - a
have rw₁ : b - a = b - a
Tactic: rw [card_Ioc, toNat_sub_of_le h]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
h : a < b
⊢ (↑(#(Ioo a b)) : ℤ) = b - a - 1
have rw : (↑(b - a - 1).toNat : ℤ) = b - a - 1
Tactic: rw [card_Ioo, sub_sub, toNat_sub_of_le h]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
h : a < b
rw : (↑(b - a - 1).toNat : ℤ) = b - a - 1
⊢ (↑(#(Ioo a b)) : ℤ) = b - a - 1
have rw₁ : (↑(b - (a + 1)).toNat : ℤ) = b - (a + 1)
Tactic: rw [card_Ioo, sub_sub, toNat_sub_of_le h]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a b : ℤ
h : a < b
rw : (↑(b - a - 1).toNat : ℤ) = b - a - 1
rw₁ : (↑(b - (a + 1)).toNat : ℤ) = b - (a + 1)
⊢ (↑(#(Ioo a b)) : ℤ) = b - a - 1
have rw₂ : b - (a + 1) = b - (a + 1)
Tactic: rw [card_Ioo, sub_sub, toNat_sub_of_le h]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a : ℤ
⊢ Icc a (a + 1) = {a, a + 1}
have h : ∀ (a_1 : ℤ), a_1 ∈ Icc a (a + 1) ↔ Membership.mem (γ := Finset ℤ) {a, a + 1} a_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
a a_1 : ℤ
⊢ a_1 ∈ Icc a (a + 1) ↔ Membership.mem (γ := Finset ℤ) {a, a + 1} a_1
have h : a ≤ a_1 ∧ a_1 ≤ a + 1 ↔ a_1 = a ∨ a_1 = a + 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
⊢ image (fun (x : ℤ) ↦ x % a) (Ico n (n + a)) = Ico 0 a
have inl : ∀ (h : LE.le (α := ℤ) 0 0), Eq (α := Finset ℤ) (image (fun (x : ℤ) ↦ x % 0) (Ico n (n + 0))) (Ico 0 0)
Tactic: obtain rfl | ha := eq_or_lt_of_le h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
inl : ∀ (h : LE.le (α := ℤ) 0 0), Eq (α := Finset ℤ) (image (fun (x : ℤ) ↦ x % 0) (Ico n (n + 0))) (Ico 0 0)
⊢ image (fun (x : ℤ) ↦ x % a) (Ico n (n + a)) = Ico 0 a
have inr : ∀ (ha : 0 < a), image (fun (x : ℤ) ↦ x % a) (Ico n (n + a)) = Ico 0 a
Tactic: obtain rfl | ha := eq_or_lt_of_le h
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
⊢ image (fun (x : ℤ) ↦ x % a) (Ico n (n + a)) = Ico 0 a
have inr : ∀ (i : ℤ), Membership.mem (γ := Finset ℤ) (image (fun (x : ℤ) ↦ x % a) (Ico n (n + a))) i ↔ i ∈ Ico 0 a
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ Membership.mem (γ := Finset ℤ) (image (fun (x : ℤ) ↦ x % a) (Ico n (n + a))) i ↔ i ∈ Ico 0 a
have inr : (∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ 0 ≤ i ∧ i < a
Tactic: simp only [mem_image, mem_Ico]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ (∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ 0 ≤ i ∧ i < a
have inr : (∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → 0 ≤ i ∧ i < a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
inr : (∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → 0 ≤ i ∧ i < a
⊢ (∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ 0 ≤ i ∧ i < a
have inr₁ : 0 ≤ i ∧ i < a → ∃ (a_2 : ℤ), (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.Interval (hypothesis)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
⊢ ∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
have hn : n % a + a * (n / a) = n
Tactic: have hn := Int.emod_add_mul_ediv n a
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
⊢ ∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
have inr : ∀ (hi : i < n % a), ∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
Tactic: obtain hi | hi := lt_or_ge i (n % a)
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
inr : ∀ (hi : i < n % a), ∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
⊢ ∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
have inr₁ : ∀ (hi : n % a ≤ i), ∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
Tactic: obtain hi | hi := lt_or_ge i (n % a)
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ ∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
have inr : n ≤ i + a * (n / a + 1)
Tactic: refine ⟨i + a * (n / a + 1), ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
inr : n ≤ i + a * (n / a + 1)
⊢ ∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
have inr₁ : i + a * (n / a + 1) < n + a
Tactic: refine ⟨i + a * (n / a + 1), ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
inr : n ≤ i + a * (n / a + 1)
inr₁ : i + a * (n / a + 1) < n + a
⊢ ∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
have inr₂ : (i + a * (n / a + 1)) % a = i
Tactic: refine ⟨i + a * (n / a + 1), ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ 0 + n % a + a * (n / a) ≤ i + a + a * (n / a)
have bc : n % a ≤ a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a * (n / a + 1)
have n₁ : n = 0 + n % a + a * (n / a)
Tactic: calc
        n = 0 + n % a + a * (n / a) := by simp [hn]
        _ ≤ i + a + a * (n / a) := by gcongr; exact (Int.emod_lt_of_pos n ha).le
        _ = i + a * (n / a + 1) := by grind
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
n₁ : n = 0 + n % a + a * (n / a)
⊢ n ≤ i + a * (n / a + 1)
have n₂ : 0 + n % a + a * (n / a) ≤ i + a + a * (n / a)
Tactic: calc
        n = 0 + n % a + a * (n / a) := by simp [hn]
        _ ≤ i + a + a * (n / a) := by gcongr; exact (Int.emod_lt_of_pos n ha).le
        _ = i + a * (n / a + 1) := by grind
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
n₁ : n = 0 + n % a + a * (n / a)
n₂ : 0 + n % a + a * (n / a) ≤ i + a + a * (n / a)
⊢ n ≤ i + a * (n / a + 1)
have n₃ : i + a + a * (n / a) = i + a * (n / a + 1)
Tactic: calc
        n = 0 + n % a + a * (n / a) := by simp [hn]
        _ ≤ i + a + a * (n / a) := by gcongr; exact (Int.emod_lt_of_pos n ha).le
        _ = i + a * (n / a + 1) := by grind
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a + a * (n / a + 1) = n + a
have rw : n % a + (a * (n / a) + a * 1) = n + a
Tactic: rw [mul_add, mul_one, ← add_assoc, hn]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
rw : n % a + (a * (n / a) + a * 1) = n + a
⊢ n % a + a * (n / a + 1) = n + a
have rw₁ : n % a + (a * (n / a) + a) = n + a
Tactic: rw [mul_add, mul_one, ← add_assoc, hn]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
rw : n % a + (a * (n / a) + a * 1) = n + a
rw₁ : n % a + (a * (n / a) + a) = n + a
⊢ n % a + a * (n / a + 1) = n + a
have rw₂ : n % a + a * (n / a) + a = n + a
Tactic: rw [mul_add, mul_one, ← add_assoc, hn]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
rw : n % a + (a * (n / a) + a * 1) = n + a
rw₁ : n % a + (a * (n / a) + a) = n + a
rw₂ : n % a + a * (n / a) + a = n + a
⊢ n % a + a * (n / a + 1) = n + a
have rw₃ : n + a = n + a
Tactic: rw [mul_add, mul_one, ← add_assoc, hn]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a
have i₁ : i + a * (n / a + 1) < n % a + a * (n / a + 1)
Tactic: calc
        i + a * (n / a + 1) < n % a + a * (n / a + 1) := by gcongr
        _ = n + a := by rw [mul_add, mul_one, ← add_assoc, hn]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
i₁ : i + a * (n / a + 1) < n % a + a * (n / a + 1)
⊢ i + a * (n / a + 1) < n + a
have i₂ : n % a + a * (n / a + 1) = n + a
Tactic: calc
        i + a * (n / a + 1) < n % a + a * (n / a + 1) := by gcongr
        _ = n + a := by rw [mul_add, mul_one, ← add_assoc, hn]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i
have inr : i % a = i
Tactic: rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hi₀ hia]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
inr : i % a = i
⊢ (i + a * (n / a + 1)) % a = i
have inr₁ : i = i
Tactic: rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hi₀ hia]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ ∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
have inr : n ≤ i + a * (n / a)
Tactic: refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
inr : n ≤ i + a * (n / a)
⊢ ∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
have inr₁ : i + a * (n / a) < n + a
Tactic: refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
inr : n ≤ i + a * (n / a)
inr₁ : i + a * (n / a) < n + a
⊢ ∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
have inr₂ : (i + a * (n / a)) % a = i
Tactic: refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < n + a
have inr : i + a * (n / a) < a + n
Tactic: rw [add_comm n a]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < a + n
have inr : a * (n / a) ≤ n % a + a * (n / a)
Tactic: refine add_lt_add_of_lt_of_le hia (le_trans ?_ hn.le)
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ a * (n / a) ≤ n % a + a * (n / a)
have inr : 0 ≤ n % a
Tactic: simp only [le_add_iff_nonneg_left]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ (i + a * (n / a)) % a = i
have inr : i % a = i
Tactic: rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hi₀ hia]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
inr : i % a = i
⊢ (i + a * (n / a)) % a = i
have inr₁ : i = i
Tactic: rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hi₀ hia]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
m n : ℕ
⊢ Icc (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    Icc (-(↑m : ℤ)) (↑n : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1}
have h : ∀ (a : ℤ),
  a ∈ Icc (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ↔
    Membership.mem (γ := Finset ℤ)
      (Icc (-(↑m : ℤ)) (↑n : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1}) a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
m n : ℕ
a : ℤ
⊢ a ∈ Icc (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ↔
    Membership.mem (γ := Finset ℤ)
      (Icc (-(↑m : ℤ)) (↑n : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1}) a
have h : -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 ≤ a ∧ a ≤ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔
  a = -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 ∨ a = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ∨ -(↑m : ℤ) ≤ a ∧ a ≤ (↑n : ℤ)
Tactic: simp only [mem_Icc, union_insert, union_singleton, mem_insert]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
m n : ℕ
⊢ Ico (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    Ico (-(↑m : ℤ)) (↑n : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1, (↑n : ℤ)}
have h : ∀ (a : ℤ),
  a ∈ Ico (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ↔
    Membership.mem (γ := Finset ℤ) (Ico (-(↑m : ℤ)) (↑n : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1, (↑n : ℤ)}) a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
m n : ℕ
a : ℤ
⊢ a ∈ Ico (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ↔
    Membership.mem (γ := Finset ℤ) (Ico (-(↑m : ℤ)) (↑n : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1, (↑n : ℤ)}) a
have h : -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 ≤ a ∧ a < HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔
  a = -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 ∨ a = (↑n : ℤ) ∨ -(↑m : ℤ) ≤ a ∧ a < (↑n : ℤ)
Tactic: simp only [mem_Ico, union_insert, union_singleton, mem_insert]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
m n : ℕ
⊢ Ioc (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    Ioc (-(↑m : ℤ)) (↑n : ℤ) ∪ {-(↑m : ℤ), HAdd.hAdd (α := ℤ) (↑n : ℤ) 1}
have h : ∀ (a : ℤ),
  a ∈ Ioc (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ↔
    Membership.mem (γ := Finset ℤ) (Ioc (-(↑m : ℤ)) (↑n : ℤ) ∪ {-(↑m : ℤ), HAdd.hAdd (α := ℤ) (↑n : ℤ) 1}) a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
m n : ℕ
a : ℤ
⊢ a ∈ Ioc (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ↔
    Membership.mem (γ := Finset ℤ) (Ioc (-(↑m : ℤ)) (↑n : ℤ) ∪ {-(↑m : ℤ), HAdd.hAdd (α := ℤ) (↑n : ℤ) 1}) a
have h : -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 < a ∧ a ≤ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔
  a = -(↑m : ℤ) ∨ a = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ∨ -(↑m : ℤ) < a ∧ a ≤ (↑n : ℤ)
Tactic: simp only [mem_Ioc, union_insert, union_singleton, mem_insert]
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
m n : ℕ
⊢ Ioo (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    Ioo (-(↑m : ℤ)) (↑n : ℤ) ∪ {-(↑m : ℤ), (↑n : ℤ)}
have h : ∀ (a : ℤ),
  a ∈ Ioo (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ↔
    Membership.mem (γ := Finset ℤ) (Ioo (-(↑m : ℤ)) (↑n : ℤ) ∪ {-(↑m : ℤ), (↑n : ℤ)}) a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Int.Interval (goal)
Goal:
m n : ℕ
a : ℤ
⊢ a ∈ Ioo (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ↔
    Membership.mem (γ := Finset ℤ) (Ioo (-(↑m : ℤ)) (↑n : ℤ) ∪ {-(↑m : ℤ), (↑n : ℤ)}) a
have h : -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 < a ∧ a < HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 ↔
  a = -(↑m : ℤ) ∨ a = (↑n : ℤ) ∨ -(↑m : ℤ) < a ∧ a < (↑n : ℤ)
Tactic: simp only [mem_Ioo, union_insert, union_singleton, mem_insert]
-- Lean 4 proof step from Mathlib.Data.Int.LeastGreatest (goal)
Goal:
P : ℤ → Prop
inst : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ (z : ℤ), P z
EX : ∃ (n : ℕ), P (b + (↑n : ℤ))
z : ℤ
h : P z
⊢ b + (↑(Nat.find (p := fun (n : ℕ) ↦ P (b + (↑n : ℤ))) EX) : ℤ) ≤ z
have obtain : ∀ (n : ℕ) (h : P (b + (↑n : ℤ))), b + (↑(Nat.find (p := fun (n : ℕ) ↦ P (b + (↑n : ℤ))) EX) : ℤ) ≤ b + (↑n : ℤ)
Tactic: obtain ⟨n, rfl⟩ := le.dest (Hb _ h)
Cleared hypotheses: z, h
-- Lean 4 proof step from Mathlib.Data.Int.LeastGreatest (goal)
Goal:
P : ℤ → Prop
inst : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ (z : ℤ), P z
EX : ∃ (n : ℕ), P (b + (↑n : ℤ))
n : ℕ
h : P (b + (↑n : ℤ))
⊢ b + (↑(Nat.find (p := fun (n : ℕ) ↦ P (b + (↑n : ℤ))) EX) : ℤ) ≤ b + (↑n : ℤ)
have grw : b + (↑n : ℤ) ≤ b + (↑n : ℤ)
Tactic: grw [Nat.find_min' EX h]
-- Lean 4 proof step from Mathlib.Data.Int.LeastGreatest (goal)
Goal:
P : ℤ → Prop
Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ (z : ℤ), P z
⊢ ∃ (lb : ℤ), P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
have let : ∀ (b : ℤ) (Hb : ∀ (z : ℤ), P z → b ≤ z), ∃ (lb : ℤ), P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
Tactic: let ⟨b, Hb⟩ := Hbdd
-- Lean 4 proof step from Mathlib.Data.Int.LeastGreatest (goal)
Goal:
P : ℤ → Prop
Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ (z : ℤ), P z
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
⊢ ∃ (lb : ℤ), P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
have let : ∀ (lb : ℤ) (H : P lb ∧ ∀ (z : ℤ), P z → lb ≤ z), ∃ (lb : ℤ), P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
Tactic: let ⟨lb, H⟩ := leastOfBdd b Hb Hinh