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
l : List I
hl : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l
hll :
  Products.isGood {fun (x : I) ↦ false}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl)
h : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) [] l
⊢ False
have a : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u) ℤ))
  (Submodule.span ℤ
    (Set.image (α := Products I) (Products.eval {fun (x : I) ↦ false})
      {m : Products I | m < Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl}))
  (Products.eval {fun (x : I) ↦ false}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl))
Tactic: apply hll
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : List I
hl : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l
hll :
  Products.isGood {fun (x : I) ↦ false}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl)
h : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) [] l
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval {fun (x : I) ↦ false})
        {m : Products I | m < Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl}))
    (Products.eval {fun (x : I) ↦ false}
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl))
have he : Subset (α := Set (Products I)) {Products.nil}
  {m : Products I | m < Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl}
Tactic: have he : {Products.nil} ⊆ {m | m < ⟨l,hl⟩} := by
      simpa only [Products.nil, Products.lt_iff_lex_lt, Set.singleton_subset_iff, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : List I
hl : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l
hll :
  Products.isGood {fun (x : I) ↦ false}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl)
h : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) [] l
he :
  Subset (α := Set (Products I)) {Products.nil}
    {m : Products I | m < Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl}
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval {fun (x : I) ↦ false})
        {m : Products I | m < Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl}))
    (Products.eval {fun (x : I) ↦ false}
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl))
have a : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u) ℤ))
  (Submodule.span ℤ (Set.image (α := Products I) (Products.eval {fun (x : I) ↦ false}) {Products.nil}))
  (Products.eval {fun (x : I) ↦ false}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl))
Tactic: grw [← he]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : List I
hl : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l
hll :
  Products.isGood {fun (x : I) ↦ false}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl)
h : List.Lex (fun (x1 x2 : I) ↦ x1 < x2) [] l
he :
  Subset (α := Set (Products I)) {Products.nil}
    {m : Products I | m < Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl}
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (Products.eval {fun (x : I) ↦ false}) {Products.nil}))
    (Products.eval {fun (x : I) ↦ false}
      (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl))
have a : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑{fun (x : I) ↦ false} : Type u) ℤ)) ⊤
  (Products.eval {fun (x : I) ↦ false}
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l hl))
Tactic: rw [Products.span_nil_eq_top]
-- 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}
⊢ Function.Bijective (β := (↑(smaller C o) : Type u)) fun (x : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦
    Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o)
      ((πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        (↑x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
      ⋯
have refine_1 : ∀ (a b : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u))
  (hab :
    Eq.{u + 1} (α := (↑(smaller C o) : Type u))
      ((fun (x : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦
          (Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o)
              ((πs C o :
                  (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
                (↑x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
              sorry :
            { x : LocallyConstant (↑C : Type u) ℤ // x ∈ smaller C o }))
        a)
      ((fun (x : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦
          (Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o)
              ((πs C o :
                  (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
                (↑x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
              sorry :
            { x : LocallyConstant (↑C : Type u) ℤ // x ∈ smaller C o }))
        b)),
  a = b
Tactic: refine ⟨fun a b hab ↦ ?_, fun ⟨a, 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}
refine_1 :
  ∀ (a b : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u))
    (hab :
      Eq.{u + 1} (α := (↑(smaller C o) : Type u))
        ((fun (x : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦
            (Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o)
                ((πs C o :
                    (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) →
                      LocallyConstant (↑C : Type u) ℤ)
                  (↑x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
                ⋯ :
              { x : LocallyConstant (↑C : Type u) ℤ // x ∈ smaller C o }))
          a)
        ((fun (x : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦
            (Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o)
                ((πs C o :
                    (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) →
                      LocallyConstant (↑C : Type u) ℤ)
                  (↑x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
                ⋯ :
              { x : LocallyConstant (↑C : Type u) ℤ // x ∈ smaller C o }))
          b)),
    a = b
⊢ Function.Bijective (β := (↑(smaller C o) : Type u)) fun (x : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦
    Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o)
      ((πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        (↑x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
      ⋯
have refine_2 : ∀ (x : (↑(smaller C o) : Type u)) (a : LocallyConstant (↑C : Type u) ℤ)
  (b : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)
  (hb :
    b ∈ range (π C fun (x : I) ↦ ord I x < o) ∧
      (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          b =
        a),
  ∃ (a_1 : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)),
    Eq (α := (↑(smaller C o) : Type u))
      ((fun (x : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦
          (Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o)
              ((πs C o :
                  (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
                (↑x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
              sorry :
            { x : LocallyConstant (↑C : Type u) ℤ // x ∈ smaller C o }))
        a_1)
      (Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o) a sorry)
Tactic: refine ⟨fun a b hab ↦ ?_, fun ⟨a, 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}
a b : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)
hab :
  Eq.{u + 1} (α := (↑(smaller C o) : Type u))
    ((fun (x : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦
        (Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o)
            ((πs C o :
                (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
              (↑x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
            ⋯ :
          { x : LocallyConstant (↑C : Type u) ℤ // x ∈ smaller C o }))
      a)
    ((fun (x : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦
        (Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o)
            ((πs C o :
                (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
              (↑x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
            ⋯ :
          { x : LocallyConstant (↑C : Type u) ℤ // x ∈ smaller C o }))
      b)
⊢ a = b
have refine_1 : (↑a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) =
  (↑b : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)
Tactic: ext1
-- 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}
a b : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)
hab :
  Eq.{u + 1} (α := (↑(smaller C o) : Type u))
    ((fun (x : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦
        (Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o)
            ((πs C o :
                (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
              (↑x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
            ⋯ :
          { x : LocallyConstant (↑C : Type u) ℤ // x ∈ smaller C o }))
      a)
    ((fun (x : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦
        (Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o)
            ((πs C o :
                (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
              (↑x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
            ⋯ :
          { x : LocallyConstant (↑C : Type u) ℤ // x ∈ smaller C o }))
      b)
⊢ (↑a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) =
    (↑b : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)
have hab₁ : Eq (α := LocallyConstant (↑C : Type u) ℤ)
  ((πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
      (↑a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : 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) ℤ)
      (↑b : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) :
    LocallyConstant (↑C : Type u) ℤ)
Tactic: simp only [Subtype.mk.injEq] at hab
Cleared hypotheses: hab
-- 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}
x : (↑(smaller C o) : Type u)
a : LocallyConstant (↑C : Type u) ℤ
b : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ
hb :
  b ∈ range (π C fun (x : I) ↦ ord I x < o) ∧
    (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) b =
      a
⊢ ∃ (a_1 : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)),
    Eq (α := (↑(smaller C o) : Type u))
      ((fun (x : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦
          (Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o)
              ((πs C o :
                  (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
                (↑x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
              ⋯ :
            { x : LocallyConstant (↑C : Type u) ℤ // x ∈ smaller C o }))
        a_1)
      (Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o) a ⋯)
have h : Eq (α := (↑(smaller C o) : Type u))
  ((fun (x : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦
      (Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o)
          ((πs C o :
              (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
            (↑x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
          sorry :
        { x : LocallyConstant (↑C : Type u) ℤ // x ∈ smaller C o }))
    (Subtype.mk (p := fun (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) ↦
      x ∈ range (π C fun (x : I) ↦ ord I x < o)) b sorry))
  (Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o) a sorry)
Tactic: use ⟨b, hb.1⟩
-- 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}
⊢ LinearIndependent (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l }) ℤ
      (eval (π C fun (x : I) ↦ ord I x < o)) ↔
    LinearIndependent ℤ (M := LocallyConstant (↑C : Type u) ℤ) fun (p : (↑(smaller C o) : Type u)) ↦
      (↑p : LocallyConstant (↑C : Type u) ℤ)
have rw : LinearIndependent (ι := (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)) ℤ (M := LocallyConstant (↑C : Type u) ℤ)
    ((fun (p : (↑(smaller C o) : Type u)) ↦ (↑p : LocallyConstant (↑C : Type u) ℤ)) ∘
      Equiv.toFun (range_equiv_smaller C o)) ↔
  LinearIndependent ℤ (M := LocallyConstant (↑C : Type u) ℤ) fun (p : (↑(smaller C o) : Type u)) ↦
    (↑p : LocallyConstant (↑C : Type u) ℤ)
Tactic: rw [GoodProducts.linearIndependent_iff_range,
    ← LinearMap.linearIndependent_iff (πs C o)
    (LinearMap.ker_eq_bot_of_injective (injective_πs _ _)), ← smaller_factorization C o]
-- 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₂
g : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ
hg : g ∈ range (π C fun (x : I) ↦ ord I x < o₁)
⊢ ∃ x ∈ range (π C fun (x : I) ↦ ord I x < o₂),
    Eq (α := LocallyConstant (↑C : Type u) ℤ)
      ((πs C o₂ :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          x :
        LocallyConstant (↑C : Type u) ℤ)
      ((πs C o₁ :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          g :
        LocallyConstant (↑C : Type u) ℤ)
have 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) ℤ)
        g :
      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) ℤ)
          g) :
      LocallyConstant (↑C : Type u) ℤ)
    ((πs C o₁ : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        g :
      LocallyConstant (↑C : Type u) ℤ)
Tactic: use πs' C h g
-- 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₂
g : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ
hg : g ∈ range (π C fun (x : I) ↦ ord I x < o₁)
⊢ 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) ℤ)
          g :
        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) ℤ)
            g) :
        LocallyConstant (↑C : Type u) ℤ)
      ((πs C o₁ :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          g :
        LocallyConstant (↑C : Type u) ℤ)
have h₁ : ∀ (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) ℤ) ∧
    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: obtain ⟨⟨l, gl⟩, rfl⟩ := hg
Cleared hypotheses: g, hg
-- 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) ℤ) ∧
    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₁ : 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) ℤ)
Tactic: refine ⟨?_, ?_⟩