case mpr.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i✝ j✝ : ι
a : α i✝
b : α j✝
h : r i✝ j✝
⊢ Lex (Function.swap r) s { fst := j✝, snd := b } { fst := i✝, snd := a }

case mpr.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
h : Function.swap (s i✝) a b
⊢ Lex (Function.swap r) s { fst := i✝, snd := b } { fst := i✝, snd := a }
case mpr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex r (fun i => Function.swap (s i)) b a → Lex (Function.swap r) s a b
rintro (⟨a, b, h⟩ | ⟨a, b, h⟩)
no goals
case mpr.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i✝ j✝ : ι
a : α i✝
b : α j✝
h : r i✝ j✝
⊢ Lex (Function.swap r) s { fst := j✝, snd := b } { fst := i✝, snd := a }

case mpr.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
h : Function.swap (s i✝) a b
⊢ Lex (Function.swap r) s { fst := i✝, snd := b } { fst := i✝, snd := a }
exacts [Lex.left _ _ h, Lex.right _ _ h]