awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (hypothesis)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : o + 1 ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (o + 1)
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)
have ho' : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
Tactic: have ho' : o < Ordinal.type (· < · : I → I → Prop) :=
    lt_of_lt_of_le (Order.lt_succ _) ho
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : o + 1 ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (o + 1)
ho' : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)
have rw : LinearIndependent (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho') : Type u)) ℤ
  (SumEval C ho')
Tactic: rw [linearIndependent_iff_sum C hsC ho']
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : o + 1 ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (o + 1)
ho' : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ LinearIndependent (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho') : Type u))
    ℤ (SumEval C ho')
have refine_1 : LinearIndependent (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ℤ
  (eval (π C fun (x : I) ↦ ord I x < o))
Tactic: refine ModuleCat.linearIndependent_leftExact (succ_exact C hC hsC ho') ?_ ?_ (succ_mono C o)
    (square_commutes C ho')
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : o + 1 ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (o + 1)
ho' : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
refine_1 :
  LinearIndependent (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ℤ
    (eval (π C fun (x : I) ↦ ord I x < o))
⊢ LinearIndependent (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho') : Type u))
    ℤ (SumEval C ho')
have refine_2 : LinearIndependent (ι := (↑(MaxProducts C ho') : Type u)) ℤ (M :=
  (↑{ 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 : CategoryTheory.ShortComplex (ModuleCat ℤ) }.X₃ :
    Type u))
  ((⇑(CategoryTheory.ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier)
          { 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 : CategoryTheory.ShortComplex (ModuleCat ℤ) }.g) :
      (a :
          (↑{ 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 }.X₂ :
            Type u)) →
        (↑{ 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 }.X₃ :
          Type u)) ∘
    SumEval C ho' ∘ Sum.inr)
Tactic: refine ModuleCat.linearIndependent_leftExact (succ_exact C hC hsC ho') ?_ ?_ (succ_mono C o)
    (square_commutes C ho')
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
S : Profinite
⊢ IsClosedEmbedding (ι S)
have h : Continuous (ι S)
Tactic: apply Continuous.isClosedEmbedding
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
S : Profinite
h : Continuous (ι S)
⊢ IsClosedEmbedding (ι S)
have hf : Function.Injective (ι S)
Tactic: apply Continuous.isClosedEmbedding
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
S : Profinite
⊢ Continuous (Y :=
    { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
        IsClopen C } →
      Bool)
    fun (s : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      (C :
        { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
          IsClopen C }) ↦
    decide (s ∈ (↑C : Set (↑S.toTop : Type u)))
have h : ∀
  (i :
    { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
      IsClopen C }),
  Continuous (Y := Bool)
    fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
    decide (a ∈ (↑i : Set (↑S.toTop : Type u)))
Tactic: refine continuous_pi ?_
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
⊢ Continuous (Y := Bool)
    fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
    decide (a ∈ (↑C : Set (↑S.toTop : Type u)))
have h : IsLocallyConstant (Y := Bool)
  fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
  decide (a ∈ (↑C : Set (↑S.toTop : Type u)))
Tactic: rw [← IsLocallyConstant.iff_continuous]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
⊢ IsLocallyConstant (Y := Bool)
    fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
    decide (a ∈ (↑C : Set (↑S.toTop : Type u)))
have h : ∀ (y : Bool),
  IsOpen.{u} (X := (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (Set.preimage (β := Bool)
      (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
        decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
      {y})
Tactic: refine ((IsLocallyConstant.tfae _).out 0 3).mpr ?_
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
⊢ IsOpen.{u} (X := (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (Set.preimage (β := Bool)
      (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
        decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
      {false})
have h : IsClopen.{u} (X := (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
  (Set.preimage (β := Bool)
      (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
        decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
      {false})ᶜ
Tactic: refine IsClopen.isOpen (isClopen_compl_iff.mp ?_)
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
⊢ IsClopen.{u} (X := (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (Set.preimage (β := Bool)
        (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
          decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
        {false})ᶜ
have h : (Set.preimage (β := Bool)
      (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
        decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
      {false})ᶜ =
  (↑C : Set (↑S.toTop : Type u))
Tactic: convert! C.2
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
⊢ (Set.preimage (β := Bool)
        (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
          decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
        {false})ᶜ =
    (↑C : Set (↑S.toTop : Type u))
have h : ∀ (x : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
  Membership.mem (γ :=
      Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      (Set.preimage (β := Bool)
          (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
            decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
          {false})ᶜ
      x ↔
    x ∈ (↑C : Set (↑S.toTop : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
⊢ IsOpen.{u} (X := (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (Set.preimage (β := Bool)
      (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
        decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
      {true})
have h : IsClopen.{u} (X := (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
  (Set.preimage (β := Bool)
    (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
      decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
    {true})
Tactic: refine IsClopen.isOpen ?_
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
⊢ IsClopen.{u} (X := (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (Set.preimage (β := Bool)
      (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
        decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
      {true})
have h : Set.preimage (β := Bool)
    (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
      decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
    {true} =
  (↑C : Set (↑S.toTop : Type u))
Tactic: convert! C.2
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
⊢ Set.preimage (β := Bool)
      (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
        decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
      {true} =
    (↑C : Set (↑S.toTop : Type u))
have h : ∀ (x : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
  Membership.mem (γ :=
      Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      (Set.preimage (β := Bool)
        (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
          decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
        {true})
      x ↔
    x ∈ (↑C : Set (↑S.toTop : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
S : Profinite
a b : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
h : ι S a = ι S b
⊢ a = b
have hf : ∀ (hn : ¬a = b), False
Tactic: by_contra hn
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
S : Profinite
a b : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
h : ι S a = ι S b
hn : ¬a = b
⊢ False
have hf : ∀ (C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
  (hC : IsClopen C) (hh : a ∈ C ∧ b ∈ Cᶜ), False
Tactic: obtain ⟨C, hC, hh⟩ := exists_isClopen_of_totally_separated hn
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
S : Profinite
a b : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
h : ι S a = ι S b
hn : ¬a = b
C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ False
have hf : decide (b ∈ C) = true
Tactic: apply hh.2 ∘ of_decide_eq_true
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
S : Profinite
a b : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
h :
  Eq.{u + 1} (α :=
    { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
        IsClopen C } →
      Bool)
    (fun
        (C :
          { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
            IsClopen C }) ↦
      decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
    fun
      (C :
        { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
          IsClopen C }) ↦
    decide (b ∈ (↑C : Set (↑S.toTop : Type u)))
hn : ¬a = b
C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ decide (b ∈ C) = true
have hf : decide
    (a ∈
      (↑(Subtype.mk (p :=
            fun
              (C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
            IsClopen C) C hC) :
        Set (↑S.toTop : Type u))) =
  true
Tactic: rw [← congr_fun h ⟨C, hC⟩]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Induction (goal)
Goal:
S : Profinite
⊢ Free.{0, u} ℤ
    (LocallyConstant (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) ℤ)
have obtain : ∀
  (w :
    LinearOrder
      { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
        IsClopen C }),
  WellFoundedLT.{u}
      { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
        IsClopen C } →
    Free.{0, u} ℤ
      (LocallyConstant (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) ℤ)
Tactic: obtain ⟨_, _⟩ := exists_wellFoundedLT {C : Set S // IsClopen C}
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
l : Products I
hl : Products.isGood (π C fun (x : I) ↦ x ∈ s) l
⊢ Products.eval C l =
    (πJ C s : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
      (Products.eval (π C fun (x : I) ↦ x ∈ s) l)
have h : ∀ (f : (↑C : Type u)),
  Eq (α := ℤ) ((Products.eval C l : (a : (↑C : Type u)) → ℤ) f : ℤ)
    ((((πJ C s : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
              (Products.eval (π C fun (x : I) ↦ x ∈ s) l) :
            LocallyConstant (↑C : Type u) ℤ) :
          (a : (↑C : Type u)) → ℤ)
        f :
      ℤ)
Tactic: ext f
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
l : Products I
hl : Products.isGood (π C fun (x : I) ↦ x ∈ s) l
f : (↑C : Type u)
⊢ Eq (α := ℤ) ((Products.eval C l : (a : (↑C : Type u)) → ℤ) f : ℤ)
    ((((πJ C s : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
              (Products.eval (π C fun (x : I) ↦ x ∈ s) l) :
            LocallyConstant (↑C : Type u) ℤ) :
          (a : (↑C : Type u)) → ℤ)
        f :
      ℤ)
have h : Eq (α := ℤ) ((Products.eval C l : (a : (↑C : Type u)) → ℤ) f : ℤ)
  ((Products.eval (π C fun (x : I) ↦ x ∈ s) l : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
      (({ toFun := ProjRestrict C fun (x : I) ↦ x ∈ s, continuous_toFun := sorry } :
            (a : (↑C : Type u)) → (↑(π C fun (x : I) ↦ x ∈ s) : Type u))
          f :
        (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) :
    ℤ)
Tactic: simp only [πJ, LocallyConstant.comapₗ, LinearMap.coe_mk, AddHom.coe_mk,
    LocallyConstant.coe_comap, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u) → ↥s → Bool :=
  fun (x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (j : ↥s) ↦ (↑x : I → Bool) (↑j : I)
⊢ Fintype (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
have refine : Function.Injective f
Tactic: refine Fintype.ofInjective f ?_
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u) → ↥s → Bool :=
  fun (x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (j : ↥s) ↦ (↑x : I → Bool) (↑j : I)
x : I → Bool
hx : x ∈ C
⊢ ∀ ⦃a₂ : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)⦄,
    f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) = f a₂ →
      Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯ = a₂
have this : ∀ (y : I → Bool) (hy : y ∈ C),
  f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) sorry) =
      f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) sorry) →
    Eq (α := (↑(π C fun (x : I) ↦ x ∈ s) : Type u))
      (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) sorry)
      (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) sorry)
Tactic: ⟨_, y, hy, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u) → ↥s → Bool :=
  fun (x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (j : ↥s) ↦ (↑x : I → Bool) (↑j : I)
x : I → Bool
hx : x ∈ C
y : I → Bool
hy : y ∈ C
h :
  f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) =
    f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯)
⊢ Eq (α := (↑(π C fun (x : I) ↦ x ∈ s) : Type u))
    (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯)
    (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯)
have a : ∀ (i : I),
  (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) sorry) : I → Bool)
      i =
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) sorry) : I → Bool)
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u) → ↥s → Bool :=
  fun (x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (j : ↥s) ↦ (↑x : I → Bool) (↑j : I)
x : I → Bool
hx : x ∈ C
y : I → Bool
hy : y ∈ C
h :
  f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) =
    f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯)
i : I
⊢ (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) : I → Bool)
      i =
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯) : I → Bool)
      i
have pos : ∀ (hi : i ∈ s),
  (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) sorry) : I → Bool)
      i =
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) sorry) : I → Bool)
      i
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u) → ↥s → Bool :=
  fun (x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (j : ↥s) ↦ (↑x : I → Bool) (↑j : I)
x : I → Bool
hx : x ∈ C
y : I → Bool
hy : y ∈ C
h :
  f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) =
    f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯)
i : I
pos :
  ∀ (hi : i ∈ s),
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) : I → Bool)
        i =
      (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯) :
          I → Bool)
        i
⊢ (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) : I → Bool)
      i =
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯) : I → Bool)
      i
have neg : ∀ (hi : i ∉ s),
  (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) sorry) : I → Bool)
      i =
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) sorry) : I → Bool)
      i
Tactic: by_cases hi : i ∈ s
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ
h : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤ f
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (Submodule.span ℤ (Set.range (spanFinBasis C s))) f
have rw : ∃ (c : (↑(π C fun (x : I) ↦ x ∈ s) : Type u) →₀ ℤ),
  (c.sum fun (i : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (a : ℤ) ↦ a • spanFinBasis C s i) = f
Tactic: rw [Finsupp.mem_span_range_iff_exists_finsupp]