awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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
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) ℤ))
                ⋯ :
              { 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 ⋯)
⊢ 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) ℤ))
      ⋯

Tactic:
refine ⟨fun a b hab ↦ ?_, fun ⟨a, b, hb⟩ ↦ ?_⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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)
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) ℤ)
⊢ a = b

Tactic:
ext1
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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)
⊢ 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

Premises used: Subtype.mk.injEq
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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 (α := 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) ℤ)
⊢ (↑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:
injective_πs C o hab

Premises used: Profinite.NobelingProof.injective_πs
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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 (α := 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) ℤ)
⊢ (↑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:
exact injective_πs C o hab

Premises used: Profinite.NobelingProof.injective_πs
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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
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) ℤ))
            ⋯ :
          { 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 ⋯))
    (Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o) 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 ⋯)

Tactic:
use ⟨b, hb.1⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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
⊢ 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 }))
      (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 ⋯))
    (Subtype.mk (p := fun (x : LocallyConstant (↑C : Type u) ℤ) ↦ x ∈ smaller C o) a ⋯)

Tactic:
simpa only [Subtype.mk.injEq] using hb.2

Premises used: And.right, Subtype.mk.injEq
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
⊢ Eq (α := (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u) → LocallyConstant (↑C : Type u) ℤ)
    ((fun (p : (↑(smaller C o) : Type u)) ↦ (↑p : LocallyConstant (↑C : Type u) ℤ)) ∘
      Equiv.toFun (range_equiv_smaller C o))
    (Function.comp (β := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)
      (⇑(πs C o) :
        (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
      fun (p : (↑(range (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦
      (↑p : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))

Tactic:
rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
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) ℤ)
⊢ 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) ℤ)

Tactic:
rw [GoodProducts.linearIndependent_iff_range,
    ← LinearMap.linearIndependent_iff (πs C o)
    (LinearMap.ker_eq_bot_of_injective (injective_πs _ _)), ← smaller_factorization C o]

Premises used: Profinite.NobelingProof.πs, Profinite.NobelingProof.GoodProducts.smaller_factorization, LinearMap.linearIndependent_iff, LinearMap.ker_eq_bot_of_injective, Profinite.NobelingProof.injective_πs, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_range
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
⊢ 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:
linearIndependent_equiv _

Premises used: linearIndependent_equiv
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
⊢ 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:
exact linearIndependent_equiv _

Premises used: linearIndependent_equiv
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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₁)
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) ℤ)
⊢ ∃ 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) ℤ)

Tactic:
use πs' C h g

Premises used: Profinite.NobelingProof.πs', DFunLike.coe
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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₁)
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) ℤ)
⊢ 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:
obtain ⟨⟨l, gl⟩, rfl⟩ := hg

Premises used: rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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) ℤ)

Tactic:
⟨?_, ?_⟩

Premises used: And.intro