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 :
  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) ℤ)
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) ℤ
hn :
  HAdd.hAdd (α := LocallyConstant (↑C : Type u) ℤ) (β := LocallyConstant (↑C : Type u) ℤ)
      ((πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          n :
        LocallyConstant (↑C : Type u) ℤ)
      (m.sum fun (i : Products I) (a : ℤ) ↦ a • (List.map (e C) (term I ho :: (↑i : List I))).prod :
        LocallyConstant (↑C : Type u) ℤ) =
    Products.eval C (↑l : Products I)
⊢ Membership.mem (γ := 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))))
    n

Tactic:
have hn' := h₁ (Submodule.mem_top : n ∈ ⊤)
-- 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) ℤ)
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) ℤ
hn :
  HAdd.hAdd (α := LocallyConstant (↑C : Type u) ℤ) (β := LocallyConstant (↑C : Type u) ℤ)
      ((πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          n :
        LocallyConstant (↑C : Type u) ℤ)
      (m.sum fun (i : Products I) (a : ℤ) ↦ a • (List.map (e C) (term I ho :: (↑i : List I))).prod :
        LocallyConstant (↑C : Type u) ℤ) =
    Products.eval C (↑l : Products I)
hn' :
  Membership.mem (γ := 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))))
    n
⊢ ∃ (c : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l } →₀ ℤ),
    (c.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

Tactic:
rw [Finsupp.mem_span_range_iff_exists_finsupp] at hn'

Premises used: Finsupp.mem_span_range_iff_exists_finsupp
-- 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) ℤ)
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) ℤ
hn :
  HAdd.hAdd (α := LocallyConstant (↑C : Type u) ℤ) (β := LocallyConstant (↑C : Type u) ℤ)
      ((πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          n :
        LocallyConstant (↑C : Type u) ℤ)
      (m.sum fun (i : Products I) (a : ℤ) ↦ a • (List.map (e C) (term I ho :: (↑i : List I))).prod :
        LocallyConstant (↑C : Type u) ℤ) =
    Products.eval C (↑l : Products I)
hn' :
  ∃ (c : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l } →₀ ℤ),
    (c.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
obtain :
  ∀ (w : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l } →₀ ℤ)
    (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),
    False
⊢ False

Tactic:
obtain ⟨w, hc⟩ := hn'
-- 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) ℤ)
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) ℤ
hn :
  HAdd.hAdd (α := LocallyConstant (↑C : Type u) ℤ) (β := LocallyConstant (↑C : Type u) ℤ)
      ((πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          n :
        LocallyConstant (↑C : Type u) ℤ)
      (m.sum fun (i : Products I) (a : ℤ) ↦ a • (List.map (e C) (term I ho :: (↑i : List I))).prod :
        LocallyConstant (↑C : Type u) ℤ) =
    Products.eval C (↑l : Products I)
w : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l } →₀ ℤ
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
⊢ 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)

Tactic:
rw [← hc, map_finsuppSum] at hn

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) ℤ)
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) ℤ
hn :
  HAdd.hAdd (α := LocallyConstant (↑C : Type u) ℤ) (β := LocallyConstant (↑C : Type u) ℤ)
      ((πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          n :
        LocallyConstant (↑C : Type u) ℤ)
      (m.sum fun (i : Products I) (a : ℤ) ↦ a • (List.map (e C) (term I ho :: (↑i : List I))).prod :
        LocallyConstant (↑C : Type u) ℤ) =
    Products.eval C (↑l : Products I)
w : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l } →₀ ℤ
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
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)
⊢ (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

Tactic:
rw [← hc, map_finsuppSum] at hn

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) ℤ)
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
apply :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < (↑l : Products I)}))
    (Products.eval C (↑l : Products I))
⊢ False

Tactic:
apply l.prop.1

Premises used: And.left, Subtype.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}
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) ℤ)
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
rw :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < (↑l : Products I)}))
    (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))
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < (↑l : Products I)}))
    (Products.eval C (↑l : Products I))

Tactic:
rw [← hn]
-- 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) ℤ)
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 : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }
h : Ne (α := ℤ) ((w : (a : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) → ℤ) q : ℤ) (0 : ℤ)
h₂ :
  Membership.mem (α := LocallyConstant (↑C : Type u) ℤ)
    (Set.image (α := Products I) (Products.eval C) {m : Products I | m < (↑l : Products I)})
    ((πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < o) q) :
      LocallyConstant (↑C : Type u) ℤ)
⊢ Membership.mem (α := LocallyConstant (↑C : Type u) ℤ) (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < (↑l : Products I)}))
    ((πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < o) q) :
      LocallyConstant (↑C : Type u) ℤ)

Tactic:
apply Submodule.subset_span

Premises used: Submodule.subset_span
-- 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) ℤ)
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 : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }
h : Ne (α := ℤ) ((w : (a : { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) → ℤ) q : ℤ) (0 : ℤ)
h₂ :
  Products.eval C (↑q : Products I) ∈
    Set.image (α := Products I) (Products.eval C) {m : Products I | m < (↑l : Products I)}
⊢ Membership.mem (α := LocallyConstant (↑C : Type u) ℤ)
    (Set.image (α := Products I) (Products.eval C) {m : Products I | m < (↑l : Products I)})
    ((πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        (Products.eval (π C fun (x : I) ↦ ord I x < o) (↑q : Products I)) :
      LocallyConstant (↑C : Type u) ℤ)

Tactic:
rw [Products.eval_πs C (Products.prop_of_isGood _ _ q.prop)]

Premises used: Profinite.NobelingProof.Products.eval_πs, Profinite.NobelingProof.Products.prop_of_isGood, Subtype.prop