awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
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
⊢ 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:
refine ⟨fun a b h ↦ ?_, fun a ↦ ?_⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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))
refine_1 : ∀ (i : I), (↑a : I → Bool) i = (↑b : I → Bool) i
⊢ a = b

Tactic:
ext i
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
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
⊢ (↑a : I → Bool) i = (↑b : I → Bool) i

Tactic:
rw [Subtype.ext_iff] at h

Premises used: Subtype.ext_iff
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
neg : ∀ (hi : ¬J i), (↑a : I → Bool) i = (↑b : I → Bool) i
⊢ (↑a : I → Bool) i = (↑b : I → Bool) i

Tactic:
by_cases hi : J i
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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

Tactic:
congr_fun h ⟨i, hi⟩

Premises used: Subtype.mk, congr_fun
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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

Tactic:
exact congr_fun h ⟨i, hi⟩

Premises used: Subtype.mk, congr_fun
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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
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) ⋯)) :
          (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
⊢ (↑a : I → Bool) i = (↑b : I → Bool) i

Tactic:
rcases a with ⟨_, c, hc, rfl⟩

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)
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)
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) ⋯)) :
          (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) ⋯)) :
          (i : { i : I // J i }) → Bool)),
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J c) ⋯) : I → Bool) i =
      (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J d) ⋯) : I → Bool) i
⊢ (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J c) ⋯) : I → Bool) i = (↑b : I → Bool) i

Tactic:
rcases b with ⟨_, d, hd, rfl⟩

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)
i : I
hi : ¬J i
c : I → Bool
hc : c ∈ C
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) ⋯)) :
      (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) ⋯)) :
      (i : { i : I // J i }) → Bool)
⊢ (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J c) ⋯) : I → Bool) i =
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C J) (Proj J d) ⋯) : I → Bool) i

Tactic:
simp only [Proj, if_neg hi]

Premises used: Profinite.NobelingProof.Proj, if_neg
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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

Tactic:
⟨⟨fun i ↦ if hi : J i then a.val ⟨i, hi⟩ else false, ?_⟩, ?_⟩

Premises used: dite, Subtype.mk, Exists.intro, Bool.false, 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)
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
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)
        ⋯) =
    a
⊢ ∃ (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 i ↦ if hi : J i then a.val ⟨i, hi⟩ else false, ?_⟩, ?_⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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 :
  ∀ (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)
                  ⋯) :
              (i : { i : I // J i }) → Bool)
            (Subtype.mk (p := fun (i : I) ↦ J i) i hi)
        else false) ∈
      π 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) ∈
    π C J

Tactic:
rcases a with ⟨_, y, hy, rfl⟩

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 : 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)
                ⋯) :
            (i : { i : I // J i }) → Bool)
          (Subtype.mk (p := fun (i : I) ↦ J i) i hi)
      else false) ∈
    π C J

Tactic:
⟨y, hy, rfl⟩

Premises used: Set.Mem, setOf, Profinite.NobelingProof.π, And.intro, Exists.intro, Set.image, 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 : 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)
                ⋯) :
            (i : { i : I // J i }) → Bool)
          (Subtype.mk (p := fun (i : I) ↦ J i) i hi)
      else false) ∈
    π C J

Tactic:
exact ⟨y, hy, 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)
a : (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J) : Type u)
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)
                ⋯)) :
          (i : { i : I // J i }) → Bool)
        i =
      (↑a : (i : { i : I // J i }) → Bool) 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)
        ⋯) =
    a

Tactic:
ext i
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
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)
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)
              ⋯)) :
        (i : { i : I // J i }) → Bool)
      i =
    (↑a : (i : { i : I // J i }) → Bool) i

Tactic:
dif_pos i.prop

Premises used: dif_pos, dite, Subtype.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)
a : (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C J) : Type u)
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)
              ⋯)) :
        (i : { i : I // J i }) → Bool)
      i =
    (↑a : (i : { i : I // J i }) → Bool) i

Tactic:
exact dif_pos i.prop

Premises used: dif_pos, Subtype.prop
-- 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)
inst_3 : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
s : (Finset I)ᵒᵖ
rw : IsCompact (π C fun (x : I) ↦ x ∈ unop s)
⊢ CompactSpace.{u} (↑(π C fun (x : I) ↦ x ∈ unop s) : Type u)

Tactic:
rw [← isCompact_iff_compactSpace]

Premises used: isCompact_iff_compactSpace
-- 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)
inst_3 : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
s : (Finset I)ᵒᵖ
⊢ IsCompact (π C fun (x : I) ↦ x ∈ unop s)

Tactic:
hC.image (continuous_proj _)

Premises used: Profinite.NobelingProof.π, Profinite.NobelingProof.continuous_proj, IsCompact.image
-- 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)
inst_3 : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
s : (Finset I)ᵒᵖ
⊢ IsCompact (π C fun (x : I) ↦ x ∈ unop s)

Tactic:
exact hC.image (continuous_proj _)

Premises used: Profinite.NobelingProof.continuous_proj, IsCompact.image
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J_1 K L : I → Prop
inst : (i : I) → Decidable (J_1 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
J : (Finset I)ᵒᵖ
simp :
  CompHausLike.ofHom (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))
      { toFun := id, continuous_toFun := ⋯ } =
    𝟙 (of (↑(π C fun (x : I) ↦ x ∈ unop J) : Type u))
⊢ CompHausLike.ofHom (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))
      { toFun := ProjRestricts C (J := fun (x : I) ↦ x ∈ unop J) (K := fun (x : I) ↦ x ∈ unop J) ⋯,
        continuous_toFun := ⋯ } =
    𝟙 (of (↑(π C fun (x : I) ↦ x ∈ unop J) : Type u))

Tactic:
simp only [projRestricts_eq_id C (· ∈ (unop J))]

Premises used: Membership.mem, Profinite.NobelingProof.projRestricts_eq_id, Opposite.unop
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J_1 K L : I → Prop
inst : (i : I) → Decidable (J_1 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
J : (Finset I)ᵒᵖ
⊢ CompHausLike.ofHom (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))
      { toFun := id, continuous_toFun := ⋯ } =
    𝟙 (of (↑(π C fun (x : I) ↦ x ∈ unop J) : Type u))

Tactic:
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)
inst_3 : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
X Y Z : (Finset I)ᵒᵖ
x : X ⟶ Y
x_1 : Y ⟶ Z
e_f :
  Eq (α := (↑(π C fun (x : I) ↦ x ∈ unop X) : Type u) → (↑(π C fun (x : I) ↦ x ∈ unop Z) : Type u))
    (ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Z) (K := fun (x : I) ↦ x ∈ unop X) ⋯)
    (Function.comp (β := (↑(π C fun (x : I) ↦ x ∈ unop Y) : Type u))
      (⇑{ toFun := ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Z) (K := fun (x : I) ↦ x ∈ unop Y) ⋯,
            continuous_toFun := ⋯ } :
        (a : (↑(π C fun (x : I) ↦ x ∈ unop Y) : Type u)) → (↑(π C fun (x : I) ↦ x ∈ unop Z) : Type u))
      (⇑{ toFun := ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Y) (K := fun (x : I) ↦ x ∈ unop X) ⋯,
            continuous_toFun := ⋯ } :
        (a : (↑(π C fun (x : I) ↦ x ∈ unop X) : Type u)) → (↑(π C fun (x : I) ↦ x ∈ unop Y) : Type u)))
⊢ Eq (α := of (↑(π C fun (x : I) ↦ x ∈ unop X) : Type u) ⟶ of (↑(π C fun (x : I) ↦ x ∈ unop Z) : Type u))
    (CompHausLike.ofHom (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))
      { toFun := ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Z) (K := fun (x : I) ↦ x ∈ unop X) ⋯,
        continuous_toFun := ⋯ })
    (CompHausLike.ofHom (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))
      (comp (β := (↑(π C fun (x : I) ↦ x ∈ unop Y) : Type u))
        { toFun := ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Z) (K := fun (x : I) ↦ x ∈ unop Y) ⋯,
          continuous_toFun := ⋯ }
        { toFun := ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Y) (K := fun (x : I) ↦ x ∈ unop X) ⋯,
          continuous_toFun := ⋯ }))

Tactic:
congr
-- 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)
inst_3 : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
X Y Z : (Finset I)ᵒᵖ
x : X ⟶ Y
x_1 : Y ⟶ Z
e_f e_f₁ :
  Eq (α := (↑(π C fun (x : I) ↦ x ∈ unop X) : Type u) → (↑(π C fun (x : I) ↦ x ∈ unop Z) : Type u))
    (ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Z) (K := fun (x : I) ↦ x ∈ unop X) ⋯)
    (ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Z) (K := fun (x : I) ↦ x ∈ unop X) ⋯)
⊢ Eq (α := (↑(π C fun (x : I) ↦ x ∈ unop X) : Type u) → (↑(π C fun (x : I) ↦ x ∈ unop Z) : Type u))
    (ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Z) (K := fun (x : I) ↦ x ∈ unop X) ⋯)
    (Function.comp (β := (↑(π C fun (x : I) ↦ x ∈ unop Y) : Type u))
      (ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Z) (K := fun (x : I) ↦ x ∈ unop Y) ⋯)
      (ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Y) (K := fun (x : I) ↦ x ∈ unop X) ⋯))

Tactic:
rw [projRestricts_eq_comp]

Premises used: Profinite.NobelingProof.projRestricts_eq_comp
-- 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)
inst_3 : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC rwa rwa₁ rwa₂ rwa₃ : IsCompact C
⊢ CompactSpace.{u} (↑C : Type u)

Tactic:
rwa [← isCompact_iff_compactSpace]

Premises used: isCompact_iff_compactSpace
-- 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)
inst_3 : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
X Y : (Finset I)ᵒᵖ
h : X ⟶ Y
⊢ Eq (α := of (↑C : Type u) ⟶ (spanFunctor (C := C) hC).obj Y)
    (ConcreteCategory.ofHom (FC :=
      fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
        (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
      (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      {
        toFun :=
          Function.comp (β := (↑(π C (Membership.mem (unop X))) : Type u))
            (ProjRestricts C (J := Membership.mem (unop Y)) (K := Membership.mem (unop X)) ⋯)
            (ProjRestrict C (Membership.mem (unop X))),
        continuous_toFun := ⋯ })
    (ConcreteCategory.ofHom (FC :=
        fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
          (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
        (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        { toFun := ProjRestrict C fun (x : I) ↦ x ∈ unop X, continuous_toFun := ⋯ } ≫
      (spanFunctor (C := C) hC).map h)

Tactic:
rfl