[GOAL]
ι : Type u_1
α : ι → Type 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
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type 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
[PROOFSTEP]
rintro (⟨a, b, hij⟩ | ⟨a, b, hab⟩)
[GOAL]
case mp.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r i✝ 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
[PROOFSTEP]
exact Or.inl hij
[GOAL]
case mp.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
hab : s i✝ a b
⊢ r { fst := i✝, snd := a }.fst { fst := i✝, snd := b }.fst ∨
    ∃ h, s { fst := i✝, snd := b }.fst (h ▸ { fst := i✝, snd := a }.snd) { fst := i✝, snd := b }.snd
[PROOFSTEP]
exact Or.inr ⟨rfl, hab⟩
[GOAL]
case mpr
ι : Type u_1
α : ι → Type 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
[PROOFSTEP]
obtain ⟨i, a⟩ := a
[GOAL]
case mpr.mk
ι : Type u_1
α : ι → Type 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
[PROOFSTEP]
obtain ⟨j, b⟩ := b
[GOAL]
case mpr.mk.mk
ι : Type u_1
α : ι → Type 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 }
[PROOFSTEP]
dsimp only
[GOAL]
case mpr.mk.mk
ι : Type u_1
α : ι → Type 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 }
[PROOFSTEP]
rintro (h | ⟨rfl, h⟩)
[GOAL]
case mpr.mk.mk.inl
ι : Type u_1
α : ι → Type 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 }
[PROOFSTEP]
exact Lex.left _ _ h
[GOAL]
case mpr.mk.mk.inr.intro
ι : Type u_1
α : ι → Type 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 }
[PROOFSTEP]
exact Lex.right _ _ h
[GOAL]
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
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
[PROOFSTEP]
obtain ⟨a, b, hij⟩ | ⟨a, b, hab⟩ := h
[GOAL]
case left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r₁ i✝ j✝
⊢ Lex r₂ s₂ { fst := i✝, snd := a } { fst := j✝, snd := b }
[PROOFSTEP]
exact Lex.left _ _ (hr _ _ hij)
[GOAL]
case right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i✝ : ι
a b : α i✝
hab : s₁ i✝ a b
⊢ Lex r₂ s₂ { fst := i✝, snd := a } { fst := i✝, snd := b }
[PROOFSTEP]
exact Lex.right _ _ (hs _ _ _ hab)
[GOAL]
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex (Function.swap r) s a b ↔ Lex r (fun i => Function.swap (s i)) b a
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex (Function.swap r) s a b → Lex r (fun i => Function.swap (s i)) b a
[PROOFSTEP]
rintro (⟨a, b, h⟩ | ⟨a, b, h⟩)
[GOAL]
case mp.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 : Function.swap r i✝ j✝
⊢ Lex r (fun i => Function.swap (s i)) { fst := j✝, snd := b } { fst := i✝, snd := a }
case mp.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
h : s i✝ a b
⊢ Lex r (fun i => Function.swap (s i)) { fst := i✝, snd := b } { fst := i✝, snd := a }
[PROOFSTEP]
exacts [Lex.left _ _ h, Lex.right _ _ h]
[GOAL]
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
[PROOFSTEP]
rintro (⟨a, b, h⟩ | ⟨a, b, h⟩)
[GOAL]
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 }
[PROOFSTEP]
exacts [Lex.left _ _ h, Lex.right _ _ h]
[GOAL]
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : IsIrrefl ι r
inst✝ : ∀ (i : ι), IsIrrefl (α i) (s i)
⊢ ∀ (a : (i : ι) × α i), ¬Lex r s a a
[PROOFSTEP]
rintro _ (⟨a, b, hi⟩ | ⟨a, b, ha⟩)
[GOAL]
case left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b : (i : ι) × α i
inst✝¹ : IsIrrefl ι r
inst✝ : ∀ (i : ι), IsIrrefl (α i) (s i)
i✝ : ι
a : α i✝
hi : r i✝ i✝
⊢ False
[PROOFSTEP]
exact irrefl _ hi
[GOAL]
case right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b : (i : ι) × α i
inst✝¹ : IsIrrefl ι r
inst✝ : ∀ (i : ι), IsIrrefl (α i) (s i)
i✝ : ι
a : α i✝
ha : s i✝ a a
⊢ False
[PROOFSTEP]
exact irrefl _ ha
[GOAL]
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
⊢ ∀ (a b c : (i : ι) × α i), Lex r s a b → Lex r s b c → Lex r s a c
[PROOFSTEP]
rintro _ _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩) (⟨_, c, hk⟩ | ⟨_, c, hc⟩)
[GOAL]
case left.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ j✝¹ : ι
a : α i✝
b : α j✝¹
hij : r i✝ j✝¹
j✝ : ι
c : α j✝
hk : r j✝¹ j✝
⊢ Lex r s { fst := i✝, snd := a } { fst := j✝, snd := c }
[PROOFSTEP]
exact Lex.left _ _ (_root_.trans hij hk)
[GOAL]
case left.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r i✝ j✝
c : α j✝
hc : s j✝ b c
⊢ Lex r s { fst := i✝, snd := a } { fst := j✝, snd := c }
[PROOFSTEP]
exact Lex.left _ _ hij
[GOAL]
case right.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
j✝ : ι
c : α j✝
hk : r i✝ j✝
⊢ Lex r s { fst := i✝, snd := a } { fst := j✝, snd := c }
[PROOFSTEP]
exact Lex.left _ _ hk
[GOAL]
case right.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
c : α i✝
hc : s i✝ b c
⊢ Lex r s { fst := i✝, snd := a } { fst := i✝, snd := c }
[PROOFSTEP]
exact Lex.right _ _ (_root_.trans hab hc)
[GOAL]
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : IsSymm ι r
inst✝ : ∀ (i : ι), IsSymm (α i) (s i)
⊢ ∀ (a b : (i : ι) × α i), Lex r s a b → Lex r s b a
[PROOFSTEP]
rintro _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩)
[GOAL]
case left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsSymm ι r
inst✝ : ∀ (i : ι), IsSymm (α i) (s i)
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r i✝ j✝
⊢ Lex r s { fst := j✝, snd := b } { fst := i✝, snd := a }
[PROOFSTEP]
exact Lex.left _ _ (symm hij)
[GOAL]
case right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsSymm ι r
inst✝ : ∀ (i : ι), IsSymm (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
⊢ Lex r s { fst := i✝, snd := b } { fst := i✝, snd := a }
[PROOFSTEP]
exact Lex.right _ _ (symm hab)
[GOAL]
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : IsAsymm ι r
inst✝ : ∀ (i : ι), IsAntisymm (α i) (s i)
⊢ ∀ (a b : (i : ι) × α i), Lex r s a b → Lex r s b a → a = b
[PROOFSTEP]
rintro _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩) (⟨_, _, hji⟩ | ⟨_, _, hba⟩)
[GOAL]
case left.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsAsymm ι r
inst✝ : ∀ (i : ι), IsAntisymm (α i) (s i)
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r i✝ j✝
hji : r j✝ i✝
⊢ { fst := i✝, snd := a } = { fst := j✝, snd := b }
[PROOFSTEP]
exact (asymm hij hji).elim
[GOAL]
case left.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsAsymm ι r
inst✝ : ∀ (i : ι), IsAntisymm (α i) (s i)
i✝ : ι
a b : α i✝
hij : r i✝ i✝
hba : s i✝ b a
⊢ { fst := i✝, snd := a } = { fst := i✝, snd := b }
[PROOFSTEP]
exact (irrefl _ hij).elim
[GOAL]
case right.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsAsymm ι r
inst✝ : ∀ (i : ι), IsAntisymm (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
hji : r i✝ i✝
⊢ { fst := i✝, snd := a } = { fst := i✝, snd := b }
[PROOFSTEP]
exact (irrefl _ hji).elim
[GOAL]
case right.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsAsymm ι r
inst✝ : ∀ (i : ι), IsAntisymm (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
hba : s i✝ b a
⊢ { fst := i✝, snd := a } = { fst := i✝, snd := b }
[PROOFSTEP]
exact ext rfl (heq_of_eq $ antisymm hab hba)
[GOAL]
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTotal (α i) (s i)
⊢ ∀ (a b : (i : ι) × α i), Lex r s a b ∨ Lex r s b a
[PROOFSTEP]
rintro ⟨i, a⟩ ⟨j, b⟩
[GOAL]
case mk.mk
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTotal (α i) (s i)
i : ι
a : α i
j : ι
b : α j
⊢ Lex r s { fst := i, snd := a } { fst := j, snd := b } ∨ Lex r s { fst := j, snd := b } { fst := i, snd := a }
[PROOFSTEP]
obtain hij | rfl | hji := trichotomous_of r i j
[GOAL]
case mk.mk.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTotal (α i) (s i)
i : ι
a : α i
j : ι
b : α j
hij : r i j
⊢ Lex r s { fst := i, snd := a } { fst := j, snd := b } ∨ Lex r s { fst := j, snd := b } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inl (Lex.left _ _ hij)
[GOAL]
case mk.mk.inr.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTotal (α i) (s i)
i : ι
a b : α i
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := b } ∨ Lex r s { fst := i, snd := b } { fst := i, snd := a }
[PROOFSTEP]
obtain hab | hba := total_of (s i) a b
[GOAL]
case mk.mk.inr.inl.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTotal (α i) (s i)
i : ι
a b : α i
hab : s i a b
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := b } ∨ Lex r s { fst := i, snd := b } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inl (Lex.right _ _ hab)
[GOAL]
case mk.mk.inr.inl.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTotal (α i) (s i)
i : ι
a b : α i
hba : s i b a
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := b } ∨ Lex r s { fst := i, snd := b } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inr (Lex.right _ _ hba)
[GOAL]
case mk.mk.inr.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTotal (α i) (s i)
i : ι
a : α i
j : ι
b : α j
hji : r j i
⊢ Lex r s { fst := i, snd := a } { fst := j, snd := b } ∨ Lex r s { fst := j, snd := b } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inr (Lex.left _ _ hji)
[GOAL]
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTrichotomous (α i) (s i)
⊢ ∀ (a b : (i : ι) × α i), Lex r s a b ∨ a = b ∨ Lex r s b a
[PROOFSTEP]
rintro ⟨i, a⟩ ⟨j, b⟩
[GOAL]
case mk.mk
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTrichotomous (α i) (s i)
i : ι
a : α i
j : ι
b : α j
⊢ Lex r s { fst := i, snd := a } { fst := j, snd := b } ∨
    { fst := i, snd := a } = { fst := j, snd := b } ∨ Lex r s { fst := j, snd := b } { fst := i, snd := a }
[PROOFSTEP]
obtain hij | rfl | hji := trichotomous_of r i j
[GOAL]
case mk.mk.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTrichotomous (α i) (s i)
i : ι
a : α i
j : ι
b : α j
hij : r i j
⊢ Lex r s { fst := i, snd := a } { fst := j, snd := b } ∨
    { fst := i, snd := a } = { fst := j, snd := b } ∨ Lex r s { fst := j, snd := b } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inl (Lex.left _ _ hij)
[GOAL]
case mk.mk.inr.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTrichotomous (α i) (s i)
i : ι
a b : α i
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := b } ∨
    { fst := i, snd := a } = { fst := i, snd := b } ∨ Lex r s { fst := i, snd := b } { fst := i, snd := a }
[PROOFSTEP]
obtain hab | rfl | hba := trichotomous_of (s i) a b
[GOAL]
case mk.mk.inr.inl.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTrichotomous (α i) (s i)
i : ι
a b : α i
hab : s i a b
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := b } ∨
    { fst := i, snd := a } = { fst := i, snd := b } ∨ Lex r s { fst := i, snd := b } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inl (Lex.right _ _ hab)
[GOAL]
case mk.mk.inr.inl.inr.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTrichotomous (α i) (s i)
i : ι
a : α i
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := a } ∨
    { fst := i, snd := a } = { fst := i, snd := a } ∨ Lex r s { fst := i, snd := a } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inr (Or.inl rfl)
[GOAL]
case mk.mk.inr.inl.inr.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTrichotomous (α i) (s i)
i : ι
a b : α i
hba : s i b a
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := b } ∨
    { fst := i, snd := a } = { fst := i, snd := b } ∨ Lex r s { fst := i, snd := b } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inr (Or.inr $ Lex.right _ _ hba)
[GOAL]
case mk.mk.inr.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTrichotomous (α i) (s i)
i : ι
a : α i
j : ι
b : α j
hji : r j i
⊢ Lex r s { fst := i, snd := a } { fst := j, snd := b } ∨
    { fst := i, snd := a } = { fst := j, snd := b } ∨ Lex r s { fst := j, snd := b } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inr (Or.inr $ Lex.left _ _ hji)
[GOAL]
ι : 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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
rintro (⟨a, b, hij⟩ | ⟨i, hab⟩)
[GOAL]
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
[PROOFSTEP]
exact Or.inl hij
[GOAL]
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
[PROOFSTEP]
exact Or.inr ⟨rfl, hab⟩
[GOAL]
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
[PROOFSTEP]
obtain ⟨i, a⟩ := a
[GOAL]
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
[PROOFSTEP]
obtain ⟨j, b⟩ := b
[GOAL]
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 }
[PROOFSTEP]
dsimp only
[GOAL]
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 }
[PROOFSTEP]
rintro (h | ⟨rfl, h⟩)
[GOAL]
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 }
[PROOFSTEP]
exact Lex.left _ _ h
[GOAL]
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 }
[PROOFSTEP]
exact Lex.right _ h
[GOAL]
ι : 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
[PROOFSTEP]
obtain ⟨a, b, hij⟩ | ⟨i, hab⟩ := h
[GOAL]
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 }
[PROOFSTEP]
exact Lex.left _ _ (hr _ _ hij)
[GOAL]
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₂✝ }
[PROOFSTEP]
exact Lex.right _ (hs _ _ _ hab)
