-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem mem_cylinder_iff_eq {x y : ∀ n, E n} {n : ℕ} :
    y ∈ cylinder x n ↔ cylinder y n = cylinder x n

Proof state:
case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder x n
i : ℕ
hi : i < n
⊢ z i = y i

Tactic:
rw [hy i hi]

Result:
case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder x n
i : ℕ
hi : i < n
⊢ z i = x i

Proof state:
case mp.h₁
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
⊢ cylinder y n ⊆ cylinder x n

Tactic:
intro z hz i hi

Result:
case mp.h₁
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder y n
i : ℕ
hi : i < n
⊢ z i = x i

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder x n ↔ cylinder y n = cylinder x n

Tactic:
constructor

Result:
case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder x n → cylinder y n = cylinder x n

case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ cylinder y n = cylinder x n → y ∈ cylinder x n

Proof state:
case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : cylinder y n = cylinder x n
⊢ y ∈ cylinder x n

Tactic:
rw [← h]

Result:
case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : cylinder y n = cylinder x n
⊢ y ∈ cylinder y n

Proof state:
case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder x n → cylinder y n = cylinder x n

Tactic:
intro hy

Result:
case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
⊢ cylinder y n = cylinder x n

Proof state:
case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
⊢ cylinder x n ⊆ cylinder y n

Tactic:
intro z hz i hi

Result:
case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder x n
i : ℕ
hi : i < n
⊢ z i = y i

Proof state:
case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : cylinder y n = cylinder x n
⊢ y ∈ cylinder y n

Tactic:
exact self_mem_cylinder _ _

Result:
no goals

Proof state:
case mp.h₁
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder y n
i : ℕ
hi : i < n
⊢ z i = y i

Tactic:
exact hz i hi

Result:
no goals

Proof state:
case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ cylinder y n = cylinder x n → y ∈ cylinder x n

Tactic:
intro h

Result:
case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : cylinder y n = cylinder x n
⊢ y ∈ cylinder x n

Proof state:
case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder x n
i : ℕ
hi : i < n
⊢ z i = x i

Tactic:
exact hz i hi

Result:
no goals

Proof state:
case mp.h₁
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder y n
i : ℕ
hi : i < n
⊢ z i = x i

Tactic:
rw [← hy i hi]

Result:
case mp.h₁
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
z : (n : ℕ) → E n
hz : z ∈ cylinder y n
i : ℕ
hi : i < n
⊢ z i = y i

Proof state:
case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
⊢ cylinder y n = cylinder x n

Tactic:
apply Subset.antisymm

Result:
case mp.h₁
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
⊢ cylinder y n ⊆ cylinder x n

case mp.h₂
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hy : y ∈ cylinder x n
⊢ cylinder x n ⊆ cylinder y n