-- Mathlib/Data/Int/CardIntervalMod.lean
lemma Ioc_filter_modEq_cast {v : ℕ} :
    {x ∈ Ioc a b | x ≡ v [MOD r]}.map castEmbedding =
      {x ∈ Ioc (a : ℤ) (b : ℤ) | x ≡ v [ZMOD r]}

Proof state:
a b r v : ℕ
x : ℤ
h : (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
⊢ 0 ≤ x

Tactic:
omega

Result:
no goals

Proof state:
case h.mpr
a b r v : ℕ
x : ℤ
⊢ (↑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:
intro h

Result:
case h.mpr
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

Proof state:
case h.mp
a b r v y : ℕ
h : (a < y ∧ y ≤ b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
⊢ (↑a < ↑y ∧ ↑y ≤ ↑b) ∧ ↑y ≡ ↑v [ZMOD ↑r]

Tactic:
exact_mod_cast h

Result:
no goals

Proof state:
a b r v : ℕ
⊢ map castEmbedding (filter (fun x => x ≡ v [MOD r]) (Ioc a b)) = filter (fun x => x ≡ ↑v [ZMOD ↑r]) (Ioc ↑a ↑b)

Tactic:
ext x

Result:
case h
a b r v : ℕ
x : ℤ
⊢ x ∈ map castEmbedding (filter (fun x => x ≡ v [MOD r]) (Ioc a b)) ↔ x ∈ filter (fun x => x ≡ ↑v [ZMOD ↑r]) (Ioc ↑a ↑b)

Proof state:
case h.mp
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]

Tactic:
simp_rw [forall_exists_index, ← natCast_modEq_iff]

Result:
case h.mp
a b r v : ℕ
x : ℤ
⊢ ∀ (x_1 : ℕ), ((a < x_1 ∧ x_1 ≤ b) ∧ ↑x_1 ≡ ↑v [ZMOD ↑r]) ∧ ↑x_1 = x → (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Proof state:
case h.mpr
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

Tactic:
lift x to ℕ using (by omega)

Result:
case h.mpr.intro
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

Proof state:
case h.mpr.intro
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

Tactic:
exact ⟨x, by simp_all [natCast_modEq_iff]⟩

Result:
no goals

Proof state:
case h
a b r v : ℕ
x : ℤ
⊢ x ∈ map castEmbedding (filter (fun x => x ≡ v [MOD r]) (Ioc a b)) ↔ x ∈ filter (fun x => x ≡ ↑v [ZMOD ↑r]) (Ioc ↑a ↑b)

Tactic:
simp only [mem_map, mem_filter, mem_Ioc, castEmbedding_apply]

Result:
case h
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]

Proof state:
case h
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]

Tactic:
constructor

Result:
case h.mp
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]

case h.mpr
a b r v : ℕ
x : ℤ
⊢ (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r] → ∃ a_2, ((a < a_2 ∧ a_2 ≤ b) ∧ a_2 ≡ v [MOD r]) ∧ ↑a_2 = x

Proof state:
case h.mp
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]

Tactic:
subst c

Result:
case h.mp
a b r v y : ℕ
h : (a < y ∧ y ≤ b) ∧ ↑y ≡ ↑v [ZMOD ↑r]
⊢ (↑a < ↑y ∧ ↑y ≤ ↑b) ∧ ↑y ≡ ↑v [ZMOD ↑r]

Proof state:
case h.mp
a b r v : ℕ
x : ℤ
⊢ ∀ (x_1 : ℕ), ((a < x_1 ∧ x_1 ≤ b) ∧ ↑x_1 ≡ ↑v [ZMOD ↑r]) ∧ ↑x_1 = x → (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
intro y ⟨h, c⟩

Result:
case h.mp
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]

Proof state:
a b r v x : ℕ
h : (↑a < ↑x ∧ ↑x ≤ ↑b) ∧ ↑x ≡ ↑v [ZMOD ↑r]
⊢ ((a < x ∧ x ≤ b) ∧ x ≡ v [MOD r]) ∧ ↑x = ↑x

Tactic:
simp_all [natCast_modEq_iff]

Result:
no goals