case h
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (y ∈ ⋃ (k : E n), cylinder (update x n k) (n + 1)) ↔ y ∈ cylinder x n
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
⊢ (⋃ (k : E n), cylinder (update x n k) (n + 1)) = cylinder x n
ext y
case h
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∃ i, ∀ (i_1 : ℕ), i_1 < n + 1 → y i_1 = update x n i i_1) ↔ ∀ (i : ℕ), i < n → y i = x i
case h
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (y ∈ ⋃ (k : E n), cylinder (update x n k) (n + 1)) ↔ y ∈ cylinder x n
simp only [mem_cylinder_iff, mem_iUnion]
case h.mp
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∃ i, ∀ (i_1 : ℕ), i_1 < n + 1 → y i_1 = update x n i i_1) → ∀ (i : ℕ), i < n → y i = x i

case h.mpr
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∀ (i : ℕ), i < n → y i = x i) → ∃ i, ∀ (i_1 : ℕ), i_1 < n + 1 → y i_1 = update x n i i_1
case h
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∃ i, ∀ (i_1 : ℕ), i_1 < n + 1 → y i_1 = update x n i i_1) ↔ ∀ (i : ℕ), i < n → y i = x i
constructor
case h.mp.intro
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
k : E n
hk : ∀ (i : ℕ), i < n + 1 → y i = update x n k i
i : ℕ
hi : i < n
⊢ y i = x i
case h.mp
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∃ i, ∀ (i_1 : ℕ), i_1 < n + 1 → y i_1 = update x n i i_1) → ∀ (i : ℕ), i < n → y i = x i
rintro ⟨k, hk⟩ i hi
no goals
case h.mp.intro
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
k : E n
hk : ∀ (i : ℕ), i < n + 1 → y i = update x n k i
i : ℕ
hi : i < n
⊢ y i = x i
simpa [hi.ne] using hk i (Nat.lt_succ_of_lt hi)
case h.mpr
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ (i : ℕ), i < n → y i = x i
⊢ ∃ i, ∀ (i_1 : ℕ), i_1 < n + 1 → y i_1 = update x n i i_1
case h.mpr
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ (∀ (i : ℕ), i < n → y i = x i) → ∃ i, ∀ (i_1 : ℕ), i_1 < n + 1 → y i_1 = update x n i i_1
intro H
case h.mpr
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ (i : ℕ), i < n → y i = x i
i : ℕ
hi : i < n + 1
⊢ y i = update x n (y n) i
case h.mpr
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ (i : ℕ), i < n → y i = x i
⊢ ∃ i, ∀ (i_1 : ℕ), i_1 < n + 1 → y i_1 = update x n i i_1
refine' ⟨y n, fun i hi => _⟩
case h.mpr.inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ (i : ℕ), 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_1 < i → y i_1 = x i_1
hi : i < i + 1
⊢ y i = update x i (y i) i
case h.mpr
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ (i : ℕ), i < n → y i = x i
i : ℕ
hi : i < n + 1
⊢ y i = update x n (y n) i
rcases Nat.lt_succ_iff_lt_or_eq.1 hi with (h'i | rfl)
no goals
case h.mpr.inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
H : ∀ (i : ℕ), i < n → y i = x i
i : ℕ
hi : i < n + 1
h'i : i < n
⊢ y i = update x n (y n) i
simp [H i h'i, h'i.ne]
no goals
case h.mpr.inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
i : ℕ
H : ∀ (i_1 : ℕ), i_1 < i → y i_1 = x i_1
hi : i < i + 1
⊢ y i = update x i (y i) i
simp