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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this : Inhabited I
a : I
ha : a ∈ (↑q : List I)
hM : (↑(↑l : Products I).Tail : List I) = []
⊢ (↑(↑l : Products I).Tail : List I).head! < term I ho
have pos : ∀ (hq : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑q : List I) []) (this : Inhabited I) (a : I) (ha : a ∈ (↑q : List I))
  (hM : (↑(↑l : Products I).Tail : List I) = []), (↑(↑l : Products I).Tail : List I).head! < term I ho
Tactic: rw [Products.lt_iff_lex_lt, hM] at hq
Cleared hypotheses: hq, this, a, ha, hM
-- 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this : Inhabited I
a : I
ha : a ∈ (↑q : List I)
hM : ¬(↑(↑l : Products I).Tail : List I) = []
⊢ (↑(↑l : Products I).Tail : List I).head! < term I ho
have this₁ : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (↑(↑l : Products I) : List I)
Tactic: have := l.val.prop
-- 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this_1 : Inhabited I
a : I
ha : a ∈ (↑q : List I)
hM : ¬(↑(↑l : Products I).Tail : List I) = []
this : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (↑(↑l : Products I) : List I)
⊢ (↑(↑l : Products I).Tail : List I).head! < term I ho
have this₁ : List.Pairwise (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑(↑l : Products I).Tail : List I))
Tactic: rw [max_eq_o_cons_tail C hsC ho l, List.isChain_iff_pairwise] at this
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}
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)
⊢ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑(↑q : Products I) : List I) (↑(↑l : Products I) : List I)
have have : ∀ (this : Inhabited I), List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑(↑q : Products I) : List I) (↑(↑l : Products I) : List I)
Tactic: have : Inhabited I := ⟨term I ho⟩
-- 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}
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
⊢ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑(↑q : Products I) : List I) (↑(↑l : Products I) : List I)
have pos : ∀ (h : (↑(↑q : Products I) : List I) = []),
  List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑(↑q : Products I) : List I) (↑(↑l : Products I) : List I)
Tactic: by_cases h : q.val.val = []
-- 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
q : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)
l : (↑(MaxProducts C ho) : Type u)
this : Inhabited I
pos :
  ∀ (h : (↑(↑q : Products I) : List I) = []),
    List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑(↑q : Products I) : List I) (↑(↑l : Products I) : List I)
⊢ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑(↑q : Products I) : List I) (↑(↑l : Products I) : List I)
have neg : ∀ (h : ¬(↑(↑q : Products I) : List I) = []),
  List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑(↑q : Products I) : List I) (↑(↑l : Products I) : List I)
Tactic: by_cases h : q.val.val = []
-- 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
q : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)
l : (↑(MaxProducts C ho) : Type u)
this : Inhabited I
h : (↑(↑q : Products I) : List I) = []
⊢ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑(↑q : Products I) : List I) (↑(↑l : Products I) : List I)
have pos : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) [] (term I ho :: (↑(↑l : Products I).Tail : List I))
Tactic: rw [h, max_eq_o_cons_tail C hsC ho l]
-- 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
q : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)
l : (↑(MaxProducts C ho) : Type u)
this : Inhabited I
h : ¬(↑(↑q : Products I) : List I) = []
⊢ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑(↑q : Products I) : List I) (↑(↑l : Products I) : List I)
have neg : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) ((↑(↑q : Products I) : List I).head! :: (↑(↑q : Products I) : List I).tail)
  (term I ho :: (↑(↑l : Products I).Tail : List I))
Tactic: rw [← List.cons_head!_tail h, max_eq_o_cons_tail C hsC ho l]
-- 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
q : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)
l : (↑(MaxProducts C ho) : Type u)
this : Inhabited I
h : ¬(↑(↑q : Products I) : List I) = []
⊢ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) ((↑(↑q : Products I) : List I).head! :: (↑(↑q : Products I) : List I).tail)
    (term I ho :: (↑(↑l : Products I).Tail : List I))
have neg : (↑(↑q : Products I) : List I).head! < term I ho
Tactic: apply List.Lex.rel
-- 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}
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) = []
⊢ (↑(↑q : Products I) : List I).head! < term I ho
have neg : LT.lt (α := Ordinal.{u})
  ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : I) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
          (Ordinal.typein fun (x1 x2 : I) ↦ x1 < x2) :
        (a : I) → Ordinal.{u})
      (↑(↑q : Products I) : List I).head! :
    Ordinal.{u})
  ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : I) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
          (Ordinal.typein fun (x1 x2 : I) ↦ x1 < x2) :
        (a : I) → Ordinal.{u})
      (term I ho) :
    Ordinal.{u})
Tactic: rw [← Ordinal.typein_lt_typein (· < ·)]
-- 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}
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) = []
⊢ LT.lt (α := Ordinal.{u})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : I) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : I) ↦ x1 < x2) :
          (a : I) → Ordinal.{u})
        (↑(↑q : Products I) : List I).head! :
      Ordinal.{u})
    ((PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : I) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
            (Ordinal.typein fun (x1 x2 : I) ↦ x1 < x2) :
          (a : I) → Ordinal.{u})
        (term I ho) :
      Ordinal.{u})
have neg : (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : I) ↦ x1 < x2) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)
        (Ordinal.typein fun (x1 x2 : I) ↦ x1 < x2) :
      (a : I) → Ordinal.{u})
    (↑(↑q : Products I) : List I).head! <
  o
Tactic: simp only [term, Ordinal.typein_enum]
-- 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))))
⊢ Products.isGood (C' C ho) (↑l : Products I).Tail
have have : ∀ (this : Inhabited I), Products.isGood (C' C ho) (↑l : Products I).Tail
Tactic: have : Inhabited I := ⟨term I 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 : 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)
⊢ False
have 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) ℤ)
Tactic: rw [Finsupp.mem_span_image_iff_linearCombination, ← max_eq_eval C hsC ho] at h
Cleared hypotheses: h
-- 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
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) ℤ)
⊢ False
have 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
Tactic: obtain ⟨m, ⟨hmmem, hmsum⟩⟩ := h
Cleared hypotheses: h
-- 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) ℤ)
    ((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
have 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) ℤ)
Tactic: rw [Finsupp.linearCombination_apply] at hmsum
Cleared hypotheses: hmsum
-- 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) ℤ)
⊢ 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) ℤ)
have 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))
Tactic: rw [← hmsum]
-- 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) ℤ)
⊢ 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))
have 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))
Tactic: simp only [map_finsuppSum]
-- 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) ℤ)
⊢ 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))
have 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)
Tactic: apply Finsupp.sum_congr
-- 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) =
    (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)
have 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) ℤ)
Tactic: rw [map_smul]