awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
⊢ x ∈ π C J ↔ x ∈ C
have h₁ : ∀ (h : x ∈ C), Proj J x = x
Tactic: refine ⟨fun ⟨y, hy, h⟩ ↦ ?_, fun h ↦ ⟨x, h, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
⊢ x ∈ C
have h₁ : ∀ (i : I), y i ≠ false → J i
Tactic: rwa [← h, proj_eq_self]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
⊢ Proj J x = x
have h₁ : ∀ (i : I), x i ≠ false → J i
Tactic: rw [proj_eq_self]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
⊢ Proj J ∘ Proj K = Proj J
have h₁ : ∀ (x : I → Bool) (i : I), (Proj J ∘ Proj K) x i = Proj J x i
Tactic: ext x i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
⊢ (Proj J ∘ Proj K) x i = Proj J x i
have h₁ : (if J i then if K i then x i else false else false) = if J i then x i else false
Tactic: dsimp [Proj]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
⊢ π (π C K) J = π C J
have h₁ : ∀ (x : I → Bool), x ∈ π (π C K) J ↔ x ∈ π C J
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
have h₁ : ∀ (h : x ∈ π (π C K) J), x ∈ π C J
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
⊢ x ∈ π (π C K) J ↔ x ∈ π C J
have h₂ : ∀ (h : x ∈ π C J), x ∈ π (π C K) J
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
⊢ x ∈ π C J
have h₁ : ∀ (z : I → Bool) (hz : z ∈ C), Proj J (Proj K z) ∈ π C J
Tactic: obtain ⟨y, ⟨z, hz, rfl⟩, rfl⟩ := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
have h₁ : Proj J z = (Proj J ∘ Proj K) z
Tactic: refine ⟨z, hz, (?_ : _ = (Proj J ∘ Proj K) z)⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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 z = (Proj J ∘ Proj K) z
have h₁ : Proj J z = Proj J z
Tactic: rw [proj_comp_of_subset J K h]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
⊢ x ∈ π (π C K) J
have h₁ : ∀ (y : I → Bool) (hy : y ∈ C), Proj J y ∈ π (π C K) J
Tactic: obtain ⟨y, hy, rfl⟩ := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
have h₁ : Proj J y ∈ Proj J ∘ Proj K '' C
Tactic: rw [← Set.image_comp]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
have h₁ : (Proj J ∘ Proj K) y = Proj J y
Tactic: refine ⟨y, hy, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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 ∘ Proj K) y = Proj J y
have h₁ : Proj J y = Proj J y
Tactic: rw [proj_comp_of_subset J K h]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
⊢ Eq (α := (↑(π C J) : Type u) → (↑(π C J) : Type u)) (ProjRestricts C (J := J) (K := J) ⋯) id
have h : ∀ (y : I → Bool) (hy : y ∈ C) (i : I),
  (↑(ProjRestricts C (J := J) (K := J) sorry (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J y) sorry)) : I → Bool)
      i =
    (↑(id (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J y) sorry)) : I → Bool) i
Tactic: ext ⟨x, y, hy, rfl⟩ i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
⊢ 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) ⋯)
have 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) sorry x) : I → Bool) i
Tactic: ext x i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
⊢ (↑(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
have 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
Tactic: simp only [π, Proj, Function.comp_apply, ProjRestricts_coe]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
⊢ 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)
have 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
Tactic: ext x i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
⊢ (↑(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
have 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
Tactic: simp only [π, Proj, Function.comp_apply, ProjRestricts_coe, ProjRestrict_coe]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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)
⊢ (fun (i : { i : I // J i }) ↦ (↑x : I → Bool) (↑i : I)) ∈ IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J
have 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) sorry) : I → Bool) (↑i : I)) ∈
    IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J
Tactic: rcases x with ⟨x, y, hy, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
have 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) sorry) : I → Bool) (↑i : I)
Tactic: refine ⟨y, hy, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
⊢ 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)
have 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) sorry) : I → Bool) (↑(Subtype.mk (p := J) i hi) : I)
Tactic: ext ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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)) ⋯
have refine : ∀ (i : { i : I // J i }), Continuous (Y := Bool) fun (a : (↑(π C J) : Type u)) ↦ (↑a : I → Bool) (↑i : I)
Tactic: refine Continuous.subtype_mk (continuous_pi fun i ↦ ?_) _
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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))
have refine_1 : ∀ (a b : (↑(π C J) : Type u))
  (h :
    Eq (α := (↑(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)) a :
        (↑(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)) b :
        (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J) : Type u))),
  a = b
Tactic: refine ⟨fun a b h ↦ ?_, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
refine_1 :
  ∀ (a b : (↑(π C J) : Type u))
    (h :
      Eq (α := (↑(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)) a :
          (↑(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)) b :
          (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J) : Type u))),
    a = b
⊢ 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))
have refine_2 : ∀ (a : (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J) : Type u)),
  ∃ (a_1 : (↑(π C J) : Type u)), (iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u)) a_1 = a
Tactic: refine ⟨fun a b h ↦ ?_, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
a b : (↑(π C J) : Type u)
h :
  Eq (α := (↑(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)) a :
      (↑(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)) b :
      (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J) : Type u))
⊢ a = b
have refine_1 : ∀ (i : I), (↑a : I → Bool) i = (↑b : I → Bool) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
a b : (↑(π C J) : Type u)
h :
  Eq (α := (↑(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)) a :
      (↑(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)) b :
      (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J) : Type u))
i : I
⊢ (↑a : I → Bool) i = (↑b : I → Bool) i
have refine_1 : ∀
  (h :
    Eq.{u + 1} (α := (i : { i : I // J i }) → Bool)
      (↑((iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u)) a) :
        (i : { i : I // J i }) → Bool)
      (↑((iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u)) b) :
        (i : { i : I // J i }) → Bool))
  (i : I), (↑a : I → Bool) i = (↑b : I → Bool) i
Tactic: rw [Subtype.ext_iff] at h
Cleared hypotheses: h, i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
a b : (↑(π C J) : Type u)
h :
  Eq.{u + 1} (α := (i : { i : I // J i }) → Bool)
    (↑((iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u)) a) :
      (i : { i : I // J i }) → Bool)
    (↑((iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u)) b) :
      (i : { i : I // J i }) → Bool)
i : I
⊢ (↑a : I → Bool) i = (↑b : I → Bool) i
have pos : ∀ (hi : J i), (↑a : I → Bool) i = (↑b : I → Bool) i
Tactic: by_cases hi : J i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
a b : (↑(π C J) : Type u)
h :
  Eq.{u + 1} (α := (i : { i : I // J i }) → Bool)
    (↑((iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u)) a) :
      (i : { i : I // J i }) → Bool)
    (↑((iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u)) b) :
      (i : { i : I // J i }) → Bool)
i : I
pos : ∀ (hi : J i), (↑a : I → Bool) i = (↑b : I → Bool) i
⊢ (↑a : I → Bool) i = (↑b : I → Bool) i
have neg : ∀ (hi : ¬J i), (↑a : I → Bool) i = (↑b : I → Bool) i
Tactic: by_cases hi : J i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
a b : (↑(π C J) : Type u)
h :
  Eq.{u + 1} (α := (i : { i : I // J i }) → Bool)
    (↑((iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u)) a) :
      (i : { i : I // J i }) → Bool)
    (↑((iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u)) b) :
      (i : { i : I // J i }) → Bool)
i : I
hi : ¬J i
⊢ (↑a : I → Bool) i = (↑b : I → Bool) i
have neg : ∀ (c : I → Bool) (hc : c ∈ C)
  (h :
    Eq.{u + 1} (α := (i : { i : I // J i }) → Bool)
      (↑((iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u))
            (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J c) sorry)) :
        (i : { i : I // J i }) → Bool)
      (↑((iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u)) b) :
        (i : { i : I // J i }) → Bool)),
  (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J c) sorry) : I → Bool) i = (↑b : I → Bool) i
Tactic: rcases a with ⟨_, c, hc, rfl⟩
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
b : (↑(π C J) : Type u)
i : I
hi : ¬J i
c : I → Bool
hc : c ∈ C
h :
  Eq.{u + 1} (α := (i : { i : I // J i }) → Bool)
    (↑((iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u))
          (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J c) ⋯)) :
      (i : { i : I // J i }) → Bool)
    (↑((iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u)) b) :
      (i : { i : I // J i }) → Bool)
⊢ (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J c) ⋯) : I → Bool) i = (↑b : I → Bool) i
have neg : ∀ (d : I → Bool) (hd : d ∈ C)
  (h :
    Eq.{u + 1} (α := (i : { i : I // J i }) → Bool)
      (↑((iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u))
            (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J c) sorry)) :
        (i : { i : I // J i }) → Bool)
      (↑((iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u))
            (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J d) sorry)) :
        (i : { i : I // J i }) → Bool)),
  (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J c) sorry) : I → Bool) i =
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J d) sorry) : I → Bool) i
Tactic: rcases b with ⟨_, d, hd, rfl⟩
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
a : (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J) : Type u)
⊢ ∃ (a_1 : (↑(π C J) : Type u)), (iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u)) a_1 = a
have refine_2 : (fun (i : I) ↦
    if hi : J i then (↑a : (i : { i : I // J i }) → Bool) (Subtype.mk (p := fun (i : I) ↦ J i) i hi) else false) ∈
  π C J
Tactic: refine ⟨⟨fun i ↦ if hi : J i then a.val ⟨i, hi⟩ else false, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
a : (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J) : Type u)
refine_2 :
  (fun (i : I) ↦
      if hi : J i then (↑a : (i : { i : I // J i }) → Bool) (Subtype.mk (p := fun (i : I) ↦ J i) i hi) else false) ∈
    π C J
⊢ ∃ (a_1 : (↑(π C J) : Type u)), (iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u)) a_1 = a
have refine_2₁ : (iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u))
    (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J)
      (fun (i : I) ↦
        if hi : J i then (↑a : (i : { i : I // J i }) → Bool) (Subtype.mk (p := fun (i : I) ↦ J i) i hi) else false)
      sorry) =
  a
Tactic: refine ⟨⟨fun i ↦ if hi : J i then a.val ⟨i, hi⟩ else false, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
a : (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J) : Type u)
⊢ (fun (i : I) ↦
      if hi : J i then (↑a : (i : { i : I // J i }) → Bool) (Subtype.mk (p := fun (i : I) ↦ J i) i hi) else false) ∈
    π C J
have refine_2 : ∀ (y : (i : I) → (fun (i : I) ↦ Bool) i) (hy : y ∈ C),
  (fun (i : I) ↦
      if hi : J i then
        (↑(Subtype.mk (p := fun (x : (i : { i : I // J i }) → Bool) ↦
                x ∈ IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J)
                ((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)
                sorry) :
            (i : { i : I // J i }) → Bool)
          (Subtype.mk (p := fun (i : I) ↦ J i) i hi)
      else false) ∈
    π C J
Tactic: rcases a with ⟨_, y, hy, rfl⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst : (i : I) → Decidable (J i)
a : (↑(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))
      (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J)
        (fun (i : I) ↦
          if hi : J i then (↑a : (i : { i : I // J i }) → Bool) (Subtype.mk (p := fun (i : I) ↦ J i) i hi) else false)
        ⋯) =
    a
have refine_2 : ∀ (i : { i : I // J i }),
  (↑((iso_map C J : (a : (↑(π C J) : Type u)) → (↑(IndexFunctor.obj C J) : Type u))
            (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J)
              (fun (i : I) ↦
                if hi : J i then (↑a : (i : { i : I // J i }) → Bool) (Subtype.mk (p := fun (i : I) ↦ J i) i hi)
                else false)
              sorry)) :
        (i : { i : I // J i }) → Bool)
      i =
    (↑a : (i : { i : I // J i }) → Bool) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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)
inst_3 : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
s : (Finset I)ᵒᵖ
⊢ CompactSpace.{u} (↑(π C fun (x : I) ↦ x ∈ unop s) : Type u)
have rw : IsCompact (π C fun (x : I) ↦ x ∈ unop s)
Tactic: rw [← isCompact_iff_compactSpace]