Theorem: Prod.Lex.le_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 [Prod.Lex.le_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 := @ne_of_lt _ _ x.1 y.1
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