awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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
⊢ 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) ℤ)
have 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) ℤ)
Tactic: rw [Finsupp.mem_supported] at hmmem
Cleared hypotheses: hmmem, hmsum, q, hq
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
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
⊢ 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) ℤ)
have hx'' : q < (↑l : Products I).Tail
Tactic: have hx'' : q < l.val.Tail := hmmem hq
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
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
⊢ 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) ℤ)
have this₁ : ∃ (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]⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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_1 : 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
this : ∃ (p : Products I), (↑p : List I) ≠ [] ∧ (↑p : List I).head! = term I ho ∧ q = p.Tail
⊢ 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) ℤ)
have h : ∀ (p : Products I) (hp : (↑p : List I) ≠ [] ∧ (↑p : List I).head! = term I ho ∧ q = p.Tail),
  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: obtain ⟨p, hp⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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
hp : (↑p : List I) ≠ [] ∧ (↑p : List I).head! = term I ho ∧ q = p.Tail
⊢ 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) ℤ)
have h : HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
    ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
        (Products.eval C p) :
      LocallyConstant (↑(C' C ho) : Type u) ℤ) =
  HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
    ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
        (List.map (e C) (term I ho :: (↑p.Tail : List I))).prod :
      LocallyConstant (↑(C' C ho) : Type u) ℤ)
Tactic: rw [hp.2.2, ← Products.max_eq_eval C hsC ho p hp.1 hp.2.1]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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
hp : (↑p : List I) ≠ [] ∧ (↑p : List I).head! = term I ho ∧ q = p.Tail
⊢ HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
      ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          (Products.eval C p) :
        LocallyConstant (↑(C' C ho) : Type u) ℤ) =
    HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
      ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          (List.map (e C) (term I ho :: (↑p.Tail : List I))).prod :
        LocallyConstant (↑(C' C ho) : Type u) ℤ)
have h : HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
    ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
        (List.map (e C) (↑p : List I)).prod :
      LocallyConstant (↑(C' C ho) : Type u) ℤ) =
  HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
    ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
        (e C (term I ho) * (List.map (e C) (↑p.Tail : List I)).prod) :
      LocallyConstant (↑(C' C ho) : Type u) ℤ)
Tactic: dsimp [Products.eval]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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
hp : (↑p : List I) ≠ [] ∧ (↑p : List I).head! = term I ho ∧ q = p.Tail
⊢ HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
      ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          (List.map (e C) (↑p : List I)).prod :
        LocallyConstant (↑(C' C ho) : Type u) ℤ) =
    HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
      ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          (e C (term I ho) * (List.map (e C) (↑p.Tail : List I)).prod) :
        LocallyConstant (↑(C' C ho) : Type u) ℤ)
have h : HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
    ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
        (List.map (e C) (term I ho :: (↑p.Tail : List I))).prod :
      LocallyConstant (↑(C' C ho) : Type u) ℤ) =
  HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
    ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
        (e C (term I ho) * (List.map (e C) (↑p.Tail : List I)).prod) :
      LocallyConstant (↑(C' C ho) : Type u) ℤ)
Tactic: rw [Products.max_eq_o_cons_tail ho p hp.1 hp.2.1, List.map_cons, List.prod_cons]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
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) ℤ)
⊢ False
have this₁ : 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: have : (Linear_CC' C hsC ho) (l.val.eval C) = (Linear_CC' C hsC ho)
      (Finsupp.sum m fun i a ↦ a • ((term I ho :: i.1).map (e C)).prod) := by
    rw [← hmsum]
    simp only [map_finsuppSum]
    apply Finsupp.sum_congr
    intro q hq
    rw [map_smul]
    rw [Finsupp.mem_supported] at hmmem
    have hx'' : q < l.val.Tail := hmmem hq
    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]⟩⟩
    obtain ⟨p, hp⟩ := this
    rw [hp.2.2, ← Products.max_eq_eval C hsC ho p hp.1 hp.2.1]
    dsimp [Products.eval]
    rw [Products.max_eq_o_cons_tail ho p hp.1 hp.2.1, List.map_cons, List.prod_cons]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
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_1 : 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) ℤ)
this :
  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) ℤ)
⊢ False
have hse : { X₁ := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
    X₂ := ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ),
    X₃ := ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ), f := ModuleCat.ofHom (πs C o),
    g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := sorry : ShortComplex (ModuleCat ℤ) }.Exact
Tactic: have hse := succ_exact C hC hsC ho
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
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_1 : 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) ℤ)
this :
  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) ℤ)
hse :
  { X₁ := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
      X₂ := ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ),
      X₃ := ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ), f := ModuleCat.ofHom (πs C o),
      g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ : ShortComplex (ModuleCat ℤ) }.Exact
⊢ False
have hse₁ : (ModuleCat.Hom.hom
      { X₁ := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
          X₂ := ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ),
          X₃ := ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ), f := ModuleCat.ofHom (πs C o),
          g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := sorry : ShortComplex (ModuleCat ℤ) }.f).range =
  (ModuleCat.Hom.hom
      { X₁ := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
          X₂ := ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ),
          X₃ := ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ), f := ModuleCat.ofHom (πs C o),
          g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := sorry : ShortComplex (ModuleCat ℤ) }.g).ker
Tactic: rw [ShortComplex.moduleCat_exact_iff_range_eq_ker] at hse
Cleared hypotheses: hse