no goals
α : Type u_1
β : Type u_2
γ : Type ?u.5817
δ : Type ?u.5820
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
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
cases h <;> simp [*]
α : Type u_1
β : Type u_2
γ : Type ?u.5817
δ : Type ?u.5820
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
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)
α : Type u_1
β : Type u_2
γ : Type ?u.5817
δ : Type ?u.5820
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
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)
subst e
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.5817
δ : Type ?u.5820
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
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)
exact Lex.right _ h