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
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) = []
⊢ (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

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

Premises used: List.head!_mem_self, List.head!, Profinite.NobelingProof.Products.prop_of_isGood, Subtype.prop, 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) = []
⊢ (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

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

Premises used: List.head!_mem_self, List.head!, Profinite.NobelingProof.Products.prop_of_isGood, Subtype.prop, 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}
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))))
have : ∀ (this : Inhabited I), Products.isGood (C' C ho) (↑l : Products I).Tail
⊢ Products.isGood (C' C ho) (↑l : Products I).Tail

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}
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
h :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (C' C ho)) {m : Products I | m < (↑l : Products I).Tail}))
    (Products.eval (C' C ho) (↑l : Products I).Tail)
⊢ ∃ (l_1 : Products I →₀ ℤ),
    Membership.mem (γ := Submodule ℤ (Products I →₀ ℤ))
        (Finsupp.supported ℤ ℤ {m : Products I | m < (↑l : Products I).Tail}) l_1 ∧
      Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ)
        ((Finsupp.linearCombination ℤ (Products.eval (C' C ho)) :
              (a : Products I →₀ ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
            l_1 :
          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) ℤ)

Tactic:
rw [Finsupp.mem_span_image_iff_linearCombination, ← max_eq_eval C hsC ho] at h

Premises used: Finsupp.mem_span_image_iff_linearCombination, 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}
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
h :
  ∃ (l_1 : Products I →₀ ℤ),
    Membership.mem (γ := Submodule ℤ (Products I →₀ ℤ))
        (Finsupp.supported ℤ ℤ {m : Products I | m < (↑l : Products I).Tail}) l_1 ∧
      Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ)
        ((Finsupp.linearCombination ℤ (Products.eval (C' C ho)) :
              (a : Products I →₀ ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
            l_1 :
          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) ℤ)
obtain :
  ∀ (m : Products I →₀ ℤ)
    (hmmem :
      Membership.mem (γ := Submodule ℤ (Products I →₀ ℤ))
        (Finsupp.supported ℤ ℤ {m : Products I | m < (↑l : Products I).Tail}) m)
    (hmsum :
      Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ)
        ((Finsupp.linearCombination ℤ (Products.eval (C' C ho)) :
              (a : Products I →₀ ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
            m :
          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) ℤ)),
    False
⊢ False

Tactic:
obtain ⟨m, ⟨hmmem, hmsum⟩⟩ := 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
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 :
  Membership.mem (γ := Submodule ℤ (Products I →₀ ℤ))
    (Finsupp.supported ℤ ℤ {m : Products I | m < (↑l : Products I).Tail}) m
hmsum :
  Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ)
    ((Finsupp.linearCombination ℤ (Products.eval (C' C ho)) :
          (a : Products I →₀ ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
        m :
      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) ℤ)
⊢ 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) ℤ)

Tactic:
rw [Finsupp.linearCombination_apply] at hmsum

Premises used: Finsupp.linearCombination_apply
-- 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 :
  Membership.mem (γ := Submodule ℤ (Products I →₀ ℤ))
    (Finsupp.supported ℤ ℤ {m : Products I | m < (↑l : Products I).Tail}) m
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) ℤ)
rw :
  Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ) (m.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (C' C ho) i)
    ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
      (m.sum fun (i : Products I) (a : ℤ) ↦ a • (List.map (e C) (term I ho :: (↑i : List I))).prod))
⊢ Eq (α := 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) ℤ)
    ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
        (m.sum fun (i : Products I) (a : ℤ) ↦ a • (List.map (e C) (term I ho :: (↑i : List I))).prod) :
      LocallyConstant (↑(C' C ho) : Type u) ℤ)

Tactic:
rw [← hmsum]
-- 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 :
  Membership.mem (γ := Submodule ℤ (Products I →₀ ℤ))
    (Finsupp.supported ℤ ℤ {m : Products I | m < (↑l : Products I).Tail}) m
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) ℤ)
simp :
  Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ) (m.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (C' C ho) i)
    (m.sum fun (a : Products I) (b : ℤ) ↦
      (Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
        (b • (List.map (e C) (term I ho :: (↑a : List I))).prod))
⊢ Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ) (m.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (C' C ho) i)
    ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
      (m.sum fun (i : Products I) (a : ℤ) ↦ a • (List.map (e C) (term I ho :: (↑i : List I))).prod))

Tactic:
simp only [map_finsuppSum]

Premises used: map_finsuppSum
-- 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 :
  Membership.mem (γ := Submodule ℤ (Products I →₀ ℤ))
    (Finsupp.supported ℤ ℤ {m : Products I | m < (↑l : Products I).Tail}) m
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) ℤ)
h :
  ∀ x ∈ m.support,
    HSMul.hSMul (α := ℤ) ((m : (a : Products I) → ℤ) x : ℤ) (Products.eval (C' C ho) x) =
      (Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
        (HSMul.hSMul (α := ℤ) ((m : (a : Products I) → ℤ) x : ℤ) (List.map (e C) (term I ho :: (↑x : List I))).prod)
⊢ Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ) (m.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (C' C ho) i)
    (m.sum fun (a : Products I) (b : ℤ) ↦
      (Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
        (b • (List.map (e C) (term I ho :: (↑a : List I))).prod))

Tactic:
apply Finsupp.sum_congr

Premises used: Finsupp.sum_congr
-- 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 :
  Membership.mem (γ := Submodule ℤ (Products I →₀ ℤ))
    (Finsupp.supported ℤ ℤ {m : Products I | m < (↑l : Products I).Tail}) m
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) ℤ)
q : Products I
hq : q ∈ m.support
h :
  HSMul.hSMul (α := ℤ) ((m : (a : Products I) → ℤ) q : ℤ) (Products.eval (C' C ho) q) =
    HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) q : ℤ)
      ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          (List.map (e C) (term I ho :: (↑q : List I))).prod :
        LocallyConstant (↑(C' C ho) : Type u) ℤ)
⊢ HSMul.hSMul (α := ℤ) ((m : (a : Products I) → ℤ) q : ℤ) (Products.eval (C' C ho) q) =
    (Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
      (HSMul.hSMul (α := ℤ) ((m : (a : Products I) → ℤ) q : ℤ) (List.map (e C) (term I ho :: (↑q : List I))).prod)

Tactic:
rw [map_smul]

Premises used: map_smul
-- 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 :
  Membership.mem (γ := Submodule ℤ (Products I →₀ ℤ))
    (Finsupp.supported ℤ ℤ {m : Products I | m < (↑l : Products I).Tail}) m
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) ℤ)
q : Products I
hq : q ∈ m.support
h :
  ∀ (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) ℤ))
    (q : Products I) (hq : q ∈ m.support),
    HSMul.hSMul (α := ℤ) ((m : (a : Products I) → ℤ) q : ℤ) (Products.eval (C' C ho) q) =
      HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) q : ℤ)
        ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
            (List.map (e C) (term I ho :: (↑q : List I))).prod :
          LocallyConstant (↑(C' C ho) : Type u) ℤ)
⊢ HSMul.hSMul (α := ℤ) ((m : (a : Products I) → ℤ) q : ℤ) (Products.eval (C' C ho) q) =
    HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) q : ℤ)
      ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          (List.map (e C) (term I ho :: (↑q : List I))).prod :
        LocallyConstant (↑(C' C ho) : Type u) ℤ)

Tactic:
rw [Finsupp.mem_supported] at hmmem

Premises used: Finsupp.mem_supported
-- 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) ℤ)
q : Products I
hq : q ∈ m.support
⊢ q < (↑l : Products I).Tail

Tactic:
have hx'' : q < l.val.Tail := hmmem hq
-- 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) ℤ)
q : Products I
hq : q ∈ m.support
hx'' : q < (↑l : Products I).Tail
⊢ (↑(Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) (term I ho :: (↑q : List I)) ⋯) :
        List I).head! =
    term I ho

Tactic:
simp only [List.head!_cons]

Premises used: List.head!_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) ℤ)
q : Products I
hq : q ∈ m.support
hx'' : q < (↑l : Products I).Tail
⊢ q =
    Products.Tail
      (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.Tail, List.tail_cons, Subtype.coe_eta]

Premises used: List.tail_cons, Subtype.coe_eta, Profinite.NobelingProof.Products.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) ℤ)
q : Products I
hq : q ∈ m.support
hx'' : q < (↑l : Products I).Tail
⊢ ∃ (p : Products I), (↑p : List I) ≠ [] ∧ (↑p : List I).head! = term I ho ∧ q = p.Tail

Tactic:
have : ∃ (p : Products I), p.val ≠ [] ∧ p.val.head! = term I ho ∧ q = p.Tail :=
      ⟨⟨term I ho :: q.val, isChain_cons_of_lt C hsC ho l q hx''⟩,
        ⟨List.cons_ne_nil _ _, by simp only [List.head!_cons],
        by simp only [Products.Tail, List.tail_cons, Subtype.coe_eta]⟩⟩