case mp
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ Lex r s a b → r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd

case mpr
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ (r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd) → Lex r s a b
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ Lex r s a b ↔ r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd
constructor
case mp.left
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a₁✝ : ι
a : α a₁✝
a₂✝ : ι
b : α a₂✝
hij : r a₁✝ a₂✝
⊢ r { fst := a₁✝, snd := a }.fst { fst := a₂✝, snd := b }.fst ∨
    ∃ h, s { fst := a₂✝, snd := b }.fst (h ▸ { fst := a₁✝, snd := a }.snd) { fst := a₂✝, snd := b }.snd

case mp.right
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
b₁✝ b₂✝ : α i
hab : s i b₁✝ b₂✝
⊢ r { fst := i, snd := b₁✝ }.fst { fst := i, snd := b₂✝ }.fst ∨
    ∃ h, s { fst := i, snd := b₂✝ }.fst (h ▸ { fst := i, snd := b₁✝ }.snd) { fst := i, snd := b₂✝ }.snd
case mp
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ Lex r s a b → r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd
rintro (⟨a, b, hij⟩ | ⟨i, hab⟩)
no goals
case mp.left
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a₁✝ : ι
a : α a₁✝
a₂✝ : ι
b : α a₂✝
hij : r a₁✝ a₂✝
⊢ r { fst := a₁✝, snd := a }.fst { fst := a₂✝, snd := b }.fst ∨
    ∃ h, s { fst := a₂✝, snd := b }.fst (h ▸ { fst := a₁✝, snd := a }.snd) { fst := a₂✝, snd := b }.snd
exact Or.inl hij
no goals
case mp.right
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
b₁✝ b₂✝ : α i
hab : s i b₁✝ b₂✝
⊢ r { fst := i, snd := b₁✝ }.fst { fst := i, snd := b₂✝ }.fst ∨
    ∃ h, s { fst := i, snd := b₂✝ }.fst (h ▸ { fst := i, snd := b₁✝ }.snd) { fst := i, snd := b₂✝ }.snd
exact Or.inr ⟨rfl, hab⟩
case mpr.mk
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
b : (i : ι) ×' α i
i : ι
a : α i
⊢ (r { fst := i, snd := a }.fst b.fst ∨ ∃ h, s b.fst (h ▸ { fst := i, snd := a }.snd) b.snd) →
    Lex r s { fst := i, snd := a } b
case mpr
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ (r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd) → Lex r s a b
obtain ⟨i, a⟩ := a
case mpr.mk.mk
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
⊢ (r { fst := i, snd := a }.fst { fst := j, snd := b }.fst ∨
      ∃ h, s { fst := j, snd := b }.fst (h ▸ { fst := i, snd := a }.snd) { fst := j, snd := b }.snd) →
    Lex r s { fst := i, snd := a } { fst := j, snd := b }
case mpr.mk
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
b : (i : ι) ×' α i
i : ι
a : α i
⊢ (r { fst := i, snd := a }.fst b.fst ∨ ∃ h, s b.fst (h ▸ { fst := i, snd := a }.snd) b.snd) →
    Lex r s { fst := i, snd := a } b
obtain ⟨j, b⟩ := b
case mpr.mk.mk
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
⊢ (r i j ∨ ∃ h, s j (h ▸ a) b) → Lex r s { fst := i, snd := a } { fst := j, snd := b }
case mpr.mk.mk
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
⊢ (r { fst := i, snd := a }.fst { fst := j, snd := b }.fst ∨
      ∃ h, s { fst := j, snd := b }.fst (h ▸ { fst := i, snd := a }.snd) { fst := j, snd := b }.snd) →
    Lex r s { fst := i, snd := a } { fst := j, snd := b }
dsimp only
case mpr.mk.mk.inl
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
h : r i j
⊢ Lex r s { fst := i, snd := a } { fst := j, snd := b }

case mpr.mk.mk.inr.intro
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
a b : α i
h : s i ((_ : i = i) ▸ a) b
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := b }
case mpr.mk.mk
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
⊢ (r i j ∨ ∃ h, s j (h ▸ a) b) → Lex r s { fst := i, snd := a } { fst := j, snd := b }
rintro (h | ⟨rfl, h⟩)
no goals
case mpr.mk.mk.inl
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
h : r i j
⊢ Lex r s { fst := i, snd := a } { fst := j, snd := b }
exact Lex.left _ _ h
no goals
case mpr.mk.mk.inr.intro
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
a b : α i
h : s i ((_ : i = i) ▸ a) b
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := b }
exact Lex.right _ h