-- Mathlib/Data/Sigma/Lex.lean
theorem lex_iff : 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.left
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r i✝ j✝
⊢ r ⟨i✝, a⟩.fst ⟨j✝, b⟩.fst ∨ ∃ h, s ⟨j✝, b⟩.fst (h ▸ ⟨i✝, a⟩.snd) ⟨j✝, b⟩.snd

Tactic:
exact Or.inl hij

Result:
no goals

Proof state:
case mpr.mk.mk.inl
ι : Type u_1
α : ι → Type 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.mk
ι : Type u_1
α : ι → Type 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
ι : Type u_1
α : ι → Type 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
ι : Type u_1
α : ι → Type 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 mpr.mk
ι : Type u_1
α : ι → Type 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
ι : Type u_1
α : ι → Type 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:
ι : Type u_1
α : ι → Type 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
ι : Type u_1
α : ι → Type 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
ι : Type u_1
α : ι → Type 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
ι : Type u_1
α : ι → Type 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
ι : Type u_1
α : ι → Type 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
ι : Type u_1
α : ι → Type 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
ι : Type u_1
α : ι → Type 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.inr.intro
ι : Type u_1
α : ι → Type 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 mp
ι : Type u_1
α : ι → Type 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⟩ | ⟨a, b, hab⟩)

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

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

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

Tactic:
exact Or.inr ⟨rfl, hab⟩

Result:
no goals