-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem iUnion_cylinder_update (x : ∀ n, E n) (n : ℕ) :
    ⋃ k, cylinder (update x n k) (n + 1) = cylinder x n

Proof state:
case h.mpr
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ i < n, y i = x i
i : ℕ
hi : i < n + 1
⊢ y i = update x n (y n) i

Tactic:
rcases Nat.lt_succ_iff_lt_or_eq.1 hi with (h'i | rfl)

Result:
case h.mpr.inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ i < n, y i = x i
i : ℕ
hi : i < n + 1
h'i : i < n
⊢ y i = update x n (y n) i

case h.mpr.inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
i : ℕ
H : ∀ i_1 < i, y i_1 = x i_1
hi : i < i + 1
⊢ y i = update x i (y i) i

Proof state:
case h.mpr.inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ i < n, y i = x i
i : ℕ
hi : i < n + 1
h'i : i < n
⊢ y i = update x n (y n) i

Tactic:
simp [H i h'i, h'i.ne]

Result:
no goals

Proof state:
case h
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∃ i, ∀ i_1 < n + 1, y i_1 = update x n i i_1) ↔ ∀ i < n, y i = x i

Tactic:
constructor

Result:
case h.mp
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∃ i, ∀ i_1 < n + 1, y i_1 = update x n i i_1) → ∀ i < n, y i = x i

case h.mpr
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∀ i < n, y i = x i) → ∃ i, ∀ i_1 < n + 1, y i_1 = update x n i i_1

Proof state:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
⊢ ⋃ k, cylinder (update x n k) (n + 1) = cylinder x n

Tactic:
ext y

Result:
case h
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ y ∈ ⋃ k, cylinder (update x n k) (n + 1) ↔ y ∈ cylinder x n

Proof state:
case h.mpr.inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
i : ℕ
H : ∀ i_1 < i, y i_1 = x i_1
hi : i < i + 1
⊢ y i = update x i (y i) i

Tactic:
simp

Result:
no goals

Proof state:
case h.mpr
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∀ i < n, y i = x i) → ∃ i, ∀ i_1 < n + 1, y i_1 = update x n i i_1

Tactic:
intro H

Result:
case h.mpr
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ i < n, y i = x i
⊢ ∃ i, ∀ i_1 < n + 1, y i_1 = update x n i i_1

Proof state:
case h.mp
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∃ i, ∀ i_1 < n + 1, y i_1 = update x n i i_1) → ∀ i < n, y i = x i

Tactic:
rintro ⟨k, hk⟩ i hi

Result:
case h.mp.intro
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
k : E n
hk : ∀ i < n + 1, y i = update x n k i
i : ℕ
hi : i < n
⊢ y i = x i

Proof state:
case h.mpr
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ i < n, y i = x i
⊢ ∃ i, ∀ i_1 < n + 1, y i_1 = update x n i i_1

Tactic:
refine ⟨y n, fun i hi => ?_⟩

Result:
case h.mpr
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ i < n, y i = x i
i : ℕ
hi : i < n + 1
⊢ y i = update x n (y n) i

Proof state:
case h.mp.intro
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
k : E n
hk : ∀ i < n + 1, y i = update x n k i
i : ℕ
hi : i < n
⊢ y i = x i

Tactic:
simpa [hi.ne] using hk i (Nat.lt_succ_of_lt hi)

Result:
no goals

Proof state:
case h
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ y ∈ ⋃ k, cylinder (update x n k) (n + 1) ↔ y ∈ cylinder x n

Tactic:
simp only [mem_cylinder_iff, mem_iUnion]

Result:
case h
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∃ i, ∀ i_1 < n + 1, y i_1 = update x n i i_1) ↔ ∀ i < n, y i = x i