awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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' := ⋯ : ℤ ↪ ℤ } : (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₂ : (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_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
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' := ⋯ : ℤ ↪ ℤ } : (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 ∈ 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₃ : (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_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
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' := ⋯ : ℤ ↪ ℤ } : (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 ∈ 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₄ : (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_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
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' := ⋯ : ℤ ↪ ℤ } : (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 ∈ 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₅ : (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_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
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' := ⋯ : ℤ ↪ ℤ } : (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 ∈ 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₆ : (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_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
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' := ⋯ : ℤ ↪ ℤ } : (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 ∈ 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₇ : (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_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
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' := ⋯ : ℤ ↪ ℤ } : (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 ∈ 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₈ : (a < x ∧ x ≤ b) ∧ r ∣ x - v ↔ (a < x ∧ x - v ≤ b - v) ∧ r ∣ x - v
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 : ℤ
hr : 0 < r
⊢ {x ∈ Ico a b | r ∣ x} =
    map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
      (Ico ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉ ⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉)
have h : ∀ (x : ℤ),
  x ∈ {x ∈ Ico a b | r ∣ x} ↔
    x ∈
      map { toFun := fun (x : ℤ) ↦ x * r, inj' := sorry : ℤ ↪ ℤ }
        (Ico ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉ ⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r : ℤ
hr : 0 < r
x : ℤ
⊢ x ∈ {x ∈ Ico a b | r ∣ x} ↔
    x ∈
      map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
        (Ico ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉ ⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉)
have h : ((a ≤ x ∧ x < b) ∧ ∃ (c : ℤ), x = c * r) ↔
  ∃ (a_1 : ℤ), (a ≤ a_1 * r ∧ a_1 * r < b) ∧ ({ toFun := fun (x : ℤ) ↦ x * r, inj' := sorry : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
Tactic: simp only [mem_map, mem_filter, mem_Ico, ceil_le, lt_ceil, div_le_iff₀, lt_div_iff₀,
    dvd_iff_exists_eq_mul_left, cast_pos.2 hr, ← cast_mul, cast_lt, cast_le]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r : ℤ
hr : 0 < r
⊢ {x ∈ Ioc a b | r ∣ x} =
    map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
      (Ioc ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋ ⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋)
have h : ∀ (x : ℤ),
  x ∈ {x ∈ Ioc a b | r ∣ x} ↔
    x ∈
      map { toFun := fun (x : ℤ) ↦ x * r, inj' := sorry : ℤ ↪ ℤ }
        (Ioc ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋ ⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r : ℤ
hr : 0 < r
x : ℤ
⊢ x ∈ {x ∈ Ioc a b | r ∣ x} ↔
    x ∈
      map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
        (Ioc ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋ ⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋)
have h : ((a < x ∧ x ≤ b) ∧ ∃ (c : ℤ), x = c * r) ↔
  ∃ (a_1 : ℤ), (a < a_1 * r ∧ a_1 * r ≤ b) ∧ ({ toFun := fun (x : ℤ) ↦ x * r, inj' := sorry : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
Tactic: simp only [mem_map, mem_filter, mem_Ioc, floor_lt, le_floor, div_lt_iff₀, le_div_iff₀,
    dvd_iff_exists_eq_mul_left, cast_pos.2 hr, ← cast_mul, cast_lt, cast_le]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r : ℤ
hr : 0 < r
⊢ (↑(#({x ∈ Ico a b | r ∣ x})) : ℤ) =
    max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
have rw : (↑(#(map { toFun := fun (x : ℤ) ↦ x * r, inj' := sorry : ℤ ↪ ℤ }
          (Ico ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉ ⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉))) :
    ℤ) =
  max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
Tactic: rw [Ico_filter_dvd_eq _ _ hr, card_map, card_Ico, toNat_eq_max]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r : ℤ
hr : 0 < r
rw :
  (↑(#(map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
            (Ico ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉ ⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉))) :
      ℤ) =
    max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
⊢ (↑(#({x ∈ Ico a b | r ∣ x})) : ℤ) =
    max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
have rw₁ : (↑(#(Ico ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉ ⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉)) : ℤ) =
  max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
Tactic: rw [Ico_filter_dvd_eq _ _ hr, card_map, card_Ico, toNat_eq_max]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r : ℤ
hr : 0 < r
rw :
  (↑(#(map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
            (Ico ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉ ⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉))) :
      ℤ) =
    max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
rw₁ :
  (↑(#(Ico ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉ ⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉)) : ℤ) =
    max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
⊢ (↑(#({x ∈ Ico a b | r ∣ x})) : ℤ) =
    max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
have rw₂ : (↑(⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉).toNat : ℤ) =
  max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
Tactic: rw [Ico_filter_dvd_eq _ _ hr, card_map, card_Ico, toNat_eq_max]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r : ℤ
hr : 0 < r
rw :
  (↑(#(map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
            (Ico ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉ ⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉))) :
      ℤ) =
    max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
rw₁ :
  (↑(#(Ico ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉ ⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉)) : ℤ) =
    max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
rw₂ :
  (↑(⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉).toNat : ℤ) =
    max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
⊢ (↑(#({x ∈ Ico a b | r ∣ x})) : ℤ) =
    max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
have rw₃ : max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0 =
  max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
Tactic: rw [Ico_filter_dvd_eq _ _ hr, card_map, card_Ico, toNat_eq_max]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r : ℤ
hr : 0 < r
⊢ (↑(#({x ∈ Ioc a b | r ∣ x})) : ℤ) =
    max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
have rw : (↑(#(map { toFun := fun (x : ℤ) ↦ x * r, inj' := sorry : ℤ ↪ ℤ }
          (Ioc ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋ ⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋))) :
    ℤ) =
  max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
Tactic: rw [Ioc_filter_dvd_eq _ _ hr, card_map, card_Ioc, toNat_eq_max]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r : ℤ
hr : 0 < r
rw :
  (↑(#(map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
            (Ioc ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋ ⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋))) :
      ℤ) =
    max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
⊢ (↑(#({x ∈ Ioc a b | r ∣ x})) : ℤ) =
    max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
have rw₁ : (↑(#(Ioc ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋ ⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋)) : ℤ) =
  max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
Tactic: rw [Ioc_filter_dvd_eq _ _ hr, card_map, card_Ioc, toNat_eq_max]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r : ℤ
hr : 0 < r
rw :
  (↑(#(map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
            (Ioc ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋ ⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋))) :
      ℤ) =
    max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
rw₁ :
  (↑(#(Ioc ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋ ⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋)) : ℤ) =
    max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
⊢ (↑(#({x ∈ Ioc a b | r ∣ x})) : ℤ) =
    max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
have rw₂ : (↑(⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋).toNat : ℤ) =
  max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
Tactic: rw [Ioc_filter_dvd_eq _ _ hr, card_map, card_Ioc, toNat_eq_max]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r : ℤ
hr : 0 < r
rw :
  (↑(#(map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
            (Ioc ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋ ⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋))) :
      ℤ) =
    max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
rw₁ :
  (↑(#(Ioc ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋ ⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋)) : ℤ) =
    max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
rw₂ :
  (↑(⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋).toNat : ℤ) =
    max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
⊢ (↑(#({x ∈ Ioc a b | r ∣ x})) : ℤ) =
    max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
have rw₃ : max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0 =
  max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
Tactic: rw [Ioc_filter_dvd_eq _ _ hr, card_map, card_Ioc, toNat_eq_max]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℕ
⊢ Eq (α := Finset ℤ) (map castEmbedding ({x ∈ Ico a b | x ≡ v [MOD r]}))
    ({x ∈ Ico (↑a : ℤ) (↑b : ℤ) | x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]})
have h : ∀ (x : ℤ),
  Membership.mem (γ := Finset ℤ) (map castEmbedding ({x ∈ Ico a b | x ≡ v [MOD r]})) x ↔
    Membership.mem (γ := Finset ℤ) ({x ∈ Ico (↑a : ℤ) (↑b : ℤ) | x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]}) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℕ
x : ℤ
⊢ Membership.mem (γ := Finset ℤ) (map castEmbedding ({x ∈ Ico a b | x ≡ v [MOD r]})) x ↔
    Membership.mem (γ := Finset ℤ) ({x ∈ Ico (↑a : ℤ) (↑b : ℤ) | x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]}) x
have h : (∃ (a_1 : ℕ), ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) ↔
  ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
Tactic: simp only [mem_map, mem_filter, mem_Ico, castEmbedding_apply]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℕ
x : ℤ
⊢ (∃ (a_1 : ℕ), ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) ↔
    ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
have h : (∃ (a_1 : ℕ), ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) →
  ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℕ
x : ℤ
h :
  (∃ (a_1 : ℕ), ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) →
    ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ (∃ (a_1 : ℕ), ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) ↔
    ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
have h₁ : ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)] →
  ∃ (a_2 : ℕ), ((a ≤ a_2 ∧ a_2 < b) ∧ a_2 ≡ v [MOD r]) ∧ (↑a_2 : ℤ) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℕ
x : ℤ
⊢ (∃ (a_1 : ℕ), ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) →
    ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
have h : ∀ (x_1 : ℕ) (h : ((a ≤ x_1 ∧ x_1 < b) ∧ (↑x_1 : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]) ∧ (↑x_1 : ℤ) = x),
  ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
Tactic: simp_rw [forall_exists_index, ← natCast_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℕ
x : ℤ
y : ℕ
⊢ ∀ (h : ((a ≤ y ∧ y < b) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]) ∧ (↑y : ℤ) = x),
    ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
have h : ∀ (h : (a ≤ y ∧ y < b) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]) (c : (↑y : ℤ) = x),
  ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
Tactic: ⟨h, c⟩
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℕ
x : ℤ
y : ℕ
h : (a ≤ y ∧ y < b) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
c : (↑y : ℤ) = x
⊢ ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
have h₁ : (LE.le (α := ℤ) (↑a : ℤ) (↑y : ℤ) ∧ LT.lt (α := ℤ) (↑y : ℤ) (↑b : ℤ)) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
Tactic: subst c
Cleared hypotheses: x, c
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℕ
x : ℤ
h : ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ ∃ (a_1 : ℕ), ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x
have h₁ : ∀ (x : ℕ)
  (h : (LE.le (α := ℤ) (↑a : ℤ) (↑x : ℤ) ∧ LT.lt (α := ℤ) (↑x : ℤ) (↑b : ℤ)) ∧ (↑x : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]),
  ∃ (a_1 : ℕ), ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ Eq (α := ℤ) (↑a_1 : ℤ) (↑x : ℤ)
Tactic: lift x to ℕ using (by omega)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℕ
⊢ Eq (α := Finset ℤ) (map castEmbedding ({x ∈ Ioc a b | x ≡ v [MOD r]}))
    ({x ∈ Ioc (↑a : ℤ) (↑b : ℤ) | x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]})
have h : ∀ (x : ℤ),
  Membership.mem (γ := Finset ℤ) (map castEmbedding ({x ∈ Ioc a b | x ≡ v [MOD r]})) x ↔
    Membership.mem (γ := Finset ℤ) ({x ∈ Ioc (↑a : ℤ) (↑b : ℤ) | x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]}) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℕ
x : ℤ
⊢ Membership.mem (γ := Finset ℤ) (map castEmbedding ({x ∈ Ioc a b | x ≡ v [MOD r]})) x ↔
    Membership.mem (γ := Finset ℤ) ({x ∈ Ioc (↑a : ℤ) (↑b : ℤ) | x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]}) x
have h : (∃ (a_1 : ℕ), ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) ↔
  ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
Tactic: simp only [mem_map, mem_filter, mem_Ioc, castEmbedding_apply]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℕ
x : ℤ
⊢ (∃ (a_1 : ℕ), ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) ↔
    ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
have h : (∃ (a_1 : ℕ), ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) →
  ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℕ
x : ℤ
h :
  (∃ (a_1 : ℕ), ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) →
    ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ (∃ (a_1 : ℕ), ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) ↔
    ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
have h₁ : ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)] →
  ∃ (a_2 : ℕ), ((a < a_2 ∧ a_2 ≤ b) ∧ a_2 ≡ v [MOD r]) ∧ (↑a_2 : ℤ) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℕ
x : ℤ
⊢ (∃ (a_1 : ℕ), ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) →
    ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
have h : ∀ (x_1 : ℕ) (h : ((a < x_1 ∧ x_1 ≤ b) ∧ (↑x_1 : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]) ∧ (↑x_1 : ℤ) = x),
  ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
Tactic: simp_rw [forall_exists_index, ← natCast_modEq_iff]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℕ
x : ℤ
y : ℕ
⊢ ∀ (h : ((a < y ∧ y ≤ b) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]) ∧ (↑y : ℤ) = x),
    ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
have h : ∀ (h : (a < y ∧ y ≤ b) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]) (c : (↑y : ℤ) = x),
  ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
Tactic: ⟨h, c⟩