awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.Init
Goal:
m n : ℕ
h : n.succ ≤ m
rw : ofNat m + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = ofNat (m - n.succ)
rw₁ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = ofNat (m - n.succ)
rw₂ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = (↑(m - n.succ) : ℤ)
rw₃ : (↑m : ℤ) + -HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) = (↑(m - n.succ) : ℤ)
rw₄ : HAdd.hAdd (α := ℤ) (↑m : ℤ) (-(↑(n + 1) : ℤ)) = (↑(m - n.succ) : ℤ)
rw₅ : HSub.hSub (α := ℤ) (↑m : ℤ) (↑(n + 1) : ℤ) = (↑(m - n.succ) : ℤ)
rw₆ rw₇ : Eq (α := ℤ) (↑(m - n.succ) : ℤ) (↑(m - n.succ) : ℤ)
⊢ ofNat m + -[n+1] = ofNat (m - n.succ)

Tactic:
rw [negSucc_eq, ofNat_eq_natCast, ofNat_eq_natCast, ← Int.natCast_one, ← Int.natCast_add,
    ← Int.sub_eq_add_neg, ← Int.natCast_sub h]

Premises used: Int.natCast_add, Int.ofNat_eq_natCast, Int.sub_eq_add_neg, Int.natCast_sub, Int.natCast_one, Int.negSucc_eq
-- Module: Mathlib.Data.Int.Init
Goal:
a b : ℤ
ha : 0 < a
hab : a ∣ b
⊢ a ≤ b ↔ 0 < b

Tactic:
⟨Int.lt_of_lt_of_le ha, (Int.le_of_dvd · hab)⟩

Premises used: Int.le_of_dvd, Int.lt_of_lt_of_le, Iff.intro
-- Module: Mathlib.Data.Int.Init
Goal:
a b c : ℤ
ha : 0 < a
hab : a ∣ c - b
rw : a ≤ c - b ↔ b < c
rw₁ : a ≤ c - b ↔ 0 < c - b
rw₂ rw₃ : 0 < c - b ↔ 0 < c - b
⊢ a + b ≤ c ↔ b < c

Tactic:
rw [Int.add_le_iff_le_sub, ← Int.sub_pos, le_iff_pos_of_dvd ha hab]

Premises used: Int.add_le_iff_le_sub, Int.sub_pos, Int.le_iff_pos_of_dvd
-- Module: Mathlib.Data.Int.Init
Goal:
⊢ ∀ {m n : ℤ}, m.sign = n.sign → (m + n).sign = n.sign

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
i : ℤ
h : 0 < i
⊢ (↑(i.toNat - 1) : ℤ) = i - 1

Tactic:
simp only [lt_toNat, Int.cast_ofNat_Int, h, natCast_pred_of_pos, Int.le_of_lt h, toNat_of_nonneg]

Premises used: Int.toNat_of_nonneg, Int.cast_ofNat_Int, Int.natCast_pred_of_pos, Int.lt_toNat, Int.le_of_lt
-- Module: Mathlib.Data.Int.Init
Goal:
m : ℤ
n : ℕ
hn : n ≠ 0
⊢ m.toNat < n ↔ m < (↑n : ℤ)

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
m : ℤ
n : ℕ
hn : n ≠ 0
⊢ LT.lt (α := ℤ) 0 (↑n : ℤ)

Tactic:
lia
-- Module: Mathlib.Data.Int.Init
Goal:
m : ℤ
n : ℕ
⊢ m.pow n = m ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Int.Init
Goal:
m n : ℕ
⊢ gcd (↑m : ℤ) -[n+1] = m.gcd (n + 1)

Tactic:
simp [gcd]

Premises used: Int.gcd
-- Module: Mathlib.Data.Int.Init
Goal:
m n : ℕ
⊢ -[m+1].gcd (↑n : ℤ) = (m + 1).gcd n

Tactic:
simp [gcd]

Premises used: Int.gcd
-- Module: Mathlib.Data.Int.Init
Goal:
m n : ℕ
⊢ -[m+1].gcd -[n+1] = (m + 1).gcd (n + 1)

Tactic:
simp [gcd]

Premises used: Int.gcd
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
simp_rw : (∃ a_1 < (b + 1 - a).toNat, a + (↑a_1 : ℤ) = x) ↔ a ≤ x ∧ x ≤ b
⊢ x ∈ map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding a)) (range (b + 1 - a).toNat) ↔ a ≤ x ∧ x ≤ b

Tactic:
simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
      addLeftEmbedding_apply]

Premises used: addLeftEmbedding_apply, Function.Embedding.trans_apply, Nat.castEmbedding_apply, Finset.mem_range, Finset.mem_map
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
mp : (∃ a_1 < (b + 1 - a).toNat, a + (↑a_1 : ℤ) = x) → a ≤ x ∧ x ≤ b
mpr : a ≤ x ∧ x ≤ b → ∃ a_2 < (b + 1 - a).toNat, a + (↑a_2 : ℤ) = x
⊢ (∃ a_1 < (b + 1 - a).toNat, a + (↑a_1 : ℤ) = x) ↔ a ≤ x ∧ x ≤ b

Tactic:
constructor
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
⊢ (∃ a_1 < (b + 1 - a).toNat, a + (↑a_1 : ℤ) = x) → a ≤ x ∧ x ≤ b

Tactic:
lia
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
h_1 : a ≤ x ∧ x ≤ b
h : (x - a).toNat < (b + 1 - a).toNat ∧ a + (↑(x - a).toNat : ℤ) = x
⊢ ∃ a_1 < (b + 1 - a).toNat, a + (↑a_1 : ℤ) = x

Tactic:
use (x - a).toNat

Premises used: HSub.hSub, Int.toNat
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
h : a ≤ x ∧ x ≤ b
⊢ (x - a).toNat < (b + 1 - a).toNat ∧ a + (↑(x - a).toNat : ℤ) = x

Tactic:
omega
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
simp_rw : (∃ a_1 < (b - a).toNat, a + (↑a_1 : ℤ) = x) ↔ a ≤ x ∧ x < b
⊢ x ∈ map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding a)) (range (b - a).toNat) ↔ a ≤ x ∧ x < b

Tactic:
simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
      addLeftEmbedding_apply]

Premises used: addLeftEmbedding_apply, Function.Embedding.trans_apply, Nat.castEmbedding_apply, Finset.mem_range, Finset.mem_map
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
mp : (∃ a_1 < (b - a).toNat, a + (↑a_1 : ℤ) = x) → a ≤ x ∧ x < b
mpr : a ≤ x ∧ x < b → ∃ a_2 < (b - a).toNat, a + (↑a_2 : ℤ) = x
⊢ (∃ a_1 < (b - a).toNat, a + (↑a_1 : ℤ) = x) ↔ a ≤ x ∧ x < b

Tactic:
constructor
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + (↑a_1 : ℤ) = x) → a ≤ x ∧ x < b

Tactic:
lia
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
h_1 : a ≤ x ∧ x < b
h : (x - a).toNat < (b - a).toNat ∧ a + (↑(x - a).toNat : ℤ) = x
⊢ ∃ a_1 < (b - a).toNat, a + (↑a_1 : ℤ) = x

Tactic:
use (x - a).toNat

Premises used: HSub.hSub, Int.toNat
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
h : a ≤ x ∧ x < b
⊢ (x - a).toNat < (b - a).toNat ∧ a + (↑(x - a).toNat : ℤ) = x

Tactic:
omega
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
simp_rw : (∃ a_1 < (b - a).toNat, a + 1 + (↑a_1 : ℤ) = x) ↔ a < x ∧ x ≤ b
⊢ x ∈ map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (a + 1))) (range (b - a).toNat) ↔ a < x ∧ x ≤ b

Tactic:
simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
      addLeftEmbedding_apply]

Premises used: addLeftEmbedding_apply, Function.Embedding.trans_apply, Nat.castEmbedding_apply, Finset.mem_range, Finset.mem_map
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
mp : (∃ a_1 < (b - a).toNat, a + 1 + (↑a_1 : ℤ) = x) → a < x ∧ x ≤ b
mpr : a < x ∧ x ≤ b → ∃ a_2 < (b - a).toNat, a + 1 + (↑a_2 : ℤ) = x
⊢ (∃ a_1 < (b - a).toNat, a + 1 + (↑a_1 : ℤ) = x) ↔ a < x ∧ x ≤ b

Tactic:
constructor
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + 1 + (↑a_1 : ℤ) = x) → a < x ∧ x ≤ b

Tactic:
lia
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
h_1 : a < x ∧ x ≤ b
h : (x - (a + 1)).toNat < (b - a).toNat ∧ a + 1 + (↑(x - (a + 1)).toNat : ℤ) = x
⊢ ∃ a_1 < (b - a).toNat, a + 1 + (↑a_1 : ℤ) = x

Tactic:
use (x - (a + 1)).toNat

Premises used: HSub.hSub, HAdd.hAdd, Int.toNat, OfNat.ofNat
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
h : a < x ∧ x ≤ b
⊢ (x - (a + 1)).toNat < (b - a).toNat ∧ a + 1 + (↑(x - (a + 1)).toNat : ℤ) = x

Tactic:
omega
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
simp_rw : (∃ a_1 < (b - a - 1).toNat, a + 1 + (↑a_1 : ℤ) = x) ↔ a < x ∧ x < b
⊢ x ∈ map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (a + 1))) (range (b - a - 1).toNat) ↔
    a < x ∧ x < b

Tactic:
simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
      addLeftEmbedding_apply]

Premises used: addLeftEmbedding_apply, Function.Embedding.trans_apply, Nat.castEmbedding_apply, Finset.mem_range, Finset.mem_map
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
mp : (∃ a_1 < (b - a - 1).toNat, a + 1 + (↑a_1 : ℤ) = x) → a < x ∧ x < b
mpr : a < x ∧ x < b → ∃ a_2 < (b - a - 1).toNat, a + 1 + (↑a_2 : ℤ) = x
⊢ (∃ a_1 < (b - a - 1).toNat, a + 1 + (↑a_1 : ℤ) = x) ↔ a < x ∧ x < b

Tactic:
constructor
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
⊢ (∃ a_1 < (b - a - 1).toNat, a + 1 + (↑a_1 : ℤ) = x) → a < x ∧ x < b

Tactic:
lia
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
h_1 : a < x ∧ x < b
h : (x - (a + 1)).toNat < (b - a - 1).toNat ∧ a + 1 + (↑(x - (a + 1)).toNat : ℤ) = x
⊢ ∃ a_1 < (b - a - 1).toNat, a + 1 + (↑a_1 : ℤ) = x

Tactic:
use (x - (a + 1)).toNat

Premises used: HSub.hSub, HAdd.hAdd, Int.toNat, OfNat.ofNat
-- Module: Mathlib.Data.Int.Interval
Goal:
a b x : ℤ
h : a < x ∧ x < b
⊢ (x - (a + 1)).toNat < (b - a - 1).toNat ∧ a + 1 + (↑(x - (a + 1)).toNat : ℤ) = x

Tactic:
lia
-- Module: Mathlib.Data.Int.Interval
Goal:
a b : ℤ
⊢ Icc a b = map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding a)) (range (b + 1 - a).toNat)

Tactic:
rfl

Premises used: Finset.map, Finset.Icc, rfl
-- Module: Mathlib.Data.Int.Interval
Goal:
a b : ℤ
⊢ Ico a b = map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding a)) (range (b - a).toNat)

Tactic:
rfl

Premises used: Finset.map, Finset.Ico, rfl
-- Module: Mathlib.Data.Int.Interval
Goal:
a b : ℤ
⊢ Ioc a b = map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (a + 1))) (range (b - a).toNat)

Tactic:
rfl

Premises used: Finset.map, rfl, Finset.Ioc
-- Module: Mathlib.Data.Int.Interval
Goal:
a b : ℤ
⊢ Ioo a b = map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (a + 1))) (range (b - a - 1).toNat)

Tactic:
rfl

Premises used: Finset.map, Finset.Ioo, rfl
-- Module: Mathlib.Data.Int.Interval
Goal:
a b : ℤ
⊢ uIcc a b =
    map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (min a b))) (range (max a b + 1 - min a b).toNat)

Tactic:
rfl

Premises used: Finset.map, Finset.Icc, rfl, Finset.uIcc
-- Module: Mathlib.Data.Int.Interval
Goal:
a b : ℤ
⊢ #(Icc a b) = (b + 1 - a).toNat

Tactic:
(card_map _).trans <| card_range _

Premises used: Finset.card_map, Finset.card_range, Finset.map, Finset.Icc, Eq.trans
-- Module: Mathlib.Data.Int.Interval
Goal:
a b : ℤ
⊢ #(Ico a b) = (b - a).toNat

Tactic:
(card_map _).trans <| card_range _

Premises used: Finset.card_map, Finset.card_range, Finset.map, Finset.Ico, Eq.trans
-- Module: Mathlib.Data.Int.Interval
Goal:
a b : ℤ
⊢ #(Ioc a b) = (b - a).toNat

Tactic:
(card_map _).trans <| card_range _

Premises used: Finset.card_map, Finset.card_range, Finset.map, Eq.trans, Finset.Ioc
-- Module: Mathlib.Data.Int.Interval
Goal:
a b : ℤ
⊢ #(Ioo a b) = (b - a - 1).toNat

Tactic:
(card_map _).trans <| card_range _

Premises used: Finset.card_map, Finset.card_range, Finset.map, Finset.Ioo, Eq.trans
-- Module: Mathlib.Data.Int.Interval
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 : ℤ)
rw₈ rw₉ : |b - a| + 1 = |b - a| + 1
⊢ Eq (α := ℤ) (↑(#(range (max a b + 1 - min a b).toNat)) : ℤ) (↑((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]

Premises used: add_sub_assoc, Int.natCast_add, Int.toNat_of_nonneg, min_le_max, sub_nonneg_of_le, Finset.card_range, Int.le_add_one, max_sub_min_eq_abs, add_comm, Int.ofNat_one, Int.natCast_natAbs
-- Module: Mathlib.Data.Int.Interval
Goal:
a b : ℤ
h : a ≤ b + 1
rw : (↑(b + 1 - a).toNat : ℤ) = b + 1 - a
rw₁ rw₂ : b + 1 - a = b + 1 - a
⊢ (↑(#(Icc a b)) : ℤ) = b + 1 - a

Tactic:
rw [card_Icc, toNat_sub_of_le h]

Premises used: Int.toNat_sub_of_le, Int.card_Icc
-- Module: Mathlib.Data.Int.Interval
Goal:
a b : ℤ
h : a ≤ b
rw : (↑(b - a).toNat : ℤ) = b - a
rw₁ rw₂ : b - a = b - a
⊢ (↑(#(Ico a b)) : ℤ) = b - a

Tactic:
rw [card_Ico, toNat_sub_of_le h]

Premises used: Int.toNat_sub_of_le, Int.card_Ico
-- Module: Mathlib.Data.Int.Interval
Goal:
a b : ℤ
h : a ≤ b
rw : (↑(b - a).toNat : ℤ) = b - a
rw₁ rw₂ : b - a = b - a
⊢ (↑(#(Ioc a b)) : ℤ) = b - a

Tactic:
rw [card_Ioc, toNat_sub_of_le h]

Premises used: Int.toNat_sub_of_le, Int.card_Ioc
-- Module: Mathlib.Data.Int.Interval
Goal:
a b : ℤ
h : a < b
rw : (↑(b - a - 1).toNat : ℤ) = b - a - 1
rw₁ : (↑(b - (a + 1)).toNat : ℤ) = b - (a + 1)
rw₂ rw₃ : b - (a + 1) = b - (a + 1)
⊢ (↑(#(Ioo a b)) : ℤ) = b - a - 1

Tactic:
rw [card_Ioo, sub_sub, toNat_sub_of_le h]

Premises used: Int.card_Ioo, Int.toNat_sub_of_le, sub_sub
-- Module: Mathlib.Data.Int.Interval
Goal:
a : ℤ
h : ∀ (a_1 : ℤ), a_1 ∈ Icc a (a + 1) ↔ Membership.mem (γ := Finset ℤ) {a, a + 1} a_1
⊢ Icc a (a + 1) = {a, a + 1}

Tactic:
ext
-- Module: Mathlib.Data.Int.Interval
Goal:
a a_1 : ℤ
h : a ≤ a_1 ∧ a_1 ≤ a + 1 ↔ a_1 = a ∨ a_1 = a + 1
⊢ a_1 ∈ Icc a (a + 1) ↔ Membership.mem (γ := Finset ℤ) {a, a + 1} a_1

Tactic:
simp
-- Module: Mathlib.Data.Int.Interval
Goal:
a a_1 : ℤ
⊢ a ≤ a_1 ∧ a_1 ≤ a + 1 ↔ a_1 = a ∨ a_1 = a + 1

Tactic:
omega
-- Module: Mathlib.Data.Int.Interval
Goal:
a b : ℤ
h : a ≤ b + 1
⊢ (↑(Fintype.card (↑(Set.Icc a b) : Type)) : ℤ) = b + 1 - a

Tactic:
simp [h]
-- Module: Mathlib.Data.Int.Interval
Goal:
a b : ℤ
h : a ≤ b
⊢ (↑(Fintype.card (↑(Set.Ico a b) : Type)) : ℤ) = b - a

Tactic:
simp [h]
-- Module: Mathlib.Data.Int.Interval
Goal:
a b : ℤ
h : a ≤ b
⊢ (↑(Fintype.card (↑(Set.Ioc a b) : Type)) : ℤ) = b - a

Tactic:
simp [h]
-- Module: Mathlib.Data.Int.Interval
Goal:
a b : ℤ
h : a < b
⊢ (↑(Fintype.card (↑(Set.Ioo a b) : Type)) : ℤ) = b - a - 1

Tactic:
simp [h]
-- Module: Mathlib.Data.Int.Interval
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)
inr : ∀ (ha : 0 < a), image (fun (x : ℤ) ↦ x % a) (Ico n (n + a)) = Ico 0 a
⊢ image (fun (x : ℤ) ↦ x % a) (Ico n (n + a)) = Ico 0 a

Tactic:
obtain rfl | ha := eq_or_lt_of_le h

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Data.Int.Interval
Goal:
n : ℤ
h : LE.le (α := ℤ) 0 0
⊢ Eq (α := Finset ℤ) (image (fun (x : ℤ) ↦ x % 0) (Ico n (n + 0))) (Ico 0 0)

Tactic:
simp
-- Module: Mathlib.Data.Int.Interval
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
inr : ∀ (i : ℤ), Membership.mem (γ := Finset ℤ) (image (fun (x : ℤ) ↦ x % a) (Ico n (n + a))) i ↔ i ∈ Ico 0 a
⊢ image (fun (x : ℤ) ↦ x % a) (Ico n (n + a)) = Ico 0 a

Tactic:
ext i
-- Module: Mathlib.Data.Int.Interval
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
⊢ Membership.mem (γ := Finset ℤ) (image (fun (x : ℤ) ↦ x % a) (Ico n (n + a))) i ↔ i ∈ Ico 0 a

Tactic:
simp only [mem_image, mem_Ico]

Premises used: Finset.mem_image, Finset.mem_Ico
-- Module: Mathlib.Data.Int.Interval
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
inr₁ : 0 ≤ i ∧ i < a → ∃ (a_2 : ℤ), (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i
⊢ (∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ 0 ≤ i ∧ i < a

Tactic:
constructor
-- Module: Mathlib.Data.Int.Interval
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
left : n ≤ i ∧ i < n + a
⊢ 0 ≤ i % a ∧ i % a < a

Tactic:
⟨emod_nonneg i ha.ne', emod_lt_of_pos i ha⟩

Premises used: LT.lt.ne', And.intro, Int.emod_lt_of_pos, Int.emod_nonneg
-- Module: Mathlib.Data.Int.Interval
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
left : n ≤ i ∧ i < n + a
⊢ 0 ≤ i % a ∧ i % a < a

Tactic:
exact ⟨emod_nonneg i ha.ne', emod_lt_of_pos i ha⟩
-- Module: Mathlib.Data.Int.Interval
Goal:
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
⊢ n % a + a * (n / a) = n

Tactic:
have hn := Int.emod_add_mul_ediv n a
-- Module: Mathlib.Data.Int.Interval
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
inr₁ : ∀ (hi : n % a ≤ i), ∃ (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

Tactic:
obtain hi | hi := lt_or_ge i (n % a)

Premises used: HMod.hMod, lt_or_ge
-- Module: Mathlib.Data.Int.Interval
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

Tactic:
⟨i + a * (n / a + 1), ⟨?_, ?_⟩, ?_⟩

Premises used: HMul.hMul, HDiv.hDiv, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Data.Int.Interval
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
inr₂ : (i + a * (n / a + 1)) % a = i
⊢ ∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
refine ⟨i + a * (n / a + 1), ⟨?_, ?_⟩, ?_⟩
-- Module: Mathlib.Data.Int.Interval
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 = 0 + n % a + a * (n / a)

Tactic:
simp [hn]
-- Module: Mathlib.Data.Int.Interval
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
bc : n % a ≤ a
⊢ 0 + n % a + a * (n / a) ≤ i + a + a * (n / a)

Tactic:
gcongr
-- Module: Mathlib.Data.Int.Interval
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

Tactic:
(Int.emod_lt_of_pos n ha).le

Premises used: LT.lt.le, Int.emod_lt_of_pos
-- Module: Mathlib.Data.Int.Interval
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

Tactic:
exact (Int.emod_lt_of_pos n ha).le

Premises used: LT.lt.le, Int.emod_lt_of_pos
-- Module: Mathlib.Data.Int.Interval
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 + a * (n / a) = i + a * (n / a + 1)

Tactic:
grind
-- Module: Mathlib.Data.Int.Interval
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 + a * (n / a) = i + a * (n / a + 1)
⊢ n ≤ 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

Premises used: HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Int.Interval
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 + a * (n / a + 1)

Tactic:
gcongr
-- Module: Mathlib.Data.Int.Interval
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
rw₃ rw₄ : n + a = n + a
⊢ n % a + a * (n / a + 1) = n + a

Tactic:
rw [mul_add, mul_one, ← add_assoc, hn]

Premises used: add_assoc, mul_add, mul_one
-- Module: Mathlib.Data.Int.Interval
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₂ : n % a + a * (n / a + 1) = n + a
⊢ i + 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]

Premises used: HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Int.Interval
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
inr₁ inr₂ : i = i
⊢ (i + a * (n / a + 1)) % a = i

Tactic:
rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hi₀ hia]

Premises used: Int.emod_eq_of_lt, Int.add_mul_emod_self_left
-- Module: Mathlib.Data.Int.Interval
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

Tactic:
⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩

Premises used: HMul.hMul, HDiv.hDiv, HAdd.hAdd, And.intro, Exists.intro
-- Module: Mathlib.Data.Int.Interval
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
inr₂ : (i + a * (n / a)) % a = i
⊢ ∃ (a_1 : ℤ), (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩
-- Module: Mathlib.Data.Int.Interval
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
⊢ n ≤ i + a * (n / a)

Tactic:
hn.symm.le.trans (add_le_add_left hi _)

Premises used: Eq.le, add_le_add_left, LE.le.trans, Eq.symm
-- Module: Mathlib.Data.Int.Interval
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
⊢ n ≤ i + a * (n / a)

Tactic:
exact hn.symm.le.trans (add_le_add_left hi _)

Premises used: Eq.le, add_le_add_left, LE.le.trans, Eq.symm
-- Module: Mathlib.Data.Int.Interval
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 * (n / a) < a + n
⊢ i + a * (n / a) < n + a

Tactic:
rw [add_comm n a]

Premises used: add_comm
-- Module: Mathlib.Data.Int.Interval
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

Tactic:
add_lt_add_of_lt_of_le hia (le_trans ?_ hn.le)

Premises used: Eq.le, add_lt_add_of_lt_of_le, le_trans
-- Module: Mathlib.Data.Int.Interval
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 : a * (n / a) ≤ n % a + a * (n / a)
⊢ i + a * (n / a) < a + n

Tactic:
refine add_lt_add_of_lt_of_le hia (le_trans ?_ hn.le)

Premises used: Eq.le, add_lt_add_of_lt_of_le, le_trans
-- Module: Mathlib.Data.Int.Interval
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 : 0 ≤ n % a
⊢ a * (n / a) ≤ n % a + a * (n / a)

Tactic:
simp only [le_add_iff_nonneg_left]

Premises used: le_add_iff_nonneg_left
-- Module: Mathlib.Data.Int.Interval
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
⊢ 0 ≤ n % a

Tactic:
Int.emod_nonneg n (ne_of_gt ha)

Premises used: ne_of_gt, Int.emod_nonneg
-- Module: Mathlib.Data.Int.Interval
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
⊢ 0 ≤ n % a

Tactic:
exact Int.emod_nonneg n (ne_of_gt ha)

Premises used: ne_of_gt, Int.emod_nonneg
-- Module: Mathlib.Data.Int.Interval
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
inr₁ inr₂ : i = i
⊢ (i + a * (n / a)) % a = i

Tactic:
rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hi₀ hia]

Premises used: Int.emod_eq_of_lt, Int.add_mul_emod_self_left
-- Module: Mathlib.Data.Int.Interval
Goal:
m n : ℕ
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
⊢ Icc (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    Icc (-(↑m : ℤ)) (↑n : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1}

Tactic:
ext
-- Module: Mathlib.Data.Int.Interval
Goal:
m n : ℕ
a : ℤ
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 : ℤ)
⊢ 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:
simp only [mem_Icc, union_insert, union_singleton, mem_insert]

Premises used: Finset.mem_Icc, Finset.mem_insert, Finset.union_insert, Finset.union_singleton
-- Module: Mathlib.Data.Int.Interval
Goal:
m n : ℕ
a : ℤ
⊢ -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:
omega
-- Module: Mathlib.Data.Int.Interval
Goal:
m n : ℕ
h :
  ∀ (a : ℤ),
    a ∈ Ico (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ↔
      Membership.mem (γ := Finset ℤ) (Ico (-(↑m : ℤ)) (↑n : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1, (↑n : ℤ)}) a
⊢ Ico (-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    Ico (-(↑m : ℤ)) (↑n : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑m : ℤ) 1, (↑n : ℤ)}

Tactic:
ext