awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property :
  π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').1 =
    π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').2
h : ¬(π t).2 = none
neg :
  ∀ (n : X) (hn : (π t).2 = Option.some n),
    ∃ (a :
      (↑(fibres π σ) : Type u_2) ⊕
        { xy : (↑(Prod.snd ∘ π_r π σ ⁻¹' {none}) : Type u_2) × (↑(Prod.snd ∘ π_r π σ ⁻¹' {none}) : Type u_2) //
          π_r π σ (fibreIncl π σ xy.1) = π_r π σ (fibreIncl π σ xy.2) }),
      coverToFun (fibreIncl π σ) (π_r π σ) a =
        Subtype.mk (p := fun (xy : (↑(fibres π σ) : Type u_2) × (↑(fibres π σ) : Type u_2)) ↦
          π_r π σ xy.1 = π_r π σ xy.2)
          (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht')
          property
⊢ ∃ (a :
    (↑(fibres π σ) : Type u_2) ⊕
      { xy : (↑(Prod.snd ∘ π_r π σ ⁻¹' {none}) : Type u_2) × (↑(Prod.snd ∘ π_r π σ ⁻¹' {none}) : Type u_2) //
        π_r π σ (fibreIncl π σ xy.1) = π_r π σ (fibreIncl π σ xy.2) }),
    coverToFun (fibreIncl π σ) (π_r π σ) a =
      Subtype.mk (p := fun (xy : (↑(fibres π σ) : Type u_2) × (↑(fibres π σ) : Type u_2)) ↦ π_r π σ xy.1 = π_r π σ xy.2)
        (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht')
        property

Tactic:
obtain ⟨n, hn⟩ := Option.ne_none_iff_exists'.mp h

Premises used: Option.ne_none_iff_exists', Iff.mp
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property :
  π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').1 =
    π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').2
h : ¬(π t).2 = none
n : X
hn : (π t).2 = Option.some n
⊢ σ (Option.some n) (π t).1 ∈ fibres π σ

Tactic:
grind
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property :
  π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').1 =
    π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').2
h : ¬(π t).2 = none
n : X
hn : (π t).2 = Option.some n
⊢ coverToFun (fibreIncl π σ) (π_r π σ)
      (Sum.inl (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) (σ (Option.some n) (π t).1) ⋯)) =
    Subtype.mk (p := fun (xy : (↑(fibres π σ) : Type u_2) × (↑(fibres π σ) : Type u_2)) ↦ π_r π σ xy.1 = π_r π σ xy.2)
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht')
      property

Tactic:
grind
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property :
  π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').1 =
    π_r π σ
      (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht').2
h : ¬(π t).2 = none
n : X
hn : (π t).2 = Option.some n
⊢ ∃ (a :
    (↑(fibres π σ) : Type u_2) ⊕
      { xy : (↑(Prod.snd ∘ π_r π σ ⁻¹' {none}) : Type u_2) × (↑(Prod.snd ∘ π_r π σ ⁻¹' {none}) : Type u_2) //
        π_r π σ (fibreIncl π σ xy.1) = π_r π σ (fibreIncl π σ xy.2) }),
    coverToFun (fibreIncl π σ) (π_r π σ) a =
      Subtype.mk (p := fun (xy : (↑(fibres π σ) : Type u_2) × (↑(fibres π σ) : Type u_2)) ↦ π_r π σ xy.1 = π_r π σ xy.2)
        (Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t ht, Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) t' ht')
        property

Tactic:
exact ⟨Sum.inl ⟨σ n (π t).1, by grind⟩, by grind⟩
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
R : Type
inst : CommRing R
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
⊢ σ none s ∈ fibres π σ

Tactic:
grind
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
R : Type
inst : CommRing R
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
⊢ Subtype.mk (p := fun (x : T) ↦ x ∈ fibres π σ) (σ none s) ⋯ ∈ Prod.snd ∘ π_r π σ ⁻¹' {none}

Tactic:
grind
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (OnePoint X)
y : (x : OnePoint X) → (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2)
⊢ y ∈ S' π ↔ ∀ (n m : OnePoint X), (π (↑(y n) : T)).1 = (π (↑(y m) : T)).1

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, _private.0.InternalProjectivityProof.S'
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (OnePoint X)
x : (↑(S' π) : Type (max u_2 u_3))
⊢ y π x = (π (↑((↑x : (x : OnePoint X) → (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2)) ∞) : T)).1

Tactic:
rfl

Premises used: _private.0.InternalProjectivityProof.y, rfl
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : TopologicalSpace T
inst_2 : TopologicalSpace X
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
⊢ Continuous (X := (↑(S' π) : Type (max u_2 u_3)))
    (Subtype.val (p := fun (x : (x : OnePoint X) → (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2)) ↦ x ∈ S' π))

Tactic:
fun_prop
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Function.Surjective π
s : S
p : (s : S) → (n : OnePoint X) → T := fun (s : S) (n : OnePoint X) ↦ Exists.choose (p := fun (a : T) ↦ π a = (s, n)) ⋯
⊢ ∀ (s : S) (n : OnePoint X), π (p s n) = (s, n)

Tactic:
have hp (s : S) (n : OnePoint X) : π (p s n) = (s, n) := (hπ (s, n)).choose_spec
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Function.Surjective π
s : S
p : (s : S) → (n : OnePoint X) → T := fun (s : S) (n : OnePoint X) ↦ Exists.choose (p := fun (a : T) ↦ π a = (s, n)) ⋯
hp : ∀ (s : S) (n : OnePoint X), π (p s n) = (s, n)
n : OnePoint X
⊢ p s n ∈ Prod.snd ∘ π ⁻¹' {n}

Tactic:
grind
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Function.Surjective π
s : S
p : (s : S) → (n : OnePoint X) → T := fun (s : S) (n : OnePoint X) ↦ Exists.choose (p := fun (a : T) ↦ π a = (s, n)) ⋯
hp : ∀ (s : S) (n : OnePoint X), π (p s n) = (s, n)
⊢ (fun (n : OnePoint X) ↦ Subtype.mk (p := fun (x : T) ↦ x ∈ Prod.snd ∘ π ⁻¹' {n}) (p s n) ⋯) ∈ S' π

Tactic:
grind
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Function.Surjective π
s : S
p : (s : S) → (n : OnePoint X) → T := fun (s : S) (n : OnePoint X) ↦ Exists.choose (p := fun (a : T) ↦ π a = (s, n)) ⋯
hp : ∀ (s : S) (n : OnePoint X), π (p s n) = (s, n)
⊢ y π
      (Subtype.mk (p := fun (x : (x : OnePoint X) → (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2)) ↦ x ∈ S' π)
        (fun (n : OnePoint X) ↦ Subtype.mk (p := fun (x : T) ↦ x ∈ Prod.snd ∘ π ⁻¹' {n}) (p s n) ⋯) ⋯) =
    s

Tactic:
grind
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Function.Surjective π
s : S
p : (s : S) → (n : OnePoint X) → T := fun (s : S) (n : OnePoint X) ↦ Exists.choose (p := fun (a : T) ↦ π a = (s, n)) ⋯
hp : ∀ (s : S) (n : OnePoint X), π (p s n) = (s, n)
⊢ ∃ (a : (↑(S' π) : Type (max u_2 u_3))), y π a = s

Tactic:
exact ⟨⟨fun n ↦ ⟨p s n, by grind⟩, by grind⟩, by grind⟩
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : T2Space S
inst_2 : TopologicalSpace T
inst_3 : CompactSpace T
inst_4 : TopologicalSpace X
inst_5 : T1Space.{u_3} (OnePoint X)
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
⊢ S' π =
    ⋂ (n : OnePoint X),
      ⋂ (m : OnePoint X),
        {x : (x : OnePoint X) → (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2) | (π (↑(x n) : T)).1 = (π (↑(x m) : T)).1}

Tactic:
aesop
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : T2Space S
inst_2 : TopologicalSpace T
inst_3 : CompactSpace T
inst_4 : TopologicalSpace X
inst_5 : T1Space.{u_3} (OnePoint X)
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
rw :
  IsCompact (X := (x : OnePoint X) → (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2))
    (⋂ (n : OnePoint X),
      ⋂ (m : OnePoint X),
        {x : (x : OnePoint X) → (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2) | (π (↑(x n) : T)).1 = (π (↑(x m) : T)).1})
⊢ CompactSpace (↑(S' π) : Type (max u_2 u_3))

Tactic:
rw [← isCompact_iff_compactSpace, show S' π =
    ⋂ (n : OnePoint X) (m : OnePoint X), {x | (π (x n).val).1 = (π (x m).val).1} by aesop]

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : T2Space S
inst_2 : TopologicalSpace T
inst_3 : CompactSpace T
inst_4 : TopologicalSpace X
inst_5 : T1Space.{u_3} (OnePoint X)
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
x : OnePoint X
⊢ Continuous (Prod.snd ∘ π)

Tactic:
fun_prop
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : T2Space S
inst_2 : TopologicalSpace T
inst_3 : CompactSpace T
inst_4 : TopologicalSpace X
inst_5 : T1Space.{u_3} (OnePoint X)
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
⊢ ∀ (x : OnePoint X), CompactSpace.{u_2} (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2)

Tactic:
have (x : OnePoint X) : CompactSpace <| (Prod.snd ∘ π) ⁻¹' {x} :=
    isCompact_iff_compactSpace.mp (IsClosed.preimage (by fun_prop) isClosed_singleton).isCompact
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : T2Space S
inst_2 : TopologicalSpace T
inst_3 : CompactSpace T
inst_4 : TopologicalSpace X
inst_5 : T1Space.{u_3} (OnePoint X)
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
this : ∀ (x : OnePoint X), CompactSpace.{u_2} (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2)
⊢ IsCompact (X := (x : OnePoint X) → (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2))
    (⋂ (n : OnePoint X),
      ⋂ (m : OnePoint X),
        {x : (x : OnePoint X) → (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2) | (π (↑(x n) : T)).1 = (π (↑(x m) : T)).1})

Tactic:
(isClosed_iInter fun n ↦ isClosed_iInter fun m ↦ isClosed_eq ?_ ?_).isCompact

Premises used: isClosed_eq, IsClosed.isCompact, isClosed_iInter
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : T2Space S
inst_2 : TopologicalSpace T
inst_3 : CompactSpace T
inst_4 : TopologicalSpace X
inst_5 : T1Space.{u_3} (OnePoint X)
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
this : ∀ (x : OnePoint X), CompactSpace.{u_2} (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2)
refine_1 :
  ∀ (n m : OnePoint X),
    Continuous (Y := S) fun (x : (x : OnePoint X) → (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2)) ↦ (π (↑(x n) : T)).1
refine_2 :
  ∀ (n m : OnePoint X),
    Continuous (Y := S) fun (x : (x : OnePoint X) → (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2)) ↦ (π (↑(x m) : T)).1
⊢ IsCompact (X := (x : OnePoint X) → (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2))
    (⋂ (n : OnePoint X),
      ⋂ (m : OnePoint X),
        {x : (x : OnePoint X) → (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2) | (π (↑(x n) : T)).1 = (π (↑(x m) : T)).1})

Tactic:
refine (isClosed_iInter fun n ↦ isClosed_iInter fun m ↦ isClosed_eq ?_ ?_).isCompact

Premises used: isClosed_eq, IsClosed.isCompact, isClosed_iInter
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : T2Space S
inst_2 : TopologicalSpace T
inst_3 : CompactSpace T
inst_4 : TopologicalSpace X
inst_5 : T1Space.{u_3} (OnePoint X)
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
this : ∀ (x : OnePoint X), CompactSpace.{u_2} (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2)
n m : OnePoint X
⊢ Continuous (Y := S) fun (x : (x : OnePoint X) → (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2)) ↦ (π (↑(x n) : T)).1

Tactic:
fun_prop
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : T2Space S
inst_2 : TopologicalSpace T
inst_3 : CompactSpace T
inst_4 : TopologicalSpace X
inst_5 : T1Space.{u_3} (OnePoint X)
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
this : ∀ (x : OnePoint X), CompactSpace.{u_2} (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2)
n m : OnePoint X
⊢ Continuous (Y := S) fun (x : (x : OnePoint X) → (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2)) ↦ (π (↑(x m) : T)).1

Tactic:
fun_prop
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
R : Type
inst : CommRing R
X : LightCondMod R
S T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
inst_1 :
  Epi (C := LightCondMod R) (X :=
    obj (lightProfiniteToLightCondSet ⋙ free R)
      (CompHausLike.of
        (fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
        ((↑(T.toTop (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
            Type) ⊕
          (↑((CompHausLike.pullback (P := fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) (X :=
                    LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})) (Y := LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞}))
                    (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                    (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)).toTop
                (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
            Type))))
    (CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) (cover π))
g : obj (lightProfiniteToLightCondSet ⋙ free R) T ⟶ X
r_inf : T ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
σ : S ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞}))
⊢ 𝟙 T ≫ π = 𝟙 T ≫ π

Tactic:
simp
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
R : Type
inst : CommRing R
X : LightCondMod R
S T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
inst_1 :
  Epi (C := LightCondMod R) (X :=
    obj (lightProfiniteToLightCondSet ⋙ free R)
      (CompHausLike.of
        (fun (X : TopCat.{0}) ↦ TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
        ((↑(T.toTop (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
            Type) ⊕
          (↑((CompHausLike.pullback (P := fun (X : TopCat.{0}) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) (X :=
                    LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})) (Y := LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞}))
                    (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
                    (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)).toTop
                (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
            Type))))
    (CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) (cover π))
g : obj (lightProfiniteToLightCondSet ⋙ free R) T ⟶ X
r_inf : T ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
σ : S ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞}))
⊢ Eq (α :=
    CompHausLike.pullback (P := fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) (X :=
        LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})) (Y := LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞}))
        (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ⟶
      tensorObj (𝒞 :=
        CompHausLike.category fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
        S ℕ∪{∞})
    ((CompHausLike.pullback.fst (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
          (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
        LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
      π)
    ((CompHausLike.pullback.snd (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
          (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π) ≫
        LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
      π)

Tactic:
simp [pullback.condition]

Premises used: CompHausLike.pullback.condition
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
inst : Epi π
⊢ Continuous (X :=
    (fun
          (X :
            CompHausLike fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
          Type))
      T)
    (Y :=
    (↑(S.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type) ×
      OnePoint ℕ)
    (⇑(ConcreteCategory.hom (FC :=
          fun
            (x1 x2 :
              CompHausLike fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
              Type),
            (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
              Type)))
          (CC :=
          fun
            (X :
              CompHausLike fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
            Type))
          π) :
      (a :
          (fun
                (X :
                  CompHausLike fun (X : TopCat) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
              (↑X.toTop : Type))
            T) →
        (fun
              (X :
                CompHausLike fun (X : TopCat) ↦
                  TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
            (↑X.toTop : Type))
          (S ⊗ ℕ∪{∞}))

Tactic:
fun_prop
-- Module: Mathlib.Condensed.Light.Sequence
Goal:
S T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
inst : Epi π
⊢ CompactSpace
    (↑(S'
          (⇑(ConcreteCategory.hom (FC :=
                fun
                  (x1 x2 :
                    CompHausLike fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type),
                  (↑(x2.toTop (P := fun (X : TopCat.{0}) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                    Type)))
                (CC :=
                fun
                  (X :
                    CompHausLike fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{0}) ↦
                      TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
                  Type))
                π) :
            (a :
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                    (↑X.toTop : Type))
                  T) →
              (fun
                    (X :
                      CompHausLike fun (X : TopCat) ↦
                        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
                  (↑X.toTop : Type))
                (S ⊗ ℕ∪{∞}))) :
      Type)

Tactic:
have := S'_compactSpace π (by fun_prop)