-- Mathlib/Order/PiLex.lean
theorem isTrichotomous_lex [∀ i, IsTrichotomous (β i) s] (wf : WellFounded r) :
    IsTrichotomous (∀ i, β i) (Pi.Lex r @s) :=
  { trichotomous := fun a b => by
      rcases eq_or_ne a b with hab | hab
      · exact Or.inr (Or.inl hab)
      · rw [Function.ne_iff] at hab
        let i := wf.min _ hab
        have hri : ∀ j, r j i → a j = b j

Proof state:
case inr
ι : Type u_1
β : ι → Type u_2
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 : ι := wf.min (fun x => a x = b x → False) hab
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a

Tactic:
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'

Result:
case inr
ι : Type u_1
β : ι → Type u_2
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 : ι := wf.min (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

Proof state:
ι : Type u_1
β : ι → Type u_2
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

Tactic:
rcases eq_or_ne a b with hab | hab

Result:
case inl
ι : Type u_1
β : ι → Type u_2
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_1
β : ι → Type u_2
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

Proof state:
case inr
ι : Type u_1
β : ι → Type u_2
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

Tactic:
let i := wf.min _ hab

Result:
case inr
ι : Type u_1
β : ι → Type u_2
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 : ι := wf.min (fun x => a x = b x → False) hab
⊢ Pi.Lex r s a b ∨ a = b ∨ Pi.Lex r s b a

Proof state:
case inr.inl
ι : Type u_1
β : ι → Type u_2
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 : ι := wf.min (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_1
β : ι → Type u_2
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 : ι := wf.min (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

Tactic:
exacts [Or.inl ⟨i, hri, hi⟩,
  Or.inr <| Or.inr <| ⟨i, fun j hj => (hri j hj).symm, hi.resolve_left hne⟩]

Result:
no goals

Proof state:
ι : Type u_1
β : ι → Type u_2
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 : ι := wf.min (fun x => a x = b x → False) hab
j : ι
⊢ r j i → a j = b j

Tactic:
rw [← not_imp_not]

Result:
ι : Type u_1
β : ι → Type u_2
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 : ι := wf.min (fun x => a x = b x → False) hab
j : ι
⊢ ¬a j = b j → ¬r j i

Proof state:
case inl
ι : Type u_1
β : ι → Type u_2
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

Tactic:
exact Or.inr (Or.inl hab)

Result:
no goals

Proof state:
case inr
ι : Type u_1
β : ι → Type u_2
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

Tactic:
rw [Function.ne_iff] at hab

Result:
case inr
ι : Type u_1
β : ι → Type u_2
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

Proof state:
ι : Type u_1
β : ι → Type u_2
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 : ι := wf.min (fun x => a x = b x → False) hab
j : ι
⊢ ¬a j = b j → ¬r j i

Tactic:
exact fun h' => wf.not_lt_min _ _ h'

Result:
no goals

Proof state:
ι : Type u_1
β : ι → Type u_2
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 : ι := wf.min (fun x => a x = b x → False) hab
⊢ ∀ (j : ι), r j i → a j = b j

Tactic:
intro j

Result:
ι : Type u_1
β : ι → Type u_2
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 : ι := wf.min (fun x => a x = b x → False) hab
j : ι
⊢ r j i → a j = b j

Proof state:
case inr
ι : Type u_1
β : ι → Type u_2
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 : ι := wf.min (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

Tactic:
have hne : a i ≠ b i := wf.min_mem _ hab

Result:
case inr
ι : Type u_1
β : ι → Type u_2
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 : ι := wf.min (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

Proof state:
case inr
ι : Type u_1
β : ι → Type u_2
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 : ι := wf.min (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

Tactic:
rcases trichotomous_of s (a i) (b i) with hi | hi

Result:
case inr.inl
ι : Type u_1
β : ι → Type u_2
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 : ι := wf.min (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_1
β : ι → Type u_2
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 : ι := wf.min (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