case left
ι : Sort u_1
α : ι → Sort u_2
r r₁✝ r₂✝ : ι → ι → Prop
s s₁✝ s₂✝ : (i : ι) → α i → α i → Prop
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a₁✝ : ι
a : α a₁✝
a₂✝ : ι
b : α a₂✝
hij : r₁ a₁✝ a₂✝
⊢ Lex r₂ s₂ { fst := a₁✝, snd := a } { fst := a₂✝, snd := b }

case right
ι : Sort u_1
α : ι → Sort u_2
r r₁✝ r₂✝ : ι → ι → Prop
s s₁✝ s₂✝ : (i : ι) → α i → α i → Prop
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i : ι
b₁✝ b₂✝ : α i
hab : s₁ i b₁✝ b₂✝
⊢ Lex r₂ s₂ { fst := i, snd := b₁✝ } { fst := i, snd := b₂✝ }
ι : Sort u_1
α : ι → Sort u_2
r r₁✝ r₂✝ : ι → ι → Prop
s s₁✝ s₂✝ : (i : ι) → α i → α i → Prop
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a b : (i : ι) ×' α i
h : Lex r₁ s₁ a b
⊢ Lex r₂ s₂ a b
obtain ⟨a, b, hij⟩ | ⟨i, hab⟩ := h
no goals
case left
ι : Sort u_1
α : ι → Sort u_2
r r₁✝ r₂✝ : ι → ι → Prop
s s₁✝ s₂✝ : (i : ι) → α i → α i → Prop
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a₁✝ : ι
a : α a₁✝
a₂✝ : ι
b : α a₂✝
hij : r₁ a₁✝ a₂✝
⊢ Lex r₂ s₂ { fst := a₁✝, snd := a } { fst := a₂✝, snd := b }
exact Lex.left _ _ (hr _ _ hij)
no goals
case right
ι : Sort u_1
α : ι → Sort u_2
r r₁✝ r₂✝ : ι → ι → Prop
s s₁✝ s₂✝ : (i : ι) → α i → α i → Prop
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i : ι
b₁✝ b₂✝ : α i
hab : s₁ i b₁✝ b₂✝
⊢ Lex r₂ s₂ { fst := i, snd := b₁✝ } { fst := i, snd := b₂✝ }
exact Lex.right _ (hs _ _ _ hab)