awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l
h₁ :
  Membership.mem (α := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
    (range (π C fun (x : I) ↦ ord I x < o₂))
    ((πs' C h :
          (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < o₁)
          (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
      LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
⊢ Membership.mem (α := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
      (range (π C fun (x : I) ↦ ord I x < o₂))
      ((πs' C h :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
              LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
          (eval (π C fun (x : I) ↦ ord I x < o₁)
            (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
        LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) ∧
    Eq (α := LocallyConstant (↑C : Type u) ℤ)
      ((πs C o₂ :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          ((πs' C h :
              (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
            (eval (π C fun (x : I) ↦ ord I x < o₁)
              (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl))) :
        LocallyConstant (↑C : Type u) ℤ)
      ((π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₁)
            (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
        LocallyConstant (↑C : Type u) ℤ)
have h₂ : Eq (α := LocallyConstant (↑C : Type u) ℤ)
  ((πs C o₂ : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
      ((πs' C h :
          (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < o₁)
          (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl))) :
    LocallyConstant (↑C : Type u) ℤ)
  ((π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₁)
        (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
    LocallyConstant (↑C : Type u) ℤ)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l
⊢ Membership.mem (α := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
    (range (π C fun (x : I) ↦ ord I x < o₂))
    ((πs' C h :
          (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < o₁)
          (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
      LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
have h₁ : eval (π C fun (x : I) ↦ ord I x < o₂)
    (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₂) l) l sorry) =
  (πs' C h :
      (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
        LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
    (eval (π C fun (x : I) ↦ ord I x < o₁)
      (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl))
Tactic: use ⟨l, Products.isGood_mono C h gl⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l
⊢ eval (π C fun (x : I) ↦ ord I x < o₂)
      (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₂) l) l ⋯) =
    (πs' C h :
        (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
          LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
      (eval (π C fun (x : I) ↦ ord I x < o₁)
        (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl))
have h₁ : ∀ (x : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)),
  Eq (α := ℤ)
    ((eval (π C fun (x : I) ↦ ord I x < o₂)
            (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₂) l) l sorry) :
          (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
        x :
      ℤ)
    ((((πs' C h :
                (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                  LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
              (eval (π C fun (x : I) ↦ ord I x < o₁)
                (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) :
          (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
        x :
      ℤ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l
x : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)
⊢ Eq (α := ℤ)
    ((eval (π C fun (x : I) ↦ ord I x < o₂)
            (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₂) l) l ⋯) :
          (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
        x :
      ℤ)
    ((((πs' C h :
                (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                  LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
              (eval (π C fun (x : I) ↦ ord I x < o₁)
                (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) :
          (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
        x :
      ℤ)
have h₁ : Eq (α := ℤ)
  ((Products.eval (π C fun (x : I) ↦ ord I x < o₂)
          (↑(Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₂) l) l sorry) :
            Products I) :
        (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
      x :
    ℤ)
  ((((πs' C h :
              (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
            (eval (π C fun (x : I) ↦ ord I x < o₁)
              (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
          LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) :
        (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
      x :
    ℤ)
Tactic: rw [eval, ← Products.eval_πs' _ h (Products.prop_of_isGood C _ gl), eval]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l
x : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)
h₁ :
  Eq (α := ℤ)
    ((Products.eval (π C fun (x : I) ↦ ord I x < o₂)
            (↑(Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₂) l) l ⋯) :
              Products I) :
          (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
        x :
      ℤ)
    ((((πs' C h :
                (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                  LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
              (eval (π C fun (x : I) ↦ ord I x < o₁)
                (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) :
          (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
        x :
      ℤ)
⊢ Eq (α := ℤ)
    ((eval (π C fun (x : I) ↦ ord I x < o₂)
            (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₂) l) l ⋯) :
          (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
        x :
      ℤ)
    ((((πs' C h :
                (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                  LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
              (eval (π C fun (x : I) ↦ ord I x < o₁)
                (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) :
          (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
        x :
      ℤ)
have h₂ : Eq (α := ℤ)
  ((((πs' C h :
              (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
            (Products.eval (π C fun (x : I) ↦ ord I x < o₁) l) :
          LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) :
        (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
      x :
    ℤ)
  ((((πs' C h :
              (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
            (eval (π C fun (x : I) ↦ ord I x < o₁)
              (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
          LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) :
        (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
      x :
    ℤ)
Tactic: rw [eval, ← Products.eval_πs' _ h (Products.prop_of_isGood C _ gl), eval]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l
⊢ Eq (α := LocallyConstant (↑C : Type u) ℤ)
    ((πs C o₂ : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        ((πs' C h :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
              LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
          (eval (π C fun (x : I) ↦ ord I x < o₁)
            (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl))) :
      LocallyConstant (↑C : Type u) ℤ)
    ((π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₁)
          (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
      LocallyConstant (↑C : Type u) ℤ)
have h₁ : ((eval (π C fun (x : I) ↦ ord I x < o₁)
        (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)).toFun ∘
    ProjRestrict C fun (x : I) ↦ ord I x < o₁) =
  Function.comp (β := (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u))
    (⇑(eval (π C fun (x : I) ↦ ord I x < o₁)
          (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
      (a : (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u)) → ℤ)
    (ProjRestrict C fun (x : I) ↦ ord I x < o₁)
Tactic: rw [← LocallyConstant.coe_inj, coe_πs C o₂, ← LocallyConstant.toFun_eq_coe, coe_πs',
      Function.comp_assoc, projRestricts_comp_projRestrict C _, coe_πs]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
⊢ isGood (π C fun (x : I) ↦ ord I x < o) l ↔ ∃ o' < o, isGood (π C fun (x : I) ↦ ord I x < o') l
have refine : ∀ (h : isGood (π C fun (x : I) ↦ ord I x < o) l), ∃ o' < o, isGood (π C fun (x : I) ↦ ord I x < o') l
Tactic: refine ⟨fun h ↦ ?_, fun ⟨o', ⟨ho', hl⟩⟩ ↦ isGood_mono C (le_of_lt ho') hl⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
⊢ ∃ o' < o, isGood (π C fun (x : I) ↦ ord I x < o') l
have h₁ : ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o ∧
  isGood (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l
Tactic: use Finset.sup l.val.toFinset (fun a ↦ Order.succ (ord I a))
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
⊢ ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o
have simp : ∀ b ∈ (↑l : List I), Order.succ (ord I b) < o
Tactic: simp only [Finset.sup_lt_iff ho.bot_lt, List.mem_toFinset]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
⊢ ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o ∧
    isGood (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l
have hslt : ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o
Tactic: have hslt : Finset.sup l.val.toFinset (fun a ↦ Order.succ (ord I a)) < o := by
    simp only [Finset.sup_lt_iff ho.bot_lt, List.mem_toFinset]
    exact fun b hb ↦ ho.succ_lt (prop_of_isGood C (ord I · < o) h b hb)
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
hslt : ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o
⊢ ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o ∧
    isGood (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l
have h₁ : ∀
  (he :
    Membership.mem (γ :=
      Submodule ℤ
        (LocallyConstant
          (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u) ℤ))
      (Submodule.span ℤ
        (Set.image (α := Products I)
          (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)))
          {m : Products I | m < l}))
      (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l)),
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < o) l)
Tactic: refine ⟨hslt, fun he ↦ h ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
hslt : ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o
he :
  Membership.mem (γ :=
    Submodule ℤ
      (LocallyConstant
        (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I)
        (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)))
        {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l)
i : I
hi : i ∈ (↑l : List I)
⊢ ord I i < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)
have simp : ∃ b ∈ (↑l : List I), ord I i ≤ ord I b
Tactic: simp only [Finset.lt_sup_iff, List.mem_toFinset, Order.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
hslt : ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o
he :
  Membership.mem (γ :=
    Submodule ℤ
      (LocallyConstant
        (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I)
        (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)))
        {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l)
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < o) l)
have hlt : ∀ i ∈ (↑l : List I), ord I i < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)
Tactic: have hlt : ∀ i ∈ l.val, ord I i < Finset.sup l.val.toFinset (fun a ↦ Order.succ (ord I a)) := by
    intro i hi
    simp only [Finset.lt_sup_iff, List.mem_toFinset, Order.lt_succ_iff]
    exact ⟨i, hi, le_rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
hslt : ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o
he :
  Membership.mem (γ :=
    Submodule ℤ
      (LocallyConstant
        (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I)
        (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)))
        {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l)
hlt : ∀ i ∈ (↑l : List I), ord I i < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < o) l)
have h₁ : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
  (Submodule.span ℤ
    ((⇑(πs' C sorry) :
        (a :
            LocallyConstant
              (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u)
              ℤ) →
          LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) ''
      Set.image (α := Products I)
        (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)))
        {m : Products I | m < l}))
  (eval (π C fun (x : I) ↦ ord I x < o) l)
Tactic: rwa [eval_πs_image' C (le_of_lt hslt) hlt, ← eval_πs' C (le_of_lt hslt) hlt,
    Submodule.apply_mem_span_image_iff_mem_span (injective_πs' C _)]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
hslt : ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o
he :
  Membership.mem (γ :=
    Submodule ℤ
      (LocallyConstant
        (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I)
        (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)))
        {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l)
hlt : ∀ i ∈ (↑l : List I), ord I i < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)
h₁ :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
    (Submodule.span ℤ
      ((⇑(πs' C ⋯) :
          (a :
              LocallyConstant
                (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u)
                ℤ) →
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) ''
        Set.image (α := Products I)
          (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)))
          {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < o) l)
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < o) l)
have h₂ : Membership.mem (α := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) (γ :=
  Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
  (Submodule.span ℤ
    ((⇑(πs' C sorry) :
        (a :
            LocallyConstant
              (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u)
              ℤ) →
          LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) ''
      Set.image (α := Products I)
        (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)))
        {m : Products I | m < l}))
  ((πs' C sorry :
        (a :
            LocallyConstant
              (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u)
              ℤ) →
          LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)
      (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l) :
    LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)
Tactic: rwa [eval_πs_image' C (le_of_lt hslt) hlt, ← eval_πs' C (le_of_lt hslt) hlt,
    Submodule.apply_mem_span_image_iff_mem_span (injective_πs' C _)]