ι : Type ?u.48700
α : Type u
β : Type v
γ : Type w
δ : Type u_1
π : ι → Type ?u.48714
r : α → α → Prop
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g b).fst < (Prod.map f g a).fst ∧ (Prod.map f g b).snd ≤ (Prod.map f g a).snd ∨
      (Prod.map f g b).fst ≤ (Prod.map f g a).fst ∧ (Prod.map f g b).snd < (Prod.map f g a).snd
ι : Type ?u.48700
α : Type u
β : Type v
γ : Type w
δ : Type u_1
π : ι → Type ?u.48714
r : α → α → Prop
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
⊢ a < b → Prod.map f g b < Prod.map f g a
simp only [Prod.lt_iff]
no goals
ι : Type ?u.48700
α : Type u
β : Type v
γ : Type w
δ : Type u_1
π : ι → Type ?u.48714
r : α → α → Prop
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g b).fst < (Prod.map f g a).fst ∧ (Prod.map f g b).snd ≤ (Prod.map f g a).snd ∨
      (Prod.map f g b).fst ≤ (Prod.map f g a).fst ∧ (Prod.map f g b).snd < (Prod.map f g a).snd
exact Or.imp (And.imp hf.imp hg.antitone.imp) (And.imp hf.antitone.imp hg.imp)