awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₃ :
  ∀
    i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I),
    (↑x : I → Bool) i = true
i : I
hi : i ∈ (↑l.Tail : List I) ∧ SwapTrue o (↑x : I → Bool) i ≠ true
pos : False
⊢ Eq (α := ℤ) 0 1

Tactic:
exfalso
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₃ :
  ∀
    i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I),
    (↑x : I → Bool) i = true
i : I
hi : i ∈ (↑l.Tail : List I) ∧ SwapTrue o (↑x : I → Bool) i ≠ true
⊢ i ∈ (↑l.Tail : List I) ∧ (↑x : I → Bool) i ≠ true

Tactic:
rw [← hi' i hi.1] at hi

Premises used: And.left
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₃ :
  ∀
    i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I),
    (↑x : I → Bool) i = true
i : I
hi : i ∈ (↑l.Tail : List I) ∧ (↑x : I → Bool) i ≠ true
⊢ False

Tactic:
hi.2 (h₃ i hi.1)

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₃ :
  ∀
    i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I),
    (↑x : I → Bool) i = true
i : I
hi : i ∈ (↑l.Tail : List I) ∧ (↑x : I → Bool) i ≠ true
⊢ False

Tactic:
exact hi.2 (h₃ i hi.1)

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
⊢ (Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
      (Products.eval C (↑l : Products I)) =
    Products.eval (C' C ho) (↑l : Products I).Tail

Tactic:
have : Inhabited I := ⟨term I ho⟩
  Products.max_eq_eval _ _ _ _ (List.ne_nil_of_mem l.prop.2)
    (head!_eq_o_of_maxProducts _ hsC ho l)

Premises used: Profinite.NobelingProof.Products.max_eq_eval, List.ne_nil_of_mem, Profinite.NobelingProof.term, And.right, Subtype.prop, Subtype.val, Profinite.NobelingProof.GoodProducts.head!_eq_o_of_maxProducts, Inhabited.mk
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h :
  ∀ (l : (↑(MaxProducts C ho) : Type u)),
    Function.comp (β := LocallyConstant (↑C : Type u) ℤ)
        (⇑(Linear_CC' C hsC ho) : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
        (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I)) l =
      Products.eval (C' C ho) (↑l : Products I).Tail
⊢ Eq (α := (↑(MaxProducts C ho) : Type u) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
    (Function.comp (β := LocallyConstant (↑C : Type u) ℤ)
      (⇑(Linear_CC' C hsC ho) : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
      fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I))
    fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval (C' C ho) (↑l : Products I).Tail

Tactic:
ext1 l
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
⊢ Function.comp (β := LocallyConstant (↑C : Type u) ℤ)
      (⇑(Linear_CC' C hsC ho) : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
      (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I)) l =
    Products.eval (C' C ho) (↑l : Products I).Tail

Tactic:
max_eq_eval _ _ _ _

Premises used: Profinite.NobelingProof.GoodProducts.max_eq_eval
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
⊢ Function.comp (β := LocallyConstant (↑C : Type u) ℤ)
      (⇑(Linear_CC' C hsC ho) : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
      (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I)) l =
    Products.eval (C' C ho) (↑l : Products I).Tail

Tactic:
exact max_eq_eval _ _ _ _

Premises used: Profinite.NobelingProof.GoodProducts.max_eq_eval
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
have : ∀ (this : Inhabited I), List.IsChain (fun (x x_1 : I) ↦ x > x_1) (term I ho :: (↑q : List I))
⊢ List.IsChain (fun (x x_1 : I) ↦ x > x_1) (term I ho :: (↑q : List I))

Tactic:
have : Inhabited I := ⟨term I ho⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this : Inhabited I
rw : List.Pairwise (fun (x x_1 : I) ↦ x > x_1) (term I ho :: (↑q : List I))
⊢ List.IsChain (fun (x x_1 : I) ↦ x > x_1) (term I ho :: (↑q : List I))

Tactic:
rw [List.isChain_iff_pairwise]

Premises used: List.isChain_iff_pairwise
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this : Inhabited I
simp : (∀ a' ∈ (↑q : List I), a' < term I ho) ∧ List.Pairwise (fun (x x_1 : I) ↦ x_1 < x) (↑q : List I)
⊢ List.Pairwise (fun (x x_1 : I) ↦ x > x_1) (term I ho :: (↑q : List I))

Tactic:
simp only [gt_iff_lt, List.pairwise_cons]

Premises used: List.pairwise_cons, gt_iff_lt
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this : Inhabited I
⊢ (∀ a' ∈ (↑q : List I), a' < term I ho) ∧ List.Pairwise (fun (x x_1 : I) ↦ x_1 < x) (↑q : List I)

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

Premises used: lt_of_le_of_lt, Subtype.prop, And.intro, Iff.mp, Profinite.NobelingProof.Products.rel_head!_of_mem, List.isChain_iff_pairwise
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this : Inhabited I
refine : ∀ (a : I) (ha : a ∈ (↑q : List I)), (↑q : List I).head! < term I ho
⊢ (∀ a' ∈ (↑q : List I), a' < term I ho) ∧ List.Pairwise (fun (x x_1 : I) ↦ x_1 < x) (↑q : List I)

Tactic:
refine ⟨fun a ha ↦ lt_of_le_of_lt (Products.rel_head!_of_mem ha) ?_,
    List.isChain_iff_pairwise.mp q.prop⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this : Inhabited I
a : I
ha : a ∈ (↑q : List I)
⊢ (↑q : List I).head! < term I ho

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

Premises used: lt_of_le_of_lt, List.ne_nil_of_mem, Profinite.NobelingProof.Products.head!_le_of_lt
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this : Inhabited I
a : I
ha : a ∈ (↑q : List I)
refine : (↑(↑l : Products I).Tail : List I).head! < term I ho
⊢ (↑q : List I).head! < term I ho

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

Premises used: lt_of_le_of_lt, List.ne_nil_of_mem, Profinite.NobelingProof.Products.head!_le_of_lt
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this : Inhabited I
a : I
ha : a ∈ (↑q : List I)
pos : ∀ (hM : (↑(↑l : Products I).Tail : List I) = []), (↑(↑l : Products I).Tail : List I).head! < term I ho
neg : ∀ (hM : ¬(↑(↑l : Products I).Tail : List I) = []), (↑(↑l : Products I).Tail : List I).head! < term I ho
⊢ (↑(↑l : Products I).Tail : List I).head! < term I ho

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

Premises used: Profinite.NobelingProof.Products.Tail, Subtype.val
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this : Inhabited I
a : I
ha : a ∈ (↑q : List I)
hM : (↑(↑l : Products I).Tail : List I) = []
pos :
  ∀ (hq : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑q : List I) []) (this : Inhabited I) (a : I) (ha : a ∈ (↑q : List I))
    (hM : (↑(↑l : Products I).Tail : List I) = []), (↑(↑l : Products I).Tail : List I).head! < term I ho
⊢ (↑(↑l : Products I).Tail : List I).head! < term I ho

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

Premises used: Profinite.NobelingProof.Products.lt_iff_lex_lt
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑q : List I) []
this : Inhabited I
a : I
ha : a ∈ (↑q : List I)
hM : (↑(↑l : Products I).Tail : List I) = []
⊢ (↑(↑l : Products I).Tail : List I).head! < term I ho

Tactic:
simp only [List.not_lex_nil] at hq

Premises used: List.not_lex_nil
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this : Inhabited I
a : I
ha : a ∈ (↑q : List I)
hM : ¬(↑(↑l : Products I).Tail : List I) = []
⊢ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (↑(↑l : Products I) : List I)

Tactic:
have := l.val.prop
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this_1 : Inhabited I
a : I
ha : a ∈ (↑q : List I)
hM : ¬(↑(↑l : Products I).Tail : List I) = []
this : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (↑(↑l : Products I) : List I)
⊢ List.Pairwise (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑(↑l : Products I).Tail : List I))

Tactic:
rw [max_eq_o_cons_tail C hsC ho l, List.isChain_iff_pairwise] at this

Premises used: Profinite.NobelingProof.GoodProducts.max_eq_o_cons_tail, List.isChain_iff_pairwise
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this_1 : Inhabited I
a : I
ha : a ∈ (↑q : List I)
hM : ¬(↑(↑l : Products I).Tail : List I) = []
this : List.Pairwise (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑(↑l : Products I).Tail : List I))
⊢ (↑(↑l : Products I).Tail : List I).head! < term I ho

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

Premises used: List.head!_mem_self, List.rel_of_pairwise_cons
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this_1 : Inhabited I
a : I
ha : a ∈ (↑q : List I)
hM : ¬(↑(↑l : Products I).Tail : List I) = []
this : List.Pairwise (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑(↑l : Products I).Tail : List I))
⊢ (↑(↑l : Products I).Tail : List I).head! < term I ho

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

Premises used: List.head!_mem_self, List.rel_of_pairwise_cons
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
q : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)
l : (↑(MaxProducts C ho) : Type u)
have :
  ∀ (this : Inhabited I),
    List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑(↑q : Products I) : List I) (↑(↑l : Products I) : List I)
⊢ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑(↑q : Products I) : List I) (↑(↑l : Products I) : List I)

Tactic:
have : Inhabited I := ⟨term I ho⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
q : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)
l : (↑(MaxProducts C ho) : Type u)
this : Inhabited I
pos :
  ∀ (h : (↑(↑q : Products I) : List I) = []),
    List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑(↑q : Products I) : List I) (↑(↑l : Products I) : List I)
neg :
  ∀ (h : ¬(↑(↑q : Products I) : List I) = []),
    List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑(↑q : Products I) : List I) (↑(↑l : Products I) : List I)
⊢ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑(↑q : Products I) : List I) (↑(↑l : Products I) : List I)

Tactic:
by_cases h : q.val.val = []

Premises used: Subtype.val
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
q : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)
l : (↑(MaxProducts C ho) : Type u)
this : Inhabited I
h : (↑(↑q : Products I) : List I) = []
pos : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) [] (term I ho :: (↑(↑l : Products I).Tail : List I))
⊢ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑(↑q : Products I) : List I) (↑(↑l : Products I) : List I)

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

Premises used: Profinite.NobelingProof.GoodProducts.max_eq_o_cons_tail
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
q : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)
l : (↑(MaxProducts C ho) : Type u)
this : Inhabited I
h : (↑(↑q : Products I) : List I) = []
⊢ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) [] (term I ho :: (↑(↑l : Products I).Tail : List I))

Tactic:
List.Lex.nil

Premises used: List.Lex.nil
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
q : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)
l : (↑(MaxProducts C ho) : Type u)
this : Inhabited I
h : (↑(↑q : Products I) : List I) = []
⊢ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) [] (term I ho :: (↑(↑l : Products I).Tail : List I))

Tactic:
exact List.Lex.nil

Premises used: List.Lex.nil
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
q : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)
l : (↑(MaxProducts C ho) : Type u)
this : Inhabited I
h : ¬(↑(↑q : Products I) : List I) = []
neg :
  List.Lex (fun (x1 x2 : I) ↦ x1 < x2) ((↑(↑q : Products I) : List I).head! :: (↑(↑q : Products I) : List I).tail)
    (term I ho :: (↑(↑l : Products I).Tail : List I))
⊢ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑(↑q : Products I) : List I) (↑(↑l : Products I) : List I)

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

Premises used: List.cons_head!_tail, Profinite.NobelingProof.GoodProducts.max_eq_o_cons_tail
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
q : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)
l : (↑(MaxProducts C ho) : Type u)
this : Inhabited I
h : ¬(↑(↑q : Products I) : List I) = []
neg : (↑(↑q : Products I) : List I).head! < term I ho
⊢ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) ((↑(↑q : Products I) : List I).head! :: (↑(↑q : Products I) : List I).tail)
    (term I ho :: (↑(↑l : Products I).Tail : List I))

Tactic:
apply List.Lex.rel

Premises used: List.Lex.rel
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
q : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)
l : (↑(MaxProducts C ho) : Type u)
this : Inhabited I
h : ¬(↑(↑q : Products I) : List I) = []
neg :
  LT.lt (α := Ordinal.{u})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : I) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : I) ↦ x1 < x2) :
          (a : I) → Ordinal.{u})
        (↑(↑q : Products I) : List I).head! :
      Ordinal.{u})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : I) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : I) ↦ x1 < x2) :
          (a : I) → Ordinal.{u})
        (term I ho) :
      Ordinal.{u})
⊢ (↑(↑q : Products I) : List I).head! < term I ho

Tactic:
rw [← Ordinal.typein_lt_typein (· < ·)]

Premises used: Ordinal.typein_lt_typein, LT.lt
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
q : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)
l : (↑(MaxProducts C ho) : Type u)
this : Inhabited I
h : ¬(↑(↑q : Products I) : List I) = []
neg :
  (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : I) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
          (Ordinal.typein fun (x1 x2 : I) ↦ x1 < x2) :
        (a : I) → Ordinal.{u})
      (↑(↑q : Products I) : List I).head! <
    o
⊢ LT.lt (α := Ordinal.{u})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : I) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : I) ↦ x1 < x2) :
          (a : I) → Ordinal.{u})
        (↑(↑q : Products I) : List I).head! :
      Ordinal.{u})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : I) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : I) ↦ x1 < x2) :
          (a : I) → Ordinal.{u})
        (term I ho) :
      Ordinal.{u})

Tactic:
simp only [term, Ordinal.typein_enum]

Premises used: Profinite.NobelingProof.term, Ordinal.typein_enum