-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem good_lt_maxProducts (q : GoodProducts (π C (ord I · < o)))
    (l : MaxProducts C ho) : List.Lex (· < ·) q.val.val l.val.val

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
q : ↑(GoodProducts (π C fun x => ord I x < o))
l : ↑(MaxProducts C ho)
⊢ List.Lex (fun x1 x2 => x1 < x2) ↑↑q ↑↑l

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
q : ↑(GoodProducts (π C fun x => ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
⊢ List.Lex (fun x1 x2 => x1 < x2) ↑↑q ↑↑l

Proof state:
case neg.h
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
q : ↑(GoodProducts (π C fun x => ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ¬↑↑q = []
⊢ (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding (↑↑q).head! < o

Tactic:
exact Products.prop_of_isGood C _ q.prop q.val.val.head! (List.head!_mem_self h)

Result:
no goals

Proof state:
case neg.h
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
q : ↑(GoodProducts (π C fun x => ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ¬↑↑q = []
⊢ (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding (↑↑q).head! <
    (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding (term I ho)

Tactic:
simp only [term, Ordinal.typein_enum]

Result:
case neg.h
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
q : ↑(GoodProducts (π C fun x => ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ¬↑↑q = []
⊢ (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding (↑↑q).head! < o

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
q : ↑(GoodProducts (π C fun x => ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ↑↑q = []
⊢ List.Lex (fun x1 x2 => x1 < x2) [] (term I ho :: ↑(↑l).Tail)

Tactic:
exact List.Lex.nil

Result:
no goals

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
q : ↑(GoodProducts (π C fun x => ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ¬↑↑q = []
⊢ List.Lex (fun x1 x2 => x1 < x2) ((↑↑q).head! :: (↑↑q).tail) (term I ho :: ↑(↑l).Tail)

Tactic:
apply List.Lex.rel

Result:
case neg.h
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
q : ↑(GoodProducts (π C fun x => ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ¬↑↑q = []
⊢ (↑↑q).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
q : ↑(GoodProducts (π C fun x => ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
⊢ List.Lex (fun x1 x2 => x1 < x2) ↑↑q ↑↑l

Tactic:
by_cases h : q.val.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
q : ↑(GoodProducts (π C fun x => ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ↑↑q = []
⊢ List.Lex (fun x1 x2 => x1 < x2) ↑↑q ↑↑l

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
q : ↑(GoodProducts (π C fun x => ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ¬↑↑q = []
⊢ List.Lex (fun x1 x2 => x1 < x2) ↑↑q ↑↑l

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
q : ↑(GoodProducts (π C fun x => ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ↑↑q = []
⊢ List.Lex (fun x1 x2 => x1 < x2) ↑↑q ↑↑l

Tactic:
rw [h, max_eq_o_cons_tail C hsC ho l]

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
q : ↑(GoodProducts (π C fun x => ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ↑↑q = []
⊢ List.Lex (fun x1 x2 => x1 < x2) [] (term I ho :: ↑(↑l).Tail)

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
q : ↑(GoodProducts (π C fun x => ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ¬↑↑q = []
⊢ List.Lex (fun x1 x2 => x1 < x2) ↑↑q ↑↑l

Tactic:
rw [← List.cons_head!_tail h, max_eq_o_cons_tail C hsC ho l]

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
q : ↑(GoodProducts (π C fun x => ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ¬↑↑q = []
⊢ List.Lex (fun x1 x2 => x1 < x2) ((↑↑q).head! :: (↑↑q).tail) (term I ho :: ↑(↑l).Tail)