Theorem: Misc.Prod.lex_def (LeanSAT/Util/Misc.lean)

State before:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
p q : α × β
h : Prod.Lex r s p q
⊢ r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
Tactic:
cases h <;> simp [*]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
p q : α × β
h✝ : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
a : α
b : β
c : α
d : β
e : (a, b).fst = (c, d).fst
h : s (a, b).snd (c, d).snd
⊢ Prod.Lex r s (a, b) (c, d)
Tactic:
subst e
State after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
p q : α × β
h✝ : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
a : α
b d : β
h : s (a, b).snd ((a, b).fst, d).snd
⊢ Prod.Lex r s (a, b) ((a, b).fst, d)

State before:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
p q : α × β
h✝ : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
a : α
b d : β
h : s (a, b).snd ((a, b).fst, d).snd
⊢ Prod.Lex r s (a, b) ((a, b).fst, d)
Tactic:
exact Prod.Lex.right _ h
State after:
no goals