Theorem: Prod.Lex.lt_iff'' (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✝¹ : PartialOrder α
inst✝ : Preorder β
x y : Lex (α × β)
⊢ x < y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)
Tactic:
rw [lt_iff', le_iff_lt_or_eq]
State after:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : Lex (α × β)
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 ↔ (x.1 < y.1 ∨ x.1 = y.1) ∧ (x.1 = y.1 → x.2 < y.2)

State before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : Lex (α × β)
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 ↔ (x.1 < y.1 ∨ x.1 = y.1) ∧ (x.1 = y.1 → x.2 < y.2)
Tactic:
have : x.1 < y.1 → ¬x.1 = y.1 := ne_of_lt
State after:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : Lex (α × β)
this : x.1 < y.1 → ¬x.1 = y.1
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 ↔ (x.1 < y.1 ∨ x.1 = y.1) ∧ (x.1 = y.1 → x.2 < y.2)

State before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : Lex (α × β)
this : x.1 < y.1 → ¬x.1 = y.1
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 ↔ (x.1 < y.1 ∨ x.1 = y.1) ∧ (x.1 = y.1 → x.2 < y.2)
Tactic:
tauto
State after:
no goals