awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
h : 0 ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h_1 : IsClosed (X := I → Bool) {fun (x : I) ↦ false}
hsC : contained (I := I) {fun (x : I) ↦ false} 0
⊢ LinearIndependent (ι := { l : Products I // Products.isGood {fun (x : I) ↦ false} l }) ℤ (eval {fun (x : I) ↦ false})

Tactic:
linearIndependentSingleton

Premises used: Profinite.NobelingProof.GoodProducts.linearIndependentSingleton
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
h : 0 ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h_1 : IsClosed (X := I → Bool) {fun (x : I) ↦ false}
hsC : contained (I := I) {fun (x : I) ↦ false} 0
⊢ LinearIndependent (ι := { l : Products I // Products.isGood {fun (x : I) ↦ false} l }) ℤ (eval {fun (x : I) ↦ false})

Tactic:
exact linearIndependentSingleton

Premises used: Profinite.NobelingProof.GoodProducts.linearIndependentSingleton
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C o
rw :
  LinearIndepOn.{u, 0, u} (ι := LocallyConstant (↑C : Type u) ℤ) ℤ id
    (⋃ (e : { o' : Ordinal.{u} // o' < o }), smaller C (↑e : Ordinal.{u}))
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)

Tactic:
rw [linearIndependent_iff_union_smaller C ho hsC, linearIndependent_subtype_iff]

Premises used: Profinite.NobelingProof.GoodProducts.linearIndependent_iff_union_smaller, linearIndependent_subtype_iff
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C o
⊢ LinearIndepOn.{u, 0, u} (ι := LocallyConstant (↑C : Type u) ℤ) ℤ id
    (⋃ (e : { o' : Ordinal.{u} // o' < o }), smaller C (↑e : Ordinal.{u}))

Tactic:
linearIndepOn_iUnion_of_directed
    (Monotone.directed_le fun _ _ h ↦ GoodProducts.smaller_mono C h) fun ⟨o', ho'⟩ ↦
    (linearIndependent_iff_smaller _ _).mp (h o' ho' (ho'.le.trans hho)
    (π C (ord I · < o')) (isClosed_proj _ _ hC) (contained_proj _ _))

Premises used: Profinite.NobelingProof.GoodProducts.smaller, linearIndepOn_iUnion_of_directed, Profinite.NobelingProof.π, _private.0.Profinite.NobelingProof.GoodProducts.Plimit.match_1, id, LT.lt.le, Int, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller, Subtype.mk, Profinite.NobelingProof.ord, Profinite.NobelingProof.isClosed_proj, Profinite.NobelingProof.GoodProducts.smaller_mono, LT.lt, Profinite.NobelingProof.contained_proj, Iff.mp, LE.le.trans, Monotone.directed_le, Subtype.val, LinearIndepOn
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C o
⊢ LinearIndepOn.{u, 0, u} (ι := LocallyConstant (↑C : Type u) ℤ) ℤ id
    (⋃ (e : { o' : Ordinal.{u} // o' < o }), smaller C (↑e : Ordinal.{u}))

Tactic:
exact linearIndepOn_iUnion_of_directed
    (Monotone.directed_le fun _ _ h ↦ GoodProducts.smaller_mono C h) fun ⟨o', ho'⟩ ↦
    (linearIndependent_iff_smaller _ _).mp (h o' ho' (ho'.le.trans hho)
    (π C (ord I · < o')) (isClosed_proj _ _ hC) (contained_proj _ _))
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
μ : Ordinal.{u}
⊢ P I μ

Tactic:
Ordinal.limitRecOn μ P0 (fun o h ho C hC hsC ↦ ?_)
      (fun o ho h ↦ (GoodProducts.Plimit o ho (fun o' ho' ↦ (h o' ho'))))

Premises used: Ordinal.limitRecOn
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
μ : Ordinal.{u}
refine :
  ∀ (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)
⊢ P I μ

Tactic:
refine Ordinal.limitRecOn μ P0 (fun o h ho C hC hsC ↦ ?_)
      (fun o ho h ↦ (GoodProducts.Plimit o ho (fun o' ho' ↦ (h o' ho'))))
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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)
⊢ 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
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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
rw :
  LinearIndependent (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho') : Type u))
    ℤ (SumEval C ho')
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)

Tactic:
rw [linearIndependent_iff_sum C hsC ho']

Premises used: Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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')

Tactic:
ModuleCat.linearIndependent_leftExact (succ_exact C hC hsC ho') ?_ ?_ (succ_mono C o)
    (square_commutes C ho')

Premises used: Profinite.NobelingProof.succ_exact, Profinite.NobelingProof.GoodProducts.square_commutes, ModuleCat.linearIndependent_leftExact, Profinite.NobelingProof.succ_mono
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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))
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 := ⋯ : 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 := ⋯ :
                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 := ⋯ }.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 := ⋯ }.X₃ :
            Type u)) ∘
      SumEval C ho' ∘ Sum.inr)
⊢ LinearIndependent (ι := (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u) ⊕ (↑(MaxProducts C ho') : Type u))
    ℤ (SumEval C ho')

Tactic:
refine ModuleCat.linearIndependent_leftExact (succ_exact C hC hsC ho') ?_ ?_ (succ_mono C o)
    (square_commutes C ho')

Premises used: Profinite.NobelingProof.succ_exact, Profinite.NobelingProof.GoodProducts.square_commutes, ModuleCat.linearIndependent_leftExact, Profinite.NobelingProof.succ_mono
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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)) ℤ
    (eval (π C fun (x : I) ↦ ord I x < o))

Tactic:
h (le_of_lt ho') (π C (ord I · < o)) (isClosed_proj C o hC) (contained_proj C o)

Premises used: Profinite.NobelingProof.Products.isGood, Set.Mem, setOf, Profinite.NobelingProof.π, le_of_lt, Profinite.NobelingProof.ord, Profinite.NobelingProof.isClosed_proj, LT.lt, Profinite.NobelingProof.contained_proj, Profinite.NobelingProof.GoodProducts, Not
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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)) ℤ
    (eval (π C fun (x : I) ↦ ord I x < o))

Tactic:
exact h (le_of_lt ho') (π C (ord I · < o)) (isClosed_proj C o hC) (contained_proj C o)

Premises used: Profinite.NobelingProof.π, le_of_lt, Profinite.NobelingProof.ord, Profinite.NobelingProof.isClosed_proj, LT.lt, Profinite.NobelingProof.contained_proj
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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 (ι := (↑(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 := ⋯ : 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 := ⋯ :
                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 := ⋯ }.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 := ⋯ }.X₃ :
            Type u)) ∘
      SumEval C ho' ∘ Sum.inr)

Tactic:
linearIndependent_comp_of_eval C hC hsC ho' (span (π C (ord I · < o))
      (isClosed_proj C o hC)) (h (le_of_lt ho') (C' C ho') (isClosed_C' C hC ho')
      (contained_C' C ho'))

Premises used: Profinite.NobelingProof.GoodProducts.linearIndependent_comp_of_eval, Profinite.NobelingProof.π, le_of_lt, Profinite.NobelingProof.GoodProducts.span, Profinite.NobelingProof.ord, Profinite.NobelingProof.isClosed_proj, Profinite.NobelingProof.isClosed_C', LT.lt, Profinite.NobelingProof.contained_C', Profinite.NobelingProof.C'
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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 (ι := (↑(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 := ⋯ : 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 := ⋯ :
                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 := ⋯ }.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 := ⋯ }.X₃ :
            Type u)) ∘
      SumEval C ho' ∘ Sum.inr)

Tactic:
exact linearIndependent_comp_of_eval C hC hsC ho' (span (π C (ord I · < o))
      (isClosed_proj C o hC)) (h (le_of_lt ho') (C' C ho') (isClosed_C' C hC ho')
      (contained_C' C ho'))

Premises used: Profinite.NobelingProof.GoodProducts.linearIndependent_comp_of_eval, Profinite.NobelingProof.π, le_of_lt, Profinite.NobelingProof.GoodProducts.span, Profinite.NobelingProof.ord, Profinite.NobelingProof.isClosed_proj, Profinite.NobelingProof.isClosed_C', LT.lt, Profinite.NobelingProof.contained_C', Profinite.NobelingProof.C'
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
hC : IsClosed C
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C)

Tactic:
GoodProducts.linearIndependentAux (Ordinal.type (· < · : I → I → Prop)) (le_refl _)
    C hC (fun _ _ _ _ ↦ Ordinal.typein_lt_type _ _)

Premises used: le_refl, Ordinal.typein_lt_type, Ordinal.type, LT.lt, Profinite.NobelingProof.GoodProducts.linearIndependentAux
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
S : Profinite
ι : (↑(S.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1) → I → Bool
hι : IsClosedEmbedding ι
⊢ Free.{0, u_1} ℤ
    (LocallyConstant
      (↑(S.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1) ℤ)

Tactic:
Module.Free.of_equiv'
  (Module.Free.of_basis <| GoodProducts.Basis _ hι.isClosed_range) (LocallyConstant.congrLeftₗ ℤ
    hι.isEmbedding.toHomeomorph).symm

Premises used: LinearEquiv.symm, Int, Topology.IsClosedEmbedding.isEmbedding, Profinite.NobelingProof.GoodProducts.Basis, Module.Free.of_equiv', Module.Free.of_basis, Topology.IsClosedEmbedding.isClosed_range, LocallyConstant.congrLeftₗ, Topology.IsEmbedding.toHomeomorph
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
h : Continuous (ι S)
hf : Function.Injective (ι S)
⊢ IsClosedEmbedding (ι S)

Tactic:
apply Continuous.isClosedEmbedding

Premises used: Continuous.isClosedEmbedding
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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)))

Tactic:
continuous_pi ?_

Premises used: continuous_pi
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
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)))
⊢ 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)))

Tactic:
refine continuous_pi ?_

Premises used: continuous_pi
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
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)))
⊢ 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)))

Tactic:
rw [← IsLocallyConstant.iff_continuous]

Premises used: IsLocallyConstant.iff_continuous
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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)))

Tactic:
((IsLocallyConstant.tfae _).out 0 3).mpr ?_

Premises used: Iff.mpr, IsLocallyConstant.tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
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})
⊢ 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:
refine ((IsLocallyConstant.tfae _).out 0 3).mpr ?_

Premises used: Iff.mpr, IsLocallyConstant.tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
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})

Tactic:
IsClopen.isOpen (isClopen_compl_iff.mp ?_)

Premises used: isClopen_compl_iff, IsClopen.isOpen, Iff.mp
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
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})ᶜ
⊢ 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})

Tactic:
refine IsClopen.isOpen (isClopen_compl_iff.mp ?_)

Premises used: isClopen_compl_iff, IsClopen.isOpen, Iff.mp
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
⊢ IsClopen (↑C : Set (↑S.toTop : Type u))

Tactic:
C.2

Premises used: Subtype.property
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
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))
⊢ 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:
convert! C.2

Premises used: Subtype.property