Theorem: Prod.Lex.fst_lt_of_lt_of_le (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : PartialOrder β
x y : Lex (α × β)
h : x < y
h' : y.2 ≤ x.2
⊢ x.1 < y.1
Tactic:
rw [Prod.Lex.lt_iff'] at h
State after:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : PartialOrder β
x y : Lex (α × β)
h : x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2
h' : y.2 ≤ x.2
⊢ x.1 < y.1

State before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : PartialOrder β
x y : Lex (α × β)
h : x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2
h' : y.2 ≤ x.2
⊢ x.1 < y.1
Tactic:
cases h with
| inl h => exact h
| inr h => cases h.2.not_le h'
State after:
no goals

State before:
case inl
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : PartialOrder β
x y : Lex (α × β)
h' : y.2 ≤ x.2
h : x.1 < y.1
⊢ x.1 < y.1
Tactic:
exact h
State after:
no goals

State before:
case inr
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : Preorder α
inst✝ : PartialOrder β
x y : Lex (α × β)
h' : y.2 ≤ x.2
h : x.1 = y.1 ∧ x.2 < y.2
⊢ x.1 < y.1
Tactic:
cases h.2.not_le h'
State after:
no goals