case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ x ∈ cylinder y i → i ≤ firstDiff x y

case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ i ≤ firstDiff x y → x ∈ cylinder y i
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ x ∈ cylinder y i ↔ i ≤ firstDiff x y
constructor
case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
h : x ∈ cylinder y i
⊢ i ≤ firstDiff x y
case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ x ∈ cylinder y i → i ≤ firstDiff x y
intro h
case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
h : x ∈ cylinder y i
this : firstDiff x y < i
⊢ False
case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
h : x ∈ cylinder y i
⊢ i ≤ firstDiff x y
by_contra'
no goals
case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
h : x ∈ cylinder y i
this : firstDiff x y < i
⊢ False
exact apply_firstDiff_ne hne (h _ this)
case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
hi : i ≤ firstDiff x y
j : ℕ
hj : j < i
⊢ x j = y j
case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ i ≤ firstDiff x y → x ∈ cylinder y i
intro hi j hj
no goals
case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
hi : i ≤ firstDiff x y
j : ℕ
hj : j < i
⊢ x j = y j
exact apply_eq_of_lt_firstDiff (hj.trans_le hi)