awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n_1 k i n : ℕ
simp_rw : (↑m : ℤ) <<< (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
⊢ (↑m : ℤ) <<< -[i+1] = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
have simp_rw₁ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
  (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
Tactic: simp_rw [negSucc_eq, shiftLeft_neg, Nat.shiftLeft'_false, Nat.shiftRight_add,
          ← Nat.shiftLeft_sub _ le_rfl, Nat.sub_self, Nat.shiftLeft_zero, ← shiftRight_natCast,
          ← shiftRight_add', Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n_1 k i n : ℕ
simp_rw : (↑m : ℤ) <<< (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
simp_rw₁ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
⊢ (↑m : ℤ) <<< -[i+1] = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
have simp_rw₂ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(m <<< n >>> (n + i + 1)) : ℤ)
Tactic: simp_rw [negSucc_eq, shiftLeft_neg, Nat.shiftLeft'_false, Nat.shiftRight_add,
          ← Nat.shiftLeft_sub _ le_rfl, Nat.sub_self, Nat.shiftLeft_zero, ← shiftRight_natCast,
          ← shiftRight_add', Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n_1 k i n : ℕ
simp_rw : (↑m : ℤ) <<< (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
simp_rw₁ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
simp_rw₂ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(m <<< n >>> (n + i + 1)) : ℤ)
⊢ (↑m : ℤ) <<< -[i+1] = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
have simp_rw₃ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
  (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< n >>> n >>> i) 1) : ℤ)
Tactic: simp_rw [negSucc_eq, shiftLeft_neg, Nat.shiftLeft'_false, Nat.shiftRight_add,
          ← Nat.shiftLeft_sub _ le_rfl, Nat.sub_self, Nat.shiftLeft_zero, ← shiftRight_natCast,
          ← shiftRight_add', Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n_1 k i n : ℕ
simp_rw : (↑m : ℤ) <<< (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
simp_rw₁ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
simp_rw₂ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(m <<< n >>> (n + i + 1)) : ℤ)
simp_rw₃ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< n >>> n >>> i) 1) : ℤ)
⊢ (↑m : ℤ) <<< -[i+1] = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
have simp_rw₄ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
  (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< (n - n) >>> i) 1) : ℤ)
Tactic: simp_rw [negSucc_eq, shiftLeft_neg, Nat.shiftLeft'_false, Nat.shiftRight_add,
          ← Nat.shiftLeft_sub _ le_rfl, Nat.sub_self, Nat.shiftLeft_zero, ← shiftRight_natCast,
          ← shiftRight_add', Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n_1 k i n : ℕ
simp_rw : (↑m : ℤ) <<< (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
simp_rw₁ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
simp_rw₂ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(m <<< n >>> (n + i + 1)) : ℤ)
simp_rw₃ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< n >>> n >>> i) 1) : ℤ)
simp_rw₄ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< (n - n) >>> i) 1) : ℤ)
⊢ (↑m : ℤ) <<< -[i+1] = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
have simp_rw₅ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
  (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< 0 >>> i) 1) : ℤ)
Tactic: simp_rw [negSucc_eq, shiftLeft_neg, Nat.shiftLeft'_false, Nat.shiftRight_add,
          ← Nat.shiftLeft_sub _ le_rfl, Nat.sub_self, Nat.shiftLeft_zero, ← shiftRight_natCast,
          ← shiftRight_add', Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n_1 k i n : ℕ
simp_rw : (↑m : ℤ) <<< (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
simp_rw₁ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
simp_rw₂ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(m <<< n >>> (n + i + 1)) : ℤ)
simp_rw₃ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< n >>> n >>> i) 1) : ℤ)
simp_rw₄ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< (n - n) >>> i) 1) : ℤ)
simp_rw₅ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< 0 >>> i) 1) : ℤ)
⊢ (↑m : ℤ) <<< -[i+1] = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
have simp_rw₆ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
  (↑(HShiftRight.hShiftRight (β := ℕ) (m >>> i) 1) : ℤ)
Tactic: simp_rw [negSucc_eq, shiftLeft_neg, Nat.shiftLeft'_false, Nat.shiftRight_add,
          ← Nat.shiftLeft_sub _ le_rfl, Nat.sub_self, Nat.shiftLeft_zero, ← shiftRight_natCast,
          ← shiftRight_add', Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n_1 k i n : ℕ
simp_rw : (↑m : ℤ) <<< (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
simp_rw₁ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
simp_rw₂ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(m <<< n >>> (n + i + 1)) : ℤ)
simp_rw₃ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< n >>> n >>> i) 1) : ℤ)
simp_rw₄ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< (n - n) >>> i) 1) : ℤ)
simp_rw₅ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< 0 >>> i) 1) : ℤ)
simp_rw₆ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m >>> i) 1) : ℤ)
⊢ (↑m : ℤ) <<< -[i+1] = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
have simp_rw₇ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
  HShiftRight.hShiftRight (β := ℤ) (HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑i : ℤ)) (↑1 : ℤ)
Tactic: simp_rw [negSucc_eq, shiftLeft_neg, Nat.shiftLeft'_false, Nat.shiftRight_add,
          ← Nat.shiftLeft_sub _ le_rfl, Nat.sub_self, Nat.shiftLeft_zero, ← shiftRight_natCast,
          ← shiftRight_add', Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n_1 k i n : ℕ
simp_rw : (↑m : ℤ) <<< (-HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
simp_rw₁ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
simp_rw₂ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) = (↑(m <<< n >>> (n + i + 1)) : ℤ)
simp_rw₃ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< n >>> n >>> i) 1) : ℤ)
simp_rw₄ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< (n - n) >>> i) 1) : ℤ)
simp_rw₅ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m <<< 0 >>> i) 1) : ℤ)
simp_rw₆ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    (↑(HShiftRight.hShiftRight (β := ℕ) (m >>> i) 1) : ℤ)
simp_rw₇ :
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
    HShiftRight.hShiftRight (β := ℤ) (HShiftRight.hShiftRight (α := ℤ) (β := ℤ) (↑m : ℤ) (↑i : ℤ)) (↑1 : ℤ)
⊢ (↑m : ℤ) <<< -[i+1] = (↑(Nat.shiftLeft' false m n >>> (n + i + 1)) : ℤ)
have simp_rw₈ : HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) =
  HShiftRight.hShiftRight (α := ℤ) (↑m : ℤ) (HAdd.hAdd (α := ℤ) (↑i : ℤ) (↑1 : ℤ))
Tactic: simp_rw [negSucc_eq, shiftLeft_neg, Nat.shiftLeft'_false, Nat.shiftRight_add,
          ← Nat.shiftLeft_sub _ le_rfl, Nat.sub_self, Nat.shiftLeft_zero, ← shiftRight_natCast,
          ← shiftRight_add', Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n_1 k i n : ℕ
⊢ Nat.shiftLeft' true m i = Nat.shiftLeft' true m (n + i) >>> n
have a : n ≤ n + i
Tactic: rw [← Nat.shiftLeft'_sub, Nat.add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n_1 k i n : ℕ
⊢ m >>> i.succ = Nat.shiftLeft' true m n >>> (n + i + 1)
have rw : m >>> i.succ = Nat.shiftLeft' true m n >>> (n + (i + 1))
Tactic: rw [add_assoc, Nat.shiftRight_add, ← Nat.shiftLeft'_sub _ _ le_rfl,
          Nat.sub_self, Nat.shiftLeft']
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n_1 k i n : ℕ
rw : m >>> i.succ = Nat.shiftLeft' true m n >>> (n + (i + 1))
⊢ m >>> i.succ = Nat.shiftLeft' true m n >>> (n + i + 1)
have rw₁ : m >>> i.succ = Nat.shiftLeft' true m n >>> n >>> (i + 1)
Tactic: rw [add_assoc, Nat.shiftRight_add, ← Nat.shiftLeft'_sub _ _ le_rfl,
          Nat.sub_self, Nat.shiftLeft']
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n_1 k i n : ℕ
rw : m >>> i.succ = Nat.shiftLeft' true m n >>> (n + (i + 1))
rw₁ : m >>> i.succ = Nat.shiftLeft' true m n >>> n >>> (i + 1)
⊢ m >>> i.succ = Nat.shiftLeft' true m n >>> (n + i + 1)
have rw₂ : m >>> i.succ = Nat.shiftLeft' true m (n - n) >>> (i + 1)
Tactic: rw [add_assoc, Nat.shiftRight_add, ← Nat.shiftLeft'_sub _ _ le_rfl,
          Nat.sub_self, Nat.shiftLeft']
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n_1 k i n : ℕ
rw : m >>> i.succ = Nat.shiftLeft' true m n >>> (n + (i + 1))
rw₁ : m >>> i.succ = Nat.shiftLeft' true m n >>> n >>> (i + 1)
rw₂ : m >>> i.succ = Nat.shiftLeft' true m (n - n) >>> (i + 1)
⊢ m >>> i.succ = Nat.shiftLeft' true m n >>> (n + i + 1)
have rw₃ : m >>> i.succ = Nat.shiftLeft' true m 0 >>> (i + 1)
Tactic: rw [add_assoc, Nat.shiftRight_add, ← Nat.shiftLeft'_sub _ _ le_rfl,
          Nat.sub_self, Nat.shiftLeft']
-- Lean 4 proof step from Mathlib.Data.Int.Bitwise (goal)
Goal:
m n_1 k i n : ℕ
rw : m >>> i.succ = Nat.shiftLeft' true m n >>> (n + (i + 1))
rw₁ : m >>> i.succ = Nat.shiftLeft' true m n >>> n >>> (i + 1)
rw₂ : m >>> i.succ = Nat.shiftLeft' true m (n - n) >>> (i + 1)
rw₃ : m >>> i.succ = Nat.shiftLeft' true m 0 >>> (i + 1)
⊢ m >>> i.succ = Nat.shiftLeft' true m n >>> (n + i + 1)
have rw₄ : m >>> i.succ = m >>> (i + 1)
Tactic: rw [add_assoc, Nat.shiftRight_add, ← Nat.shiftLeft'_sub _ _ le_rfl,
          Nat.sub_self, Nat.shiftLeft']
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℤ
⊢ {x ∈ Ico a b | x ≡ v [ZMOD r]} =
    map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})
have h : ∀ (x : ℤ),
  x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    x ∈ map { toFun := fun (x : ℤ) ↦ x + v, inj' := sorry : ℤ ↪ ℤ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v x : ℤ
⊢ x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    x ∈ map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})
have h : x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
  ∃ a_1 ∈ {x ∈ Ico (a - v) (b - v) | r ∣ x}, ({ toFun := fun (x : ℤ) ↦ x + v, inj' := sorry : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
Tactic: simp_rw [mem_map, mem_filter, mem_Ico, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v x : ℤ
h :
  x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    ∃ a_1 ∈ {x ∈ Ico (a - v) (b - v) | r ∣ x},
      ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
⊢ x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    x ∈ map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})
have h₁ : x ∈ Ico a b ∧ x ≡ v [ZMOD r] ↔
  ∃ (a_1 : ℤ),
    (a_1 ∈ Ico (a - v) (b - v) ∧ r ∣ a_1) ∧ ({ toFun := fun (x : ℤ) ↦ x + v, inj' := sorry : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
Tactic: simp_rw [mem_map, mem_filter, mem_Ico, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v x : ℤ
h :
  x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    ∃ a_1 ∈ {x ∈ Ico (a - v) (b - v) | r ∣ x},
      ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₁ :
  x ∈ Ico a b ∧ x ≡ v [ZMOD r] ↔
    ∃ (a_1 : ℤ),
      (a_1 ∈ Ico (a - v) (b - v) ∧ r ∣ a_1) ∧
        ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
⊢ x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    x ∈ map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})
have h₂ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔
  ∃ (a_1 : ℤ),
    ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧
      ({ toFun := fun (x : ℤ) ↦ x + v, inj' := sorry : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
Tactic: simp_rw [mem_map, mem_filter, mem_Ico, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v x : ℤ
h :
  x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    ∃ a_1 ∈ {x ∈ Ico (a - v) (b - v) | r ∣ x},
      ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₁ :
  x ∈ Ico a b ∧ x ≡ v [ZMOD r] ↔
    ∃ (a_1 : ℤ),
      (a_1 ∈ Ico (a - v) (b - v) ∧ r ∣ a_1) ∧
        ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₂ :
  (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔
    ∃ (a_1 : ℤ),
      ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧
        ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
⊢ x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    x ∈ map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})
have h₃ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ ∃ (a_1 : ℤ), ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧ a_1 + v = x
Tactic: simp_rw [mem_map, mem_filter, mem_Ico, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v x : ℤ
h :
  x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    ∃ a_1 ∈ {x ∈ Ico (a - v) (b - v) | r ∣ x},
      ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₁ :
  x ∈ Ico a b ∧ x ≡ v [ZMOD r] ↔
    ∃ (a_1 : ℤ),
      (a_1 ∈ Ico (a - v) (b - v) ∧ r ∣ a_1) ∧
        ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₂ :
  (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔
    ∃ (a_1 : ℤ),
      ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧
        ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₃ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ ∃ (a_1 : ℤ), ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧ a_1 + v = x
⊢ x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    x ∈ map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})
have h₄ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ ∃ (a_1 : ℤ), ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧ a_1 = x - v
Tactic: simp_rw [mem_map, mem_filter, mem_Ico, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v x : ℤ
h :
  x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    ∃ a_1 ∈ {x ∈ Ico (a - v) (b - v) | r ∣ x},
      ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₁ :
  x ∈ Ico a b ∧ x ≡ v [ZMOD r] ↔
    ∃ (a_1 : ℤ),
      (a_1 ∈ Ico (a - v) (b - v) ∧ r ∣ a_1) ∧
        ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₂ :
  (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔
    ∃ (a_1 : ℤ),
      ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧
        ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₃ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ ∃ (a_1 : ℤ), ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧ a_1 + v = x
h₄ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ ∃ (a_1 : ℤ), ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧ a_1 = x - v
⊢ x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    x ∈ map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})
have h₅ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ (a - v ≤ x - v ∧ x - v < b - v) ∧ r ∣ x - v
Tactic: simp_rw [mem_map, mem_filter, mem_Ico, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v x : ℤ
h :
  x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    ∃ a_1 ∈ {x ∈ Ico (a - v) (b - v) | r ∣ x},
      ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₁ :
  x ∈ Ico a b ∧ x ≡ v [ZMOD r] ↔
    ∃ (a_1 : ℤ),
      (a_1 ∈ Ico (a - v) (b - v) ∧ r ∣ a_1) ∧
        ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₂ :
  (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔
    ∃ (a_1 : ℤ),
      ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧
        ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₃ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ ∃ (a_1 : ℤ), ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧ a_1 + v = x
h₄ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ ∃ (a_1 : ℤ), ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧ a_1 = x - v
h₅ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ (a - v ≤ x - v ∧ x - v < b - v) ∧ r ∣ x - v
⊢ x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    x ∈ map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})
have h₆ : (a ≤ x ∧ x < b) ∧ v ≡ x [ZMOD r] ↔ (a - v ≤ x - v ∧ x - v < b - v) ∧ r ∣ x - v
Tactic: simp_rw [mem_map, mem_filter, mem_Ico, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v x : ℤ
h :
  x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    ∃ a_1 ∈ {x ∈ Ico (a - v) (b - v) | r ∣ x},
      ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₁ :
  x ∈ Ico a b ∧ x ≡ v [ZMOD r] ↔
    ∃ (a_1 : ℤ),
      (a_1 ∈ Ico (a - v) (b - v) ∧ r ∣ a_1) ∧
        ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₂ :
  (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔
    ∃ (a_1 : ℤ),
      ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧
        ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₃ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ ∃ (a_1 : ℤ), ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧ a_1 + v = x
h₄ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ ∃ (a_1 : ℤ), ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧ a_1 = x - v
h₅ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ (a - v ≤ x - v ∧ x - v < b - v) ∧ r ∣ x - v
h₆ : (a ≤ x ∧ x < b) ∧ v ≡ x [ZMOD r] ↔ (a - v ≤ x - v ∧ x - v < b - v) ∧ r ∣ x - v
⊢ x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    x ∈ map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})
have h₇ : (a ≤ x ∧ x < b) ∧ r ∣ x - v ↔ (a - v ≤ x - v ∧ x - v < b - v) ∧ r ∣ x - v
Tactic: simp_rw [mem_map, mem_filter, mem_Ico, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v x : ℤ
h :
  x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    ∃ a_1 ∈ {x ∈ Ico (a - v) (b - v) | r ∣ x},
      ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₁ :
  x ∈ Ico a b ∧ x ≡ v [ZMOD r] ↔
    ∃ (a_1 : ℤ),
      (a_1 ∈ Ico (a - v) (b - v) ∧ r ∣ a_1) ∧
        ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₂ :
  (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔
    ∃ (a_1 : ℤ),
      ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧
        ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₃ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ ∃ (a_1 : ℤ), ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧ a_1 + v = x
h₄ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ ∃ (a_1 : ℤ), ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧ a_1 = x - v
h₅ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ (a - v ≤ x - v ∧ x - v < b - v) ∧ r ∣ x - v
h₆ : (a ≤ x ∧ x < b) ∧ v ≡ x [ZMOD r] ↔ (a - v ≤ x - v ∧ x - v < b - v) ∧ r ∣ x - v
h₇ : (a ≤ x ∧ x < b) ∧ r ∣ x - v ↔ (a - v ≤ x - v ∧ x - v < b - v) ∧ r ∣ x - v
⊢ x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    x ∈ map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})
have h₈ : (a ≤ x ∧ x < b) ∧ r ∣ x - v ↔ (a - v ≤ x - v ∧ x < b) ∧ r ∣ x - v
Tactic: simp_rw [mem_map, mem_filter, mem_Ico, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℤ
⊢ {x ∈ Ioc a b | x ≡ v [ZMOD r]} =
    map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ioc (a - v) (b - v) | r ∣ x})
have h : ∀ (x : ℤ),
  x ∈ {x ∈ Ioc a b | x ≡ v [ZMOD r]} ↔
    x ∈ map { toFun := fun (x : ℤ) ↦ x + v, inj' := sorry : ℤ ↪ ℤ } ({x ∈ Ioc (a - v) (b - v) | r ∣ x})
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v x : ℤ
⊢ x ∈ {x ∈ Ioc a b | x ≡ v [ZMOD r]} ↔
    x ∈ map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ioc (a - v) (b - v) | r ∣ x})
have h : x ∈ {x ∈ Ioc a b | x ≡ v [ZMOD r]} ↔
  ∃ a_1 ∈ {x ∈ Ioc (a - v) (b - v) | r ∣ x}, ({ toFun := fun (x : ℤ) ↦ x + v, inj' := sorry : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
Tactic: simp_rw [mem_map, mem_filter, mem_Ioc, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v x : ℤ
h :
  x ∈ {x ∈ Ioc a b | x ≡ v [ZMOD r]} ↔
    ∃ a_1 ∈ {x ∈ Ioc (a - v) (b - v) | r ∣ x},
      ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
⊢ x ∈ {x ∈ Ioc a b | x ≡ v [ZMOD r]} ↔
    x ∈ map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ioc (a - v) (b - v) | r ∣ x})
have h₁ : x ∈ Ioc a b ∧ x ≡ v [ZMOD r] ↔
  ∃ (a_1 : ℤ),
    (a_1 ∈ Ioc (a - v) (b - v) ∧ r ∣ a_1) ∧ ({ toFun := fun (x : ℤ) ↦ x + v, inj' := sorry : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
Tactic: simp_rw [mem_map, mem_filter, mem_Ioc, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]