awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Extend
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
S : Profinite
i : DiscreteQuotient (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
⊢ Epi (S.asLimitCone.π.app i)

Tactic:
(epi_iff_surjective _).mpr i.proj_surjective

Premises used: Iff.mpr, Profinite.epi_iff_surjective, DiscreteQuotient.proj_surjective
-- Module: Mathlib.Topology.Category.Profinite.Limits
Goal:
⊢ FinitaryExtensive Profinite

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Category.Profinite.Limits
Goal:
⊢ PreservesFiniteCoproducts profiniteToCompHaus

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
J : I → Prop
inst : (i : I) → Decidable (J i)
h : ∀ (i : I), Continuous (Y := Bool) fun (a : I → Bool) ↦ if J i then a i else false
⊢ Continuous (Y := I → Bool) fun (c : I → Bool) (i : I) ↦ if J i then c i else false

Tactic:
apply continuous_pi

Premises used: continuous_pi
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
J : I → Prop
inst : (i : I) → Decidable (J i)
i : I
h : J i → Continuous (Y := Bool) fun (a : I → Bool) ↦ a i
h₁ : ¬J i → Continuous (Y := Bool) fun (a : I → Bool) ↦ false
⊢ Continuous (Y := Bool) fun (a : I → Bool) ↦ if J i then a i else false

Tactic:
split
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
J : I → Prop
inst : (i : I) → Decidable (J i)
i : I
h : J i
⊢ Continuous (Y := Bool) fun (a : I → Bool) ↦ a i

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
J : I → Prop
inst : (i : I) → Decidable (J i)
i : I
h : ¬J i
⊢ Continuous (Y := Bool) fun (a : I → Bool) ↦ false

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
⊢ Continuous (Y := (↑(π C J) : Type u)) (ProjRestrict C J)

Tactic:
Continuous.restrict _ (continuous_proj _)

Premises used: Continuous.restrict, Profinite.NobelingProof.ProjRestrict, Profinite.NobelingProof.continuous_proj
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
J : I → Prop
inst : (i : I) → Decidable (J i)
x : I → Bool
h : ∀ (i : I), x i ≠ false → J i
h₁ : ∀ (i : I), Proj J x i = x i
⊢ Proj J x = x

Tactic:
ext i
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
J : I → Prop
inst : (i : I) → Decidable (J i)
x : I → Bool
h : ∀ (i : I), x i ≠ false → J i
i : I
h₁ : ¬J i → false = x i
⊢ Proj J x i = x i

Tactic:
simp only [Proj, ite_eq_left_iff]

Premises used: ite_eq_left_iff, Profinite.NobelingProof.Proj
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
J : I → Prop
inst : (i : I) → Decidable (J i)
x : I → Bool
h : ∀ (i : I), x i ≠ false → J i
i : I
h₁ : false ≠ x i → J i
⊢ ¬J i → false = x i

Tactic:
contrapose!
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
J : I → Prop
inst : (i : I) → Decidable (J i)
x : I → Bool
h : ∀ (i : I), x i ≠ false → J i
i : I
⊢ false ≠ x i → J i

Tactic:
simpa only [ne_comm] using h i

Premises used: ne_comm
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
h : ∀ (x : I → Bool), x ∈ π C J ↔ x ∈ C
⊢ π C J = C

Tactic:
ext x
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
⊢ x ∈ π C J ↔ x ∈ C

Tactic:
⟨fun ⟨y, hy, h⟩ ↦ ?_, fun h ↦ ⟨x, h, ?_⟩⟩

Premises used: _private.0.Profinite.NobelingProof.proj_prop_eq_self.match_1, Membership.mem, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
h : x ∈ π C J → ∀ (y : I → Bool) (hy : y ∈ C) (h : Proj J y = x), x ∈ C
h₁ : ∀ (h : x ∈ C), Proj J x = x
⊢ x ∈ π C J ↔ x ∈ C

Tactic:
refine ⟨fun ⟨y, hy, h⟩ ↦ ?_, fun h ↦ ⟨x, h, ?_⟩⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
h_1 : x ∈ π C J
y : I → Bool
hy : y ∈ C
h : Proj J y = x
h₁ : ∀ (i : I), y i ≠ false → J i
⊢ x ∈ C

Tactic:
rwa [← h, proj_eq_self]

Premises used: Profinite.NobelingProof.proj_eq_self
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
h_1 : x ∈ π C J
y : I → Bool
hy : y ∈ C
h : Proj J y = x
⊢ ∀ (i : I), y i ≠ false → J i

Tactic:
(hh · y hy)
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
h_1 : x ∈ π C J
y : I → Bool
hy : y ∈ C
h : Proj J y = x
⊢ ∀ (i : I), y i ≠ false → J i

Tactic:
exact (hh · y hy)
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
h : x ∈ C
h₁ : ∀ (i : I), x i ≠ false → J i
⊢ Proj J x = x

Tactic:
rw [proj_eq_self]

Premises used: Profinite.NobelingProof.proj_eq_self
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
h : x ∈ C
⊢ ∀ (i : I), x i ≠ false → J i

Tactic:
(hh · x h)
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
h : x ∈ C
⊢ ∀ (i : I), x i ≠ false → J i

Tactic:
exact (hh · x h)
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
h₁ : ∀ (x : I → Bool) (i : I), (Proj J ∘ Proj K) x i = Proj J x i
⊢ Proj J ∘ Proj K = Proj J

Tactic:
ext x i
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : I → Bool
i : I
h₁ : (if J i then if K i then x i else false else false) = if J i then x i else false
⊢ (Proj J ∘ Proj K) x i = Proj J x i

Tactic:
dsimp [Proj]

Premises used: Profinite.NobelingProof.Proj
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : I → Bool
i : I
⊢ (if J i then if K i then x i else false else false) = if J i then x i else false

Tactic:
simp_all
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
h₁ : ∀ (x : I → Bool), x ∈ π (π C K) J ↔ x ∈ π C J
⊢ π (π C K) J = π C J

Tactic:
ext x
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : I → Bool
⊢ x ∈ π (π C K) J ↔ x ∈ π C J

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : I → Bool
h₁ : ∀ (h : x ∈ π (π C K) J), x ∈ π C J
h₂ : ∀ (h : x ∈ π C J), x ∈ π (π C K) J
⊢ x ∈ π (π C K) J ↔ x ∈ π C J

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h_1 : ∀ (i : I), J i → K i
x : I → Bool
h : x ∈ π (π C K) J
h₁ : ∀ (z : I → Bool) (hz : z ∈ C), Proj J (Proj K z) ∈ π C J
⊢ x ∈ π C J

Tactic:
obtain ⟨y, ⟨z, hz, rfl⟩, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
z : I → Bool
hz : z ∈ C
⊢ Proj J (Proj K z) ∈ π C J

Tactic:
⟨z, hz, (?_ : _ = (Proj J ∘ Proj K) z)⟩

Premises used: Set.Mem, setOf, Profinite.NobelingProof.π, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
z : I → Bool
hz : z ∈ C
h₁ : Proj J z = (Proj J ∘ Proj K) z
⊢ Proj J (Proj K z) ∈ π C J

Tactic:
refine ⟨z, hz, (?_ : _ = (Proj J ∘ Proj K) z)⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
z : I → Bool
hz : z ∈ C
h₁ h₂ : Proj J z = Proj J z
⊢ Proj J z = (Proj J ∘ Proj K) z

Tactic:
rw [proj_comp_of_subset J K h]

Premises used: Profinite.NobelingProof.proj_comp_of_subset
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h_1 : ∀ (i : I), J i → K i
x : I → Bool
h : x ∈ π C J
h₁ : ∀ (y : I → Bool) (hy : y ∈ C), Proj J y ∈ π (π C K) J
⊢ x ∈ π (π C K) J

Tactic:
obtain ⟨y, hy, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
y : I → Bool
hy : y ∈ C
h₁ : Proj J y ∈ Proj J ∘ Proj K '' C
⊢ Proj J y ∈ Proj J '' Proj K '' C

Tactic:
rw [← Set.image_comp]

Premises used: Set.image_comp
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
y : I → Bool
hy : y ∈ C
⊢ Proj J y ∈ Proj J ∘ Proj K '' C

Tactic:
⟨y, hy, ?_⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
y : I → Bool
hy : y ∈ C
h₁ : (Proj J ∘ Proj K) y = Proj J y
⊢ Proj J y ∈ Proj J ∘ Proj K '' C

Tactic:
refine ⟨y, hy, ?_⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
y : I → Bool
hy : y ∈ C
h₁ h₂ : Proj J y = Proj J y
⊢ (Proj J ∘ Proj K) y = Proj J y

Tactic:
rw [proj_comp_of_subset J K h]

Premises used: Profinite.NobelingProof.proj_comp_of_subset
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
⊢ Continuous (X := (↑(π C K) : Type u)) (Y := (↑(π C J) : Type u)) (ProjRestricts C (J := J) (K := K) h)

Tactic:
Continuous.comp (Homeomorph.continuous _) (continuous_projRestrict _ _)

Premises used: Homeomorph.continuous, Continuous.comp, Profinite.NobelingProof.continuous_projRestrict, Profinite.NobelingProof.ProjRestricts
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
⊢ Function.Surjective (α := (↑(π C K) : Type u)) (β := (↑(π C J) : Type u)) (ProjRestricts C (J := J) (K := K) h)

Tactic:
(Homeomorph.surjective _).comp (Set.surjective_mapsTo_image_restrict _ _)

Premises used: Set.surjective_mapsTo_image_restrict, Profinite.NobelingProof.ProjRestricts, Function.Surjective.comp, Homeomorph.surjective
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
h :
  ∀ (y : I → Bool) (hy : y ∈ C) (i : I),
    (↑(ProjRestricts C (J := J) (K := J) ⋯ (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J y) ⋯)) : I → Bool)
        i =
      (↑(id (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J y) ⋯)) : I → Bool) i
⊢ Eq (α := (↑(π C J) : Type u) → (↑(π C J) : Type u)) (ProjRestricts C (J := J) (K := J) ⋯) id

Tactic:
ext ⟨x, y, hy, rfl⟩ i

Premises used: rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
y : I → Bool
hy : y ∈ C
i : I
⊢ (↑(ProjRestricts C (J := J) (K := J) ⋯ (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J y) ⋯)) : I → Bool)
      i =
    (↑(id (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J y) ⋯)) : I → Bool) i

Tactic:
simp +contextual only [π, Proj, ProjRestricts_coe, id_eq, if_true]

Premises used: if_true, Profinite.NobelingProof.π, Profinite.NobelingProof.Proj, Profinite.NobelingProof.ProjRestricts_coe, id_eq
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
hJK : ∀ (i : I), J i → K i
hKL : ∀ (i : I), K i → L i
h :
  ∀ (x : (↑(π C L) : Type u)) (i : I),
    (↑(Function.comp (β := (↑(π C K) : Type u)) (ProjRestricts C (J := J) (K := K) hJK)
              (ProjRestricts C (J := K) (K := L) hKL) x) :
          I → Bool)
        i =
      (↑(ProjRestricts C (J := J) (K := L) ⋯ x) : I → Bool) i
⊢ Eq (α := (↑(π C L) : Type u) → (↑(π C J) : Type u))
    (Function.comp (β := (↑(π C K) : Type u)) (ProjRestricts C (J := J) (K := K) hJK)
      (ProjRestricts C (J := K) (K := L) hKL))
    (ProjRestricts C (J := J) (K := L) ⋯)

Tactic:
ext x i
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
hJK : ∀ (i : I), J i → K i
hKL : ∀ (i : I), K i → L i
x : (↑(π C L) : Type u)
i : I
h : (if J i then if K i then (↑x : I → Bool) i else false else false) = if J i then (↑x : I → Bool) i else false
⊢ (↑(Function.comp (β := (↑(π C K) : Type u)) (ProjRestricts C (J := J) (K := K) hJK)
            (ProjRestricts C (J := K) (K := L) hKL) x) :
        I → Bool)
      i =
    (↑(ProjRestricts C (J := J) (K := L) ⋯ x) : I → Bool) i

Tactic:
simp only [π, Proj, Function.comp_apply, ProjRestricts_coe]

Premises used: Profinite.NobelingProof.π, Profinite.NobelingProof.Proj, Profinite.NobelingProof.ProjRestricts_coe, Function.comp_apply
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
hJK : ∀ (i : I), J i → K i
hKL : ∀ (i : I), K i → L i
x : (↑(π C L) : Type u)
i : I
⊢ (if J i then if K i then (↑x : I → Bool) i else false else false) = if J i then (↑x : I → Bool) i else false

Tactic:
simp_all
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
h₁ :
  ∀ (x : (↑C : Type u)) (i : I),
    (↑(Function.comp (β := (↑(π C K) : Type u)) (ProjRestricts C (J := J) (K := K) h) (ProjRestrict C K) x) : I → Bool)
        i =
      (↑(ProjRestrict C J x) : I → Bool) i
⊢ Eq (α := (↑C : Type u) → (↑(π C J) : Type u))
    (Function.comp (β := (↑(π C K) : Type u)) (ProjRestricts C (J := J) (K := K) h) (ProjRestrict C K))
    (ProjRestrict C J)

Tactic:
ext x i
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : (↑C : Type u)
i : I
h₁ : (if J i then if K i then (↑x : I → Bool) i else false else false) = if J i then (↑x : I → Bool) i else false
⊢ (↑(Function.comp (β := (↑(π C K) : Type u)) (ProjRestricts C (J := J) (K := K) h) (ProjRestrict C K) x) : I → Bool)
      i =
    (↑(ProjRestrict C J x) : I → Bool) i

Tactic:
simp only [π, Proj, Function.comp_apply, ProjRestricts_coe, ProjRestrict_coe]

Premises used: Profinite.NobelingProof.π, Profinite.NobelingProof.ProjRestrict_coe, Profinite.NobelingProof.Proj, Profinite.NobelingProof.ProjRestricts_coe, Function.comp_apply
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : (↑C : Type u)
i : I
⊢ (if J i then if K i then (↑x : I → Bool) i else false else false) = if J i then (↑x : I → Bool) i else false

Tactic:
simp_all
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
x : (↑(π C J) : Type u)
rcases :
  ∀ (y : I → Bool) (hy : y ∈ C),
    (fun (i : { i : I // J i }) ↦
        (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J y) ⋯) : I → Bool) (↑i : I)) ∈
      IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J
⊢ (fun (i : { i : I // J i }) ↦ (↑x : I → Bool) (↑i : I)) ∈ IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J

Tactic:
rcases x with ⟨x, y, hy, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
y : I → Bool
hy : y ∈ C
⊢ (fun (i : { i : I // J i }) ↦
      (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J y) ⋯) : I → Bool) (↑i : I)) ∈
    IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J

Tactic:
⟨y, hy, ?_⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, Profinite.IndexFunctor.obj
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
y : I → Bool
hy : y ∈ C
refine :
  Eq (α := (i : { i : I // J i }) → (fun (i : I) ↦ Bool) (↑i : I))
    ((precomp (X := fun (i : I) ↦ Bool) (Subtype.val (p := J)) :
          (a : (i : I) → (fun (i : I) ↦ Bool) i) → (i : Subtype J) → (fun (i : I) ↦ Bool) (↑i : I))
        y :
      (i : Subtype J) → (fun (i : I) ↦ Bool) (↑i : I))
    fun (i : { i : I // J i }) ↦ (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J y) ⋯) : I → Bool) (↑i : I)
⊢ (fun (i : { i : I // J i }) ↦
      (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J y) ⋯) : I → Bool) (↑i : I)) ∈
    IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J

Tactic:
refine ⟨y, hy, ?_⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
y : I → Bool
hy : y ∈ C
h :
  ∀ (i : I) (hi : J i),
    (precomp (X := fun (i : I) ↦ Bool) (Subtype.val (p := J)) :
          (a : (i : I) → (fun (i : I) ↦ Bool) i) → (i : Subtype J) → (fun (i : I) ↦ Bool) (↑i : I))
        y (Subtype.mk (p := J) i hi) =
      (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J y) ⋯) : I → Bool) (↑(Subtype.mk (p := J) i hi) : I)
⊢ Eq (α := (i : { i : I // J i }) → (fun (i : I) ↦ Bool) (↑i : I))
    ((precomp (X := fun (i : I) ↦ Bool) (Subtype.val (p := J)) :
          (a : (i : I) → (fun (i : I) ↦ Bool) i) → (i : Subtype J) → (fun (i : I) ↦ Bool) (↑i : I))
        y :
      (i : Subtype J) → (fun (i : I) ↦ Bool) (↑i : I))
    fun (i : { i : I // J i }) ↦ (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J y) ⋯) : I → Bool) (↑i : I)

Tactic:
ext ⟨i, hi⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
y : I → Bool
hy : y ∈ C
i : I
hi : J i
⊢ (precomp (X := fun (i : I) ↦ Bool) (Subtype.val (p := J)) :
        (a : (i : I) → (fun (i : I) ↦ Bool) i) → (i : Subtype J) → (fun (i : I) ↦ Bool) (↑i : I))
      y (Subtype.mk (p := J) i hi) =
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J y) ⋯) : I → Bool) (↑(Subtype.mk (p := J) i hi) : I)

Tactic:
simp [precomp, Proj, hi]

Premises used: Profinite.NobelingProof.Proj, ContinuousMap.precomp
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
⊢ Continuous (Y := (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J) : Type u)) fun (x : (↑(π C J) : Type u)) ↦
    Subtype.mk (p := fun (x : (i : { i : I // J i }) → Bool) ↦ x ∈ IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J)
      (fun (i : { i : I // J i }) ↦ (↑x : I → Bool) (↑i : I)) ⋯

Tactic:
Continuous.subtype_mk (continuous_pi fun i ↦ ?_) _

Premises used: continuous_pi, Continuous.subtype_mk
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
refine : ∀ (i : { i : I // J i }), Continuous (Y := Bool) fun (a : (↑(π C J) : Type u)) ↦ (↑a : I → Bool) (↑i : I)
⊢ Continuous (Y := (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J) : Type u)) fun (x : (↑(π C J) : Type u)) ↦
    Subtype.mk (p := fun (x : (i : { i : I // J i }) → Bool) ↦ x ∈ IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J)
      (fun (i : { i : I // J i }) ↦ (↑x : I → Bool) (↑i : I)) ⋯

Tactic:
refine Continuous.subtype_mk (continuous_pi fun i ↦ ?_) _

Premises used: continuous_pi, Continuous.subtype_mk
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
i : { i : I // J i }
⊢ Continuous (Y := Bool) fun (a : (↑(π C J) : Type u)) ↦ (↑a : I → Bool) (↑i : I)

Tactic:
(continuous_apply i.val).comp continuous_subtype_val

Premises used: continuous_subtype_val, Continuous.comp, continuous_apply, Subtype.val
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
i : { i : I // J i }
⊢ Continuous (Y := Bool) fun (a : (↑(π C J) : Type u)) ↦ (↑a : I → Bool) (↑i : I)

Tactic:
exact (continuous_apply i.val).comp continuous_subtype_val

Premises used: continuous_subtype_val, Continuous.comp, continuous_apply, Subtype.val
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
⊢ Function.Bijective (α := (↑(π C J) : Type u)) (β := (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J) : Type u))
    (⇑(iso_map C J) : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u))

Tactic:
⟨fun a b h ↦ ?_, fun a ↦ ?_⟩

Premises used: And.intro, Function.Bijective