-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem chain'_cons_of_lt (l : MaxProducts C ho)
    (q : Products I) (hq : q < l.val.Tail) :
    List.Chain' (fun x x_1 ↦ x > x_1) (term I ho :: q.val)

Proof state:
case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : List.Lex (fun x1 x2 => x1 < x2) ↑q []
this : Inhabited I
a : I
ha : a ∈ ↑q
hM : ↑(↑l).Tail = []
⊢ (↑(↑l).Tail).head! < term I ho

Tactic:
simp only [List.not_lex_nil] at hq

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
⊢ List.Chain' (fun x x_1 => x > x_1) (term I ho :: ↑q)

Tactic:
rw [List.chain'_iff_pairwise]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
⊢ List.Pairwise (fun x x_1 => x > x_1) (term I ho :: ↑q)

Proof state:
case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
a : I
ha : a ∈ ↑q
hM : ↑(↑l).Tail = []
⊢ (↑(↑l).Tail).head! < term I ho

Tactic:
rw [Products.lt_iff_lex_lt, hM] at hq

Result:
case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : List.Lex (fun x1 x2 => x1 < x2) ↑q []
this : Inhabited I
a : I
ha : a ∈ ↑q
hM : ↑(↑l).Tail = []
⊢ (↑(↑l).Tail).head! < term I ho

Proof state:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this✝ : Inhabited I
a : I
ha : a ∈ ↑q
hM : ¬↑(↑l).Tail = []
this : List.Pairwise (fun x1 x2 => x1 > x2) (term I ho :: ↑(↑l).Tail)
⊢ (↑(↑l).Tail).head! < term I ho

Tactic:
exact List.rel_of_pairwise_cons this (List.head!_mem_self hM)

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
⊢ List.Chain' (fun x x_1 => x > x_1) (term I ho :: ↑q)

Tactic:
have : Inhabited I := ⟨term I ho⟩

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
⊢ List.Chain' (fun x x_1 => x > x_1) (term I ho :: ↑q)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
a : I
ha : a ∈ ↑q
⊢ (↑(↑l).Tail).head! < term I ho

Tactic:
by_cases hM : l.val.Tail.val = []

Result:
case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
a : I
ha : a ∈ ↑q
hM : ↑(↑l).Tail = []
⊢ (↑(↑l).Tail).head! < term I ho

case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
a : I
ha : a ∈ ↑q
hM : ¬↑(↑l).Tail = []
⊢ (↑(↑l).Tail).head! < term I ho

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
⊢ (∀ a' ∈ ↑q, a' < term I ho) ∧ List.Pairwise (fun x x_1 => x_1 < x) ↑q

Tactic:
refine ⟨fun a ha ↦ lt_of_le_of_lt (Products.rel_head!_of_mem ha) ?_,
  List.chain'_iff_pairwise.mp q.prop⟩

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
a : I
ha : a ∈ ↑q
⊢ (↑q).head! < term I ho

Proof state:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
a : I
ha : a ∈ ↑q
hM : ¬↑(↑l).Tail = []
⊢ (↑(↑l).Tail).head! < term I ho

Tactic:
have := l.val.prop

Result:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this✝ : Inhabited I
a : I
ha : a ∈ ↑q
hM : ¬↑(↑l).Tail = []
this : List.Chain' (fun x1 x2 => x1 > x2) ↑↑l
⊢ (↑(↑l).Tail).head! < term I ho

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
⊢ List.Pairwise (fun x x_1 => x > x_1) (term I ho :: ↑q)

Tactic:
simp only [gt_iff_lt, List.pairwise_cons]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
⊢ (∀ a' ∈ ↑q, a' < term I ho) ∧ List.Pairwise (fun x x_1 => x_1 < x) ↑q

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
a : I
ha : a ∈ ↑q
⊢ (↑q).head! < term I ho

Tactic:
refine lt_of_le_of_lt (Products.head!_le_of_lt hq (q.val.ne_nil_of_mem ha)) ?_

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
a : I
ha : a ∈ ↑q
⊢ (↑(↑l).Tail).head! < term I ho

Proof state:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this✝ : Inhabited I
a : I
ha : a ∈ ↑q
hM : ¬↑(↑l).Tail = []
this : List.Chain' (fun x1 x2 => x1 > x2) ↑↑l
⊢ (↑(↑l).Tail).head! < term I ho

Tactic:
rw [max_eq_o_cons_tail C hsC ho l, List.chain'_iff_pairwise] at this

Result:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this✝ : Inhabited I
a : I
ha : a ∈ ↑q
hM : ¬↑(↑l).Tail = []
this : List.Pairwise (fun x1 x2 => x1 > x2) (term I ho :: ↑(↑l).Tail)
⊢ (↑(↑l).Tail).head! < term I ho