case a
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ x ∈ image (fun x => x - c) (Ico a b) ↔ x ∈ Ico (a - c) (b - c)
a b c : ℕ
h : c ≤ a
⊢ image (fun x => x - c) (Ico a b) = Ico (a - c) (b - c)
ext x
case a
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ (∃ a_1, a_1 ∈ Ico a b ∧ a_1 - c = x) ↔ x ∈ Ico (a - c) (b - c)
case a
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ x ∈ image (fun x => x - c) (Ico a b) ↔ x ∈ Ico (a - c) (b - c)
rw [mem_image]
case a.mp
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ (∃ a_1, a_1 ∈ Ico a b ∧ a_1 - c = x) → x ∈ Ico (a - c) (b - c)

case a.mpr
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ x ∈ Ico (a - c) (b - c) → ∃ a_2, a_2 ∈ Ico a b ∧ a_2 - c = x
case a
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ (∃ a_1, a_1 ∈ Ico a b ∧ a_1 - c = x) ↔ x ∈ Ico (a - c) (b - c)
constructor
case a.mp.intro.intro
a b c : ℕ
h : c ≤ a
x : ℕ
hx : x ∈ Ico a b
⊢ x - c ∈ Ico (a - c) (b - c)
case a.mp
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ (∃ a_1, a_1 ∈ Ico a b ∧ a_1 - c = x) → x ∈ Ico (a - c) (b - c)
rintro ⟨x, hx, rfl⟩
case a.mp.intro.intro
a b c : ℕ
h : c ≤ a
x : ℕ
hx : a ≤ x ∧ x < b
⊢ a - c ≤ x - c ∧ x - c < b - c
case a.mp.intro.intro
a b c : ℕ
h : c ≤ a
x : ℕ
hx : x ∈ Ico a b
⊢ x - c ∈ Ico (a - c) (b - c)
rw [mem_Ico] at hx⊢
no goals
case a.mp.intro.intro
a b c : ℕ
h : c ≤ a
x : ℕ
hx : a ≤ x ∧ x < b
⊢ a - c ≤ x - c ∧ x - c < b - c
exact ⟨tsub_le_tsub_right hx.1 _, tsub_lt_tsub_right_of_le (h.trans hx.1) hx.2⟩
case a.mpr
a b c : ℕ
h✝ : c ≤ a
x : ℕ
h : x ∈ Ico (a - c) (b - c)
⊢ ∃ a_1, a_1 ∈ Ico a b ∧ a_1 - c = x
case a.mpr
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ x ∈ Ico (a - c) (b - c) → ∃ a_2, a_2 ∈ Ico a b ∧ a_2 - c = x
rintro h
case a.mpr
a b c : ℕ
h✝ : c ≤ a
x : ℕ
h : x ∈ Ico (a - c) (b - c)
⊢ x + c ∈ Ico a b
case a.mpr
a b c : ℕ
h✝ : c ≤ a
x : ℕ
h : x ∈ Ico (a - c) (b - c)
⊢ ∃ a_1, a_1 ∈ Ico a b ∧ a_1 - c = x
refine' ⟨x + c, _, add_tsub_cancel_right _ _⟩
case a.mpr
a b c : ℕ
h✝ : c ≤ a
x : ℕ
h : a - c ≤ x ∧ x < b - c
⊢ a ≤ x + c ∧ x + c < b
case a.mpr
a b c : ℕ
h✝ : c ≤ a
x : ℕ
h : x ∈ Ico (a - c) (b - c)
⊢ x + c ∈ Ico a b
rw [mem_Ico] at h⊢
no goals
case a.mpr
a b c : ℕ
h✝ : c ≤ a
x : ℕ
h : a - c ≤ x ∧ x < b - c
⊢ a ≤ x + c ∧ x + c < b
exact ⟨tsub_le_iff_right.1 h.1, lt_tsub_iff_right.1 h.2⟩