-- Mathlib/Data/Sigma/Lex.lean
theorem lex_iff {a b : Σ' i, α i} :
    Lex r s a b ↔ r a.1 b.1 ∨ ∃ h : a.1 = b.1, s b.1 (h.rec a.2) b.2

Proof state:
case mp
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
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

Tactic:
rintro (⟨a, b, hij⟩ | ⟨i, hab⟩)

Result:
case mp.left
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a₁✝ : ι
a : α a₁✝
a₂✝ : ι
b : α a₂✝
hij : r a₁✝ a₂✝
⊢ r ⟨a₁✝, a⟩.fst ⟨a₂✝, b⟩.fst ∨ ∃ h, s ⟨a₂✝, b⟩.fst (h ▸ ⟨a₁✝, a⟩.snd) ⟨a₂✝, b⟩.snd

case mp.right
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
b₁✝ b₂✝ : α i
hab : s i b₁✝ b₂✝
⊢ r ⟨i, b₁✝⟩.fst ⟨i, b₂✝⟩.fst ∨ ∃ h, s ⟨i, b₂✝⟩.fst (h ▸ ⟨i, b₁✝⟩.snd) ⟨i, b₂✝⟩.snd

Proof state:
case mp.left
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a₁✝ : ι
a : α a₁✝
a₂✝ : ι
b : α a₂✝
hij : r a₁✝ a₂✝
⊢ r ⟨a₁✝, a⟩.fst ⟨a₂✝, b⟩.fst ∨ ∃ h, s ⟨a₂✝, b⟩.fst (h ▸ ⟨a₁✝, a⟩.snd) ⟨a₂✝, b⟩.snd

Tactic:
exact Or.inl hij

Result:
no goals

Proof state:
case mpr.mk.mk
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
⊢ (r ⟨i, a⟩.fst ⟨j, b⟩.fst ∨ ∃ h, s ⟨j, b⟩.fst (h ▸ ⟨i, a⟩.snd) ⟨j, b⟩.snd) → Lex r s ⟨i, a⟩ ⟨j, b⟩

Tactic:
dsimp only

Result:
case mpr.mk.mk
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
⊢ (r i j ∨ ∃ h, s j (h ▸ a) b) → Lex r s ⟨i, a⟩ ⟨j, b⟩

Proof state:
case mpr.mk.mk.inl
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
h : r i j
⊢ Lex r s ⟨i, a⟩ ⟨j, b⟩

Tactic:
exact Lex.left _ _ h

Result:
no goals

Proof state:
case mpr.mk
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) ×' α i
i : ι
a : α i
⊢ (r ⟨i, a⟩.fst b.fst ∨ ∃ h, s b.fst (h ▸ ⟨i, a⟩.snd) b.snd) → Lex r s ⟨i, a⟩ b

Tactic:
obtain ⟨j, b⟩ := b

Result:
case mpr.mk.mk
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
⊢ (r ⟨i, a⟩.fst ⟨j, b⟩.fst ∨ ∃ h, s ⟨j, b⟩.fst (h ▸ ⟨i, a⟩.snd) ⟨j, b⟩.snd) → Lex r s ⟨i, a⟩ ⟨j, b⟩

Proof state:
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
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

Tactic:
constructor

Result:
case mp
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
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 : ι → ι → Prop
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

Proof state:
case mpr.mk.mk.inr.intro
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
a b : α i
h : s i (⋯ ▸ a) b
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩

Tactic:
exact Lex.right _ h

Result:
no goals

Proof state:
case mpr
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
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

Tactic:
obtain ⟨i, a⟩ := a

Result:
case mpr.mk
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) ×' α i
i : ι
a : α i
⊢ (r ⟨i, a⟩.fst b.fst ∨ ∃ h, s b.fst (h ▸ ⟨i, a⟩.snd) b.snd) → Lex r s ⟨i, a⟩ b

Proof state:
case mpr.mk.mk
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
⊢ (r i j ∨ ∃ h, s j (h ▸ a) b) → Lex r s ⟨i, a⟩ ⟨j, b⟩

Tactic:
rintro (h | ⟨rfl, h⟩)

Result:
case mpr.mk.mk.inl
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
h : r i j
⊢ Lex r s ⟨i, a⟩ ⟨j, b⟩

case mpr.mk.mk.inr.intro
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
a b : α i
h : s i (⋯ ▸ a) b
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩

Proof state:
case mp.right
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
b₁✝ b₂✝ : α i
hab : s i b₁✝ b₂✝
⊢ r ⟨i, b₁✝⟩.fst ⟨i, b₂✝⟩.fst ∨ ∃ h, s ⟨i, b₂✝⟩.fst (h ▸ ⟨i, b₁✝⟩.snd) ⟨i, b₂✝⟩.snd

Tactic:
exact Or.inr ⟨rfl, hab⟩

Result:
no goals