[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
⊢ ∀ (a b c : Σₗ' (i : ι), α i), a ≤ b → b ≤ c → a ≤ c
[PROOFSTEP]
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ ⟨a₃, b₃⟩ ⟨h₁r⟩ ⟨h₂r⟩
[GOAL]
case mk.mk.mk.left.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ { fst := a₁, snd := b₁ } ≤ { fst := a₃, snd := b₃ }
[PROOFSTEP]
left
[GOAL]
case mk.mk.mk.left.left.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ a₁ < a₃
[PROOFSTEP]
apply lt_trans
[GOAL]
case mk.mk.mk.left.left.a.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ a₁ < ?mk.mk.mk.left.left.a.b
case mk.mk.mk.left.left.a.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ ?mk.mk.mk.left.left.a.b < a₃
case mk.mk.mk.left.left.a.b
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ ι
[PROOFSTEP]
repeat' assumption
[GOAL]
case mk.mk.mk.left.left.a.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ a₁ < ?mk.mk.mk.left.left.a.b
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.mk.left.left.a.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ a₂ < a₃
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.mk.left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a✝¹ : a₁ < a₂
b₂✝ : α a₂
a✝ : b₂ ≤ b₂✝
⊢ { fst := a₁, snd := b₁ } ≤ { fst := a₂, snd := b₂✝ }
[PROOFSTEP]
left
[GOAL]
case mk.mk.mk.left.right.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a✝¹ : a₁ < a₂
b₂✝ : α a₂
a✝ : b₂ ≤ b₂✝
⊢ a₁ < a₂
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.mk.right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₃ : ι
b₃ : α a₃
b₂✝ : α a₁
a✝¹ : b₁ ≤ b₂✝
a✝ : a₁ < a₃
⊢ { fst := a₁, snd := b₁ } ≤ { fst := a₃, snd := b₃ }
[PROOFSTEP]
left
[GOAL]
case mk.mk.mk.right.left.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ : α a₁
a₃ : ι
b₃ : α a₃
b₂✝ : α a₁
a✝¹ : b₁ ≤ b₂✝
a✝ : a₁ < a₃
⊢ a₁ < a₃
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.mk.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ { fst := a₁, snd := b₁ } ≤ { fst := a₁, snd := b₂✝ }
[PROOFSTEP]
right
[GOAL]
case mk.mk.mk.right.right.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ b₁ ≤ b₂✝
[PROOFSTEP]
apply le_trans
[GOAL]
case mk.mk.mk.right.right.a.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ b₁ ≤ ?mk.mk.mk.right.right.a.b
case mk.mk.mk.right.right.a.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ ?mk.mk.mk.right.right.a.b ≤ b₂✝
case mk.mk.mk.right.right.a.b
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ (fun i => α i) a₁
[PROOFSTEP]
repeat' assumption
[GOAL]
case mk.mk.mk.right.right.a.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ b₁ ≤ ?mk.mk.mk.right.right.a.b
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.mk.right.right.a.a
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ b₂✝¹ ≤ b₂✝
[PROOFSTEP]
assumption
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
⊢ ∀ (a b : Σₗ' (i : ι), α i), a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
refine' fun a b => ⟨fun hab => ⟨hab.mono_right fun i a b => le_of_lt, _⟩, _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a b : Σₗ' (i : ι), α i
hab : a < b
⊢ ¬b ≤ a
[PROOFSTEP]
rintro (⟨i, a, hji⟩ | ⟨i, hba⟩)
[GOAL]
case refine'_1.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁✝ : ι
i : α a₁✝
a₂✝ : ι
a : α a₂✝
hji : a₁✝ < a₂✝
hab : { fst := a₂✝, snd := a } < { fst := a₁✝, snd := i }
⊢ False
[PROOFSTEP]
obtain ⟨_, _, hij⟩ | ⟨_, hab⟩ := hab
[GOAL]
case refine'_1.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hab : { fst := i, snd := b₂✝ } < { fst := i, snd := b₁✝ }
⊢ False
[PROOFSTEP]
obtain ⟨_, _, hij⟩ | ⟨_, hab⟩ := hab
[GOAL]
case refine'_1.left.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁✝ : ι
i : α a₁✝
a₂✝ : ι
a : α a₂✝
hji : a₁✝ < a₂✝
hij : a₂✝ < a₁✝
⊢ False
[PROOFSTEP]
exact hij.not_lt hji
[GOAL]
case refine'_1.left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁✝ : ι
i a : α a₁✝
hji : a₁✝ < a₁✝
hab : a < i
⊢ False
[PROOFSTEP]
exact lt_irrefl _ hji
[GOAL]
case refine'_1.right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hij : i < i
⊢ False
[PROOFSTEP]
exact lt_irrefl _ hij
[GOAL]
case refine'_1.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hab : b₂✝ < b₁✝
⊢ False
[PROOFSTEP]
exact hab.not_le hba
[GOAL]
case refine'_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a b : Σₗ' (i : ι), α i
⊢ a ≤ b ∧ ¬b ≤ a → a < b
[PROOFSTEP]
rintro ⟨⟨j, b, hij⟩ | ⟨i, hab⟩, hba⟩
[GOAL]
case refine'_2.intro.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
a₁✝ : ι
j : α a₁✝
a₂✝ : ι
b : α a₂✝
hij : a₁✝ < a₂✝
hba : ¬{ fst := a₂✝, snd := b } ≤ { fst := a₁✝, snd := j }
⊢ { fst := a₁✝, snd := j } < { fst := a₂✝, snd := b }
[PROOFSTEP]
exact Lex.left _ _ hij
[GOAL]
case refine'_2.intro.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
src✝¹ : LE (Σₗ' (i : ι), α i) := le
src✝ : LT (Σₗ' (i : ι), α i) := lt
i : ι
b₁✝ b₂✝ : α i
hab : b₁✝ ≤ b₂✝
hba : ¬{ fst := i, snd := b₂✝ } ≤ { fst := i, snd := b₁✝ }
⊢ { fst := i, snd := b₁✝ } < { fst := i, snd := b₂✝ }
[PROOFSTEP]
exact Lex.right _ (hab.lt_of_not_le fun h => hba <| Lex.right _ h)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
src✝ : Preorder (Σₗ' (i : ι), α i) := preorder
⊢ ∀ (a b : Σₗ' (i : ι), α i), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ (⟨_, _, hlt₁⟩ | ⟨_, hlt₁⟩) (⟨_, _, hlt₂⟩ | ⟨_, hlt₂⟩)
[GOAL]
case mk.mk.left.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
src✝ : Preorder (Σₗ' (i : ι), α i) := preorder
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
hlt₁ : a₁ < a₂
hlt₂ : a₂ < a₁
⊢ { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }
[PROOFSTEP]
exact (lt_irrefl a₁ <| hlt₁.trans hlt₂).elim
[GOAL]
case mk.mk.left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
src✝ : Preorder (Σₗ' (i : ι), α i) := preorder
a₁ : ι
b₁ b₂ : α a₁
hlt₁ : a₁ < a₁
hlt₂ : b₂ ≤ b₁
⊢ { fst := a₁, snd := b₁ } = { fst := a₁, snd := b₂ }
[PROOFSTEP]
exact (lt_irrefl a₁ hlt₁).elim
[GOAL]
case mk.mk.right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
src✝ : Preorder (Σₗ' (i : ι), α i) := preorder
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : a₁ < a₁
⊢ { fst := a₁, snd := b₁ } = { fst := a₁, snd := b₂✝ }
[PROOFSTEP]
exact (lt_irrefl a₁ hlt₂).elim
[GOAL]
case mk.mk.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
src✝ : Preorder (Σₗ' (i : ι), α i) := preorder
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : b₂✝ ≤ b₁
⊢ { fst := a₁, snd := b₁ } = { fst := a₁, snd := b₂✝ }
[PROOFSTEP]
rw [hlt₁.antisymm hlt₂]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
src✝ : PartialOrder (Σₗ' (i : ι), α i) := partialOrder
⊢ ∀ (a b : Σₗ' (i : ι), α i), a ≤ b ∨ b ≤ a
[PROOFSTEP]
rintro ⟨i, a⟩ ⟨j, b⟩
[GOAL]
case mk.mk
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
src✝ : PartialOrder (Σₗ' (i : ι), α i) := partialOrder
i : ι
a : α i
j : ι
b : α j
⊢ { fst := i, snd := a } ≤ { fst := j, snd := b } ∨ { fst := j, snd := b } ≤ { fst := i, snd := a }
[PROOFSTEP]
obtain hij | rfl | hji := lt_trichotomy i j
[GOAL]
case mk.mk.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
src✝ : PartialOrder (Σₗ' (i : ι), α i) := partialOrder
i : ι
a : α i
j : ι
b : α j
hij : i < j
⊢ { fst := i, snd := a } ≤ { fst := j, snd := b } ∨ { fst := j, snd := b } ≤ { fst := i, snd := a }
[PROOFSTEP]
exact Or.inl (Lex.left _ _ hij)
[GOAL]
case mk.mk.inr.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
src✝ : PartialOrder (Σₗ' (i : ι), α i) := partialOrder
i : ι
a b : α i
⊢ { fst := i, snd := a } ≤ { fst := i, snd := b } ∨ { fst := i, snd := b } ≤ { fst := i, snd := a }
[PROOFSTEP]
obtain hab | hba := le_total a b
[GOAL]
case mk.mk.inr.inl.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
src✝ : PartialOrder (Σₗ' (i : ι), α i) := partialOrder
i : ι
a b : α i
hab : a ≤ b
⊢ { fst := i, snd := a } ≤ { fst := i, snd := b } ∨ { fst := i, snd := b } ≤ { fst := i, snd := a }
[PROOFSTEP]
exact Or.inl (Lex.right _ hab)
[GOAL]
case mk.mk.inr.inl.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
src✝ : PartialOrder (Σₗ' (i : ι), α i) := partialOrder
i : ι
a b : α i
hba : b ≤ a
⊢ { fst := i, snd := a } ≤ { fst := i, snd := b } ∨ { fst := i, snd := b } ≤ { fst := i, snd := a }
[PROOFSTEP]
exact Or.inr (Lex.right _ hba)
[GOAL]
case mk.mk.inr.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
src✝ : PartialOrder (Σₗ' (i : ι), α i) := partialOrder
i : ι
a : α i
j : ι
b : α j
hji : j < i
⊢ { fst := i, snd := a } ≤ { fst := j, snd := b } ∨ { fst := j, snd := b } ≤ { fst := i, snd := a }
[PROOFSTEP]
exact Or.inr (Lex.left _ _ hji)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
⊢ ⊥ ≤ { fst := a, snd := b }
[PROOFSTEP]
obtain rfl | ha := eq_bot_or_bot_lt a
[GOAL]
case inl
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ' (i : ι), α i
b : α ⊥
⊢ ⊥ ≤ { fst := ⊥, snd := b }
[PROOFSTEP]
exact Lex.right _ bot_le
[GOAL]
case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
ha : ⊥ < a
⊢ ⊥ ≤ { fst := a, snd := b }
[PROOFSTEP]
exact Lex.left _ _ ha
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
⊢ { fst := a, snd := b } ≤ ⊤
[PROOFSTEP]
obtain rfl | ha := eq_top_or_lt_top a
[GOAL]
case inl
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ' (i : ι), α i
b : α ⊤
⊢ { fst := ⊤, snd := b } ≤ ⊤
[PROOFSTEP]
exact Lex.right _ le_top
[GOAL]
case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
ha : a < ⊤
⊢ { fst := a, snd := b } ≤ ⊤
[PROOFSTEP]
exact Lex.left _ _ ha
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
⊢ ∀ (a₁ a₂ : Σₗ' (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
[PROOFSTEP]
rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | @⟨_, _, b, h⟩)
[GOAL]
case mk.mk.left
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
obtain ⟨k, hi, hj⟩ := exists_between h
[GOAL]
case mk.mk.left.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
k : ι
hi : i < k
hj : k < j
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
obtain ⟨c⟩ : Nonempty (α k) := inferInstance
[GOAL]
case mk.mk.left.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
k : ι
hi : i < k
hj : k < j
c : α k
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
exact ⟨⟨k, c⟩, left _ _ hi, left _ _ hj⟩
[GOAL]
case mk.mk.right
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
obtain ⟨c, ha, hb⟩ := exists_between h
[GOAL]
case mk.mk.right.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
⊢ ∀ (a₁ a₂ : Σₗ' (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
[PROOFSTEP]
rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | @⟨_, _, b, h⟩)
[GOAL]
case mk.mk.left
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
obtain ⟨c, ha⟩ := exists_gt a
[GOAL]
case mk.mk.left.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
c : α i
ha : a < c
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
exact ⟨⟨i, c⟩, right _ ha, left _ _ h⟩
[GOAL]
case mk.mk.right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
obtain ⟨c, ha, hb⟩ := exists_between h
[GOAL]
case mk.mk.right.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
⊢ ∀ (a₁ a₂ : Σₗ' (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
[PROOFSTEP]
rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | @⟨_, _, b, h⟩)
[GOAL]
case mk.mk.left
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
obtain ⟨c, hb⟩ := exists_lt b
[GOAL]
case mk.mk.left.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
c : α j
hb : c < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := j, snd := b }
[PROOFSTEP]
exact ⟨⟨j, c⟩, left _ _ h, right _ hb⟩
[GOAL]
case mk.mk.right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
obtain ⟨c, ha, hb⟩ := exists_between h
[GOAL]
case mk.mk.right.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, { fst := i, snd := a } < a_1 ∧ a_1 < { fst := i, snd := b }
[PROOFSTEP]
exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ ∀ (a : Σₗ' (i : ι), α i), ∃ b, a < b
[PROOFSTEP]
rintro ⟨i, a⟩
[GOAL]
case mk
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
⊢ ∃ b, { fst := i, snd := a } < b
[PROOFSTEP]
obtain ⟨j, h⟩ := exists_gt i
[GOAL]
case mk.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : i < j
⊢ ∃ b, { fst := i, snd := a } < b
[PROOFSTEP]
obtain ⟨b⟩ : Nonempty (α j) := inferInstance
[GOAL]
case mk.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : i < j
b : α j
⊢ ∃ b, { fst := i, snd := a } < b
[PROOFSTEP]
exact ⟨⟨j, b⟩, left _ _ h⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ ∀ (a : Σₗ' (i : ι), α i), ∃ b, b < a
[PROOFSTEP]
rintro ⟨i, a⟩
[GOAL]
case mk
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
⊢ ∃ b, b < { fst := i, snd := a }
[PROOFSTEP]
obtain ⟨j, h⟩ := exists_lt i
[GOAL]
case mk.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : j < i
⊢ ∃ b, b < { fst := i, snd := a }
[PROOFSTEP]
obtain ⟨b⟩ : Nonempty (α j) := inferInstance
[GOAL]
case mk.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : j < i
b : α j
⊢ ∃ b, b < { fst := i, snd := a }
[PROOFSTEP]
exact ⟨⟨j, b⟩, left _ _ h⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
⊢ ∀ (a : Σₗ' (i : ι), α i), ∃ b, a < b
[PROOFSTEP]
rintro ⟨i, a⟩
[GOAL]
case mk
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a : α i
⊢ ∃ b, { fst := i, snd := a } < b
[PROOFSTEP]
obtain ⟨b, h⟩ := exists_gt a
[GOAL]
case mk.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ b, { fst := i, snd := a } < b
[PROOFSTEP]
exact ⟨⟨i, b⟩, right _ h⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
⊢ ∀ (a : Σₗ' (i : ι), α i), ∃ b, b < a
[PROOFSTEP]
rintro ⟨i, a⟩
[GOAL]
case mk
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a : α i
⊢ ∃ b, b < { fst := i, snd := a }
[PROOFSTEP]
obtain ⟨b, h⟩ := exists_lt a
[GOAL]
case mk.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : b < a
⊢ ∃ b, b < { fst := i, snd := a }
[PROOFSTEP]
exact ⟨⟨i, b⟩, right _ h⟩
