case intro
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
hb : some b ∈ c
i : ℕ
ha : some a = ↑c i
⊢ a = b
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
ha : some a ∈ c
hb : some b ∈ c
⊢ a = b
cases' ha with i ha
case intro
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
hb : some b ∈ c
i : ℕ
ha : ↑c i = some a
⊢ a = b
case intro
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
hb : some b ∈ c
i : ℕ
ha : some a = ↑c i
⊢ a = b
replace ha := ha.symm
case intro.intro
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : ↑c i = some a
j : ℕ
hb : some b = ↑c j
⊢ a = b
case intro
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
hb : some b ∈ c
i : ℕ
ha : ↑c i = some a
⊢ a = b
cases' hb with j hb
case intro.intro
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : ↑c i = some a
j : ℕ
hb : ↑c j = some b
⊢ a = b
case intro.intro
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : ↑c i = some a
j : ℕ
hb : some b = ↑c j
⊢ a = b
replace hb := hb.symm
case intro.intro
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
⊢ a = b
case intro.intro
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : ↑c i = some a
j : ℕ
hb : ↑c j = some b
⊢ a = b
rw [eq_some_iff] at ha hb
case intro.intro.inl
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hij : i ≤ j
⊢ a = b

case intro.intro.inr
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hji : j ≤ i
⊢ a = b
case intro.intro
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
⊢ a = b
cases' le_total i j with hij hji
case intro.intro.inr
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hji : j ≤ i
⊢ a = b
case intro.intro.inl
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hij : i ≤ j
⊢ a = b

case intro.intro.inr
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hji : j ≤ i
⊢ a = b
. have := c.monotone hij _ ha; apply mem_unique this hb
no goals
case intro.intro.inr
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hji : j ≤ i
⊢ a = b
. have := c.monotone hji _ hb; apply Eq.symm; apply mem_unique this ha
case intro.intro.inl
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hij : i ≤ j
this : a ∈ ↑c j
⊢ a = b
case intro.intro.inl
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hij : i ≤ j
⊢ a = b
have := c.monotone hij _ ha
no goals
case intro.intro.inl
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hij : i ≤ j
this : a ∈ ↑c j
⊢ a = b
apply mem_unique this hb
case intro.intro.inr
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hji : j ≤ i
this : b ∈ ↑c i
⊢ a = b
case intro.intro.inr
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hji : j ≤ i
⊢ a = b
have := c.monotone hji _ hb
case intro.intro.inr.h
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hji : j ≤ i
this : b ∈ ↑c i
⊢ b = a
case intro.intro.inr
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hji : j ≤ i
this : b ∈ ↑c i
⊢ a = b
apply Eq.symm
no goals
case intro.intro.inr.h
α : Type u
β : Type v
γ : Type ?u.13795
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hji : j ≤ i
this : b ∈ ↑c i
⊢ b = a
apply mem_unique this ha