case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
⊢ a < c
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
⊢ a < b → b < c → a < c
rintro ⟨k₁, k₁z, notinA, inB⟩ ⟨k₂, k₂z, notinB, inC⟩
case intro.intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
⊢ a < c

case intro.intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ > k₂
⊢ a < c
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
⊢ a < c
cases' lt_or_gt_of_ne (ne_of_mem_of_not_mem inB notinB) with h h
case intro.intro.intro.intro.intro.intro.inl.refine'_1
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
x : α
hx : k₂ < x
⊢ x ∈ a ↔ x ∈ c

case intro.intro.intro.intro.intro.intro.inl.refine'_2
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
⊢ ¬k₂ ∈ a
case intro.intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
⊢ a < c
refine' ⟨k₂, @fun x hx => _, _, inC⟩
case intro.intro.intro.intro.intro.intro.inl.refine'_1
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
x : α
hx : k₂ < x
⊢ x ∈ a ↔ x ∈ b

case intro.intro.intro.intro.intro.intro.inl.refine'_2
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
⊢ ¬k₂ ∈ a
case intro.intro.intro.intro.intro.intro.inl.refine'_1
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
x : α
hx : k₂ < x
⊢ x ∈ a ↔ x ∈ c

case intro.intro.intro.intro.intro.intro.inl.refine'_2
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
⊢ ¬k₂ ∈ a
rw [← k₂z hx]
case intro.intro.intro.intro.intro.intro.inl.refine'_2
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
⊢ ¬k₂ ∈ a
case intro.intro.intro.intro.intro.intro.inl.refine'_1
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
x : α
hx : k₂ < x
⊢ x ∈ a ↔ x ∈ b

case intro.intro.intro.intro.intro.intro.inl.refine'_2
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
⊢ ¬k₂ ∈ a
apply k₁z (Trans.trans h hx)
no goals
case intro.intro.intro.intro.intro.intro.inl.refine'_2
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ < k₂
⊢ ¬k₂ ∈ a
rwa [k₁z h]
case intro.intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ > k₂
x : α
hx : k₁ < x
⊢ x ∈ a ↔ x ∈ c
case intro.intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ > k₂
⊢ a < c
refine' ⟨k₁, @fun x hx => _, notinA, by rwa [← k₂z h]⟩
case intro.intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ > k₂
x : α
hx : k₁ < x
⊢ x ∈ b ↔ x ∈ c
case intro.intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ > k₂
x : α
hx : k₁ < x
⊢ x ∈ a ↔ x ∈ c
rw [k₁z hx]
no goals
case intro.intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ > k₂
x : α
hx : k₁ < x
⊢ x ∈ b ↔ x ∈ c
apply k₂z (Trans.trans h hx)
no goals
α : Type u_1
inst✝ : LinearOrder α
a b c : Colex α
k₁ : α
k₁z : ∀ {x : α}, k₁ < x → (x ∈ a ↔ x ∈ b)
notinA : ¬k₁ ∈ a
inB : k₁ ∈ b
k₂ : α
k₂z : ∀ {x : α}, k₂ < x → (x ∈ b ↔ x ∈ c)
notinB : ¬k₂ ∈ b
inC : k₂ ∈ c
h : k₁ > k₂
⊢ k₁ ∈ c
rwa [← k₂z h]