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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : (↑m.support : Set (Products I)) ⊆ {m : Products I | m < (↑l : Products I).Tail}
hmsum :
  Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ)
    (m.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (C' C ho) i : LocallyConstant (↑(C' 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)) :
      LocallyConstant (↑(C' C ho) : Type u) ℤ)
hse :
  LinearMap.range (M := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) (πs C o) =
    (Linear_CC' C hsC ho).ker
n : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
w : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l } →₀ ℤ
hn :
  HAdd.hAdd (α := LocallyConstant (↑C : Type u) ℤ)
      (w.sum fun (a : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) (b : ℤ) ↦
        (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          (b • eval (π C fun (x : I) ↦ ord I x < o) a))
      (m.sum fun (i : Products I) (a : ℤ) ↦ a • (List.map (e C) (term I ho :: (↑i : List I))).prod) =
    Products.eval C (↑l : Products I)
hc :
  (w.sum fun (i : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) (a : ℤ) ↦
      a • eval (π C fun (x : I) ↦ ord I x < o) i) =
    n
q : Products I
hq : q ∈ m.support
⊢ (List.map (e C) (term I ho :: (↑q : List I))).prod ∈
    Set.image (α := Products I) (Products.eval C) {m : Products I | m < (↑l : Products I)}

Tactic:
⟨⟨term I ho :: q.val, isChain_cons_of_lt C hsC ho l q (hmmem hq)⟩, ⟨?_, rfl⟩⟩

Premises used: Set.Mem, setOf, Profinite.NobelingProof.term, List.cons, Subtype.mk, And.intro, Exists.intro, Set.image, Profinite.NobelingProof.GoodProducts.isChain_cons_of_lt, Subtype.val, rfl
-- 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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : (↑m.support : Set (Products I)) ⊆ {m : Products I | m < (↑l : Products I).Tail}
hmsum :
  Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ)
    (m.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (C' C ho) i : LocallyConstant (↑(C' 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)) :
      LocallyConstant (↑(C' C ho) : Type u) ℤ)
hse :
  LinearMap.range (M := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) (πs C o) =
    (Linear_CC' C hsC ho).ker
n : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
w : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l } →₀ ℤ
hn :
  HAdd.hAdd (α := LocallyConstant (↑C : Type u) ℤ)
      (w.sum fun (a : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) (b : ℤ) ↦
        (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          (b • eval (π C fun (x : I) ↦ ord I x < o) a))
      (m.sum fun (i : Products I) (a : ℤ) ↦ a • (List.map (e C) (term I ho :: (↑i : List I))).prod) =
    Products.eval C (↑l : Products I)
hc :
  (w.sum fun (i : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) (a : ℤ) ↦
      a • eval (π C fun (x : I) ↦ ord I x < o) i) =
    n
q : Products I
hq : q ∈ m.support
h₂ :
  Membership.mem (γ := Set (Products I)) {m : Products I | m < (↑l : Products I)}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) (term I ho :: (↑q : List I)) ⋯)
⊢ (List.map (e C) (term I ho :: (↑q : List I))).prod ∈
    Set.image (α := Products I) (Products.eval C) {m : Products I | m < (↑l : Products I)}

Tactic:
refine ⟨⟨term I ho :: q.val, isChain_cons_of_lt C hsC ho l q (hmmem hq)⟩, ⟨?_, rfl⟩⟩
-- 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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : (↑m.support : Set (Products I)) ⊆ {m : Products I | m < (↑l : Products I).Tail}
hmsum :
  Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ)
    (m.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (C' C ho) i : LocallyConstant (↑(C' 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)) :
      LocallyConstant (↑(C' C ho) : Type u) ℤ)
hse :
  LinearMap.range (M := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) (πs C o) =
    (Linear_CC' C hsC ho).ker
n : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
w : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l } →₀ ℤ
hn :
  HAdd.hAdd (α := LocallyConstant (↑C : Type u) ℤ)
      (w.sum fun (a : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) (b : ℤ) ↦
        (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          (b • eval (π C fun (x : I) ↦ ord I x < o) a))
      (m.sum fun (i : Products I) (a : ℤ) ↦ a • (List.map (e C) (term I ho :: (↑i : List I))).prod) =
    Products.eval C (↑l : Products I)
hc :
  (w.sum fun (i : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) (a : ℤ) ↦
      a • eval (π C fun (x : I) ↦ ord I x < o) i) =
    n
q : Products I
hq : q ∈ m.support
h₂ : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (term I ho :: (↑q : List I)) (↑(↑l : Products I) : List I)
⊢ Membership.mem (γ := Set (Products I)) {m : Products I | m < (↑l : Products I)}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) (term I ho :: (↑q : List I)) ⋯)

Tactic:
simp only [Products.lt_iff_lex_lt, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, 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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : (↑m.support : Set (Products I)) ⊆ {m : Products I | m < (↑l : Products I).Tail}
hmsum :
  Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ)
    (m.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (C' C ho) i : LocallyConstant (↑(C' 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)) :
      LocallyConstant (↑(C' C ho) : Type u) ℤ)
hse :
  LinearMap.range (M := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) (πs C o) =
    (Linear_CC' C hsC ho).ker
n : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
w : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l } →₀ ℤ
hn :
  HAdd.hAdd (α := LocallyConstant (↑C : Type u) ℤ)
      (w.sum fun (a : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) (b : ℤ) ↦
        (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          (b • eval (π C fun (x : I) ↦ ord I x < o) a))
      (m.sum fun (i : Products I) (a : ℤ) ↦ a • (List.map (e C) (term I ho :: (↑i : List I))).prod) =
    Products.eval C (↑l : Products I)
hc :
  (w.sum fun (i : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) (a : ℤ) ↦
      a • eval (π C fun (x : I) ↦ ord I x < o) i) =
    n
q : Products I
hq : q ∈ m.support
h₂ : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (term I ho :: (↑q : List I)) (term I ho :: (↑(↑l : Products I).Tail : List I))
⊢ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (term I ho :: (↑q : List I)) (↑(↑l : Products I) : List I)

Tactic:
rw [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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : (↑m.support : Set (Products I)) ⊆ {m : Products I | m < (↑l : Products I).Tail}
hmsum :
  Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ)
    (m.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (C' C ho) i : LocallyConstant (↑(C' 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)) :
      LocallyConstant (↑(C' C ho) : Type u) ℤ)
hse :
  LinearMap.range (M := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) (πs C o) =
    (Linear_CC' C hsC ho).ker
n : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
w : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l } →₀ ℤ
hn :
  HAdd.hAdd (α := LocallyConstant (↑C : Type u) ℤ)
      (w.sum fun (a : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) (b : ℤ) ↦
        (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          (b • eval (π C fun (x : I) ↦ ord I x < o) a))
      (m.sum fun (i : Products I) (a : ℤ) ↦ a • (List.map (e C) (term I ho :: (↑i : List I))).prod) =
    Products.eval C (↑l : Products I)
hc :
  (w.sum fun (i : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) (a : ℤ) ↦
      a • eval (π C fun (x : I) ↦ ord I x < o) i) =
    n
q : Products I
hq : q ∈ m.support
⊢ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (term I ho :: (↑q : List I)) (term I ho :: (↑(↑l : Products I).Tail : List I))

Tactic:
List.Lex.cons ((Products.lt_iff_lex_lt q l.val.Tail).mp (hmmem hq))

Premises used: Profinite.NobelingProof.Products.lt_iff_lex_lt, Iff.mp, Profinite.NobelingProof.Products.Tail, Subtype.val, List.Lex.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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : (↑m.support : Set (Products I)) ⊆ {m : Products I | m < (↑l : Products I).Tail}
hmsum :
  Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ)
    (m.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (C' C ho) i : LocallyConstant (↑(C' 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)) :
      LocallyConstant (↑(C' C ho) : Type u) ℤ)
hse :
  LinearMap.range (M := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) (πs C o) =
    (Linear_CC' C hsC ho).ker
n : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
w : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l } →₀ ℤ
hn :
  HAdd.hAdd (α := LocallyConstant (↑C : Type u) ℤ)
      (w.sum fun (a : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) (b : ℤ) ↦
        (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          (b • eval (π C fun (x : I) ↦ ord I x < o) a))
      (m.sum fun (i : Products I) (a : ℤ) ↦ a • (List.map (e C) (term I ho :: (↑i : List I))).prod) =
    Products.eval C (↑l : Products I)
hc :
  (w.sum fun (i : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) (a : ℤ) ↦
      a • eval (π C fun (x : I) ↦ ord I x < o) i) =
    n
q : Products I
hq : q ∈ m.support
⊢ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (term I ho :: (↑q : List I)) (term I ho :: (↑(↑l : Products I).Tail : List I))

Tactic:
exact List.Lex.cons ((Products.lt_iff_lex_lt q l.val.Tail).mp (hmmem hq))

Premises used: Profinite.NobelingProof.Products.lt_iff_lex_lt, Iff.mp, Profinite.NobelingProof.Products.Tail, Subtype.val, List.Lex.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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
m n : (↑(MaxProducts C ho) : Type u)
h : MaxToGood C hC hsC ho h₁ m = MaxToGood C hC hsC ho h₁ n
apply :
  (↑(↑m : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I) =
    (↑(↑n : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I)
⊢ m = n

Tactic:
apply Subtype.ext ∘ Subtype.ext

Premises used: Subtype.ext
-- 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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
m n : (↑(MaxProducts C ho) : Type u)
h : MaxToGood C hC hsC ho h₁ m = MaxToGood C hC hsC ho h₁ n
⊢ (↑(MaxToGood C hC hsC ho h₁ m) : Products I) = (↑(MaxToGood C hC hsC ho h₁ n) : Products I)

Tactic:
rw [Subtype.ext_iff] at h

Premises used: Subtype.ext_iff
-- 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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
m n : (↑(MaxProducts C ho) : Type u)
h : (↑m : Products I).Tail = (↑n : Products I).Tail
rw :
  term I ho :: (↑(↑m : Products I).Tail : List I) =
    (↑(↑n : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I)
rw₁ : term I ho :: (↑(↑m : Products I).Tail : List I) = term I ho :: (↑(↑n : Products I).Tail : List I)
rw₂ rw₃ : term I ho :: (↑(↑n : Products I).Tail : List I) = term I ho :: (↑(↑n : Products I).Tail : List I)
⊢ (↑(↑m : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I) =
    (↑(↑n : { x : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x }) : List I)

Tactic:
rw [max_eq_o_cons_tail C hsC ho m, max_eq_o_cons_tail C hsC ho n, h]

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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
rw :
  LinearIndependent (ι := { l : Products I // Products.isGood (C' C ho) l }) ℤ (eval (C' C ho)) →
    LinearIndependent ℤ (M := LocallyConstant (↑(C' C ho) : Type u) ℤ) fun (l : (↑(MaxProducts C ho) : Type u)) ↦
      Products.eval (C' C ho) (↑l : Products I).Tail
⊢ LinearIndependent (ι := { l : Products I // Products.isGood (C' C ho) l }) ℤ (eval (C' C ho)) →
    LinearIndependent (ι := (↑(MaxProducts C ho) : Type u)) ℤ (M := 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))

Tactic:
rw [max_eq_eval_unapply C hsC ho]

Premises used: Profinite.NobelingProof.GoodProducts.max_eq_eval_unapply
-- 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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
h : LinearIndependent (ι := { l : Products I // Products.isGood (C' C ho) l }) ℤ (eval (C' C ho))
f : (↑(MaxProducts C ho) : Type u) → (↑(GoodProducts (C' C ho)) : Type u) := MaxToGood C hC hsC ho h₁
⊢ Function.Injective f

Tactic:
have hf : f.Injective := maxToGood_injective C hC hsC ho h₁
-- 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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
h : LinearIndependent (ι := { l : Products I // Products.isGood (C' C ho) l }) ℤ (eval (C' C ho))
f : (↑(MaxProducts C ho) : Type u) → (↑(GoodProducts (C' C ho)) : Type u) := MaxToGood C hC hsC ho h₁
hf : Function.Injective f
⊢ (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval (C' C ho) (↑l : Products I).Tail) = eval (C' C ho) ∘ f

Tactic:
have hh : (fun l ↦ Products.eval (C' C ho) l.val.Tail) = eval (C' C ho) ∘ f := rfl
-- 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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
h : LinearIndependent (ι := { l : Products I // Products.isGood (C' C ho) l }) ℤ (eval (C' C ho))
f : (↑(MaxProducts C ho) : Type u) → (↑(GoodProducts (C' C ho)) : Type u) := MaxToGood C hC hsC ho h₁
hf : Function.Injective f
hh : (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval (C' C ho) (↑l : Products I).Tail) = eval (C' C ho) ∘ f
rw : LinearIndependent ℤ (eval (C' C ho) ∘ f)
⊢ LinearIndependent ℤ (M := LocallyConstant (↑(C' C ho) : Type u) ℤ) fun (l : (↑(MaxProducts C ho) : Type u)) ↦
    Products.eval (C' C ho) (↑l : Products I).Tail

Tactic:
rw [hh]
-- 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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
h : LinearIndependent (ι := { l : Products I // Products.isGood (C' C ho) l }) ℤ (eval (C' C ho))
f : (↑(MaxProducts C ho) : Type u) → (↑(GoodProducts (C' C ho)) : Type u) := MaxToGood C hC hsC ho h₁
hf : Function.Injective f
hh : (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval (C' C ho) (↑l : Products I).Tail) = eval (C' C ho) ∘ f
⊢ LinearIndependent ℤ (eval (C' C ho) ∘ f)

Tactic:
h.comp f hf

Premises used: LinearIndependent.comp
-- 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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
h : LinearIndependent (ι := { l : Products I // Products.isGood (C' C ho) l }) ℤ (eval (C' C ho))
f : (↑(MaxProducts C ho) : Type u) → (↑(GoodProducts (C' C ho)) : Type u) := MaxToGood C hC hsC ho h₁
hf : Function.Injective f
hh : (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval (C' C ho) (↑l : Products I).Tail) = eval (C' C ho) ∘ f
⊢ LinearIndependent ℤ (eval (C' C ho) ∘ f)

Tactic:
exact h.comp f hf

Premises used: LinearIndependent.comp
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
⊢ Subsingleton.{max 1 (u + 1)} (LocallyConstant (↑∅ : Type u) ℤ)

Tactic:
subsingleton_iff.mpr (fun _ _ ↦ LocallyConstant.ext isEmptyElim)

Premises used: Iff.mpr, subsingleton_iff, isEmptyElim, LocallyConstant.ext