case inl
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : a = b
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a

case inr
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : a ≠ b
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
cases' eq_or_ne a b with hab hab
no goals
case inl
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : a = b
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
exact Or.inr (Or.inl hab)
case inr
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
case inr
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : a ≠ b
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
rw [Function.ne_iff] at hab
case inr
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
case inr
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
let i := wf.min _ hab
case inr
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
hri : ∀ (j : ι), r j i → a j = b j
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
case inr
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
have hri : ∀ j, r j i → a j = b j := by
  intro j
  rw [← not_imp_not]
  exact fun h' => wf.not_lt_min _ _ h'
case inr
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
hri : ∀ (j : ι), r j i → a j = b j
hne : a i ≠ b i
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
case inr
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
hri : ∀ (j : ι), r j i → a j = b j
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
have hne : a i ≠ b i := wf.min_mem _ hab
case inr.inl
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
hri : ∀ (j : ι), r j i → a j = b j
hne : a i ≠ b i
hi : s (a i) (b i)
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a

case inr.inr
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
hri : ∀ (j : ι), r j i → a j = b j
hne : a i ≠ b i
hi : a i = b i ∨ s (b i) (a i)
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
case inr
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
hri : ∀ (j : ι), r j i → a j = b j
hne : a i ≠ b i
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
cases' trichotomous_of s (a i) (b i) with hi hi
no goals
case inr.inl
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
hri : ∀ (j : ι), r j i → a j = b j
hne : a i ≠ b i
hi : s (a i) (b i)
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a

case inr.inr
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
hri : ∀ (j : ι), r j i → a j = b j
hne : a i ≠ b i
hi : a i = b i ∨ s (b i) (a i)
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a
exacts [Or.inl ⟨i, hri, hi⟩,
  Or.inr <| Or.inr <| ⟨i, fun j hj => (hri j hj).symm, hi.resolve_left hne⟩]
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
j : ι
⊢ r j i → a j = b j
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
⊢ ∀ (j : ι), r j i → a j = b j
intro j
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
j : ι
⊢ ¬a j = b j → ¬r j i
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
j : ι
⊢ r j i → a j = b j
rw [← not_imp_not]
no goals
ι : Type u_2
β : ι → Type u_1
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), IsTrichotomous (β i) s
wf : WellFounded r
a b : (i : ι) → β i
hab : ∃ a_1, a a_1 ≠ b a_1
i : ι := WellFounded.min wf (fun x => a x = b x → False) hab
j : ι
⊢ ¬a j = b j → ¬r j i
exact fun h' => wf.not_lt_min _ _ h'