awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : TopologicalSpace T
inst_2 : TopologicalSpace X
inst_3 : DiscreteTopology X
inst_4 : T2Space T
inst_5 : CompactSpace S
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
⊢ IsOpen (fibres π σ)ᶜ
have rw : IsOpen.{u_2} (X := T) (⋃ (i : X), (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {(↑i : OnePoint X)})
Tactic: rw [fibres_compl_eq_iUnion π σ hσ']
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : TopologicalSpace T
inst_2 : TopologicalSpace X
inst_3 : DiscreteTopology X
inst_4 : T2Space T
inst_5 : CompactSpace S
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
⊢ IsOpen.{u_2} (X := T) (⋃ (i : X), (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {(↑i : OnePoint X)})
have refine_1 : ∀ (i : X), IsOpen (Set.range (σ (Option.some i)))ᶜ
Tactic: refine isOpen_iUnion fun i ↦ IsOpen.inter ?_ ?_
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
inst : TopologicalSpace S
inst_1 : TopologicalSpace T
inst_2 : TopologicalSpace X
inst_3 : DiscreteTopology X
inst_4 : T2Space T
inst_5 : CompactSpace S
π : T → Prod.{u_1, u_3} S (OnePoint X)
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
refine_1 : ∀ (i : X), IsOpen (Set.range (σ (Option.some i)))ᶜ
⊢ IsOpen.{u_2} (X := T) (⋃ (i : X), (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {(↑i : OnePoint X)})
have refine_2 : ∀ (i : X), IsOpen (Prod.snd ∘ π ⁻¹' {(↑i : OnePoint X)})
Tactic: refine isOpen_iUnion fun i ↦ IsOpen.inter ?_ ?_
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
Goal:
S : Type u_1
T : Type u_2
X : Type u_3
π : T → Prod.{u_1, u_3} S (Option X)
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
⊢ ∃ (a : (↑(fibres π σ) : Type u_2)),
    Eq (α := Prod.{u_1, u_3} S (Option X)) ((fun (x : (↑(fibres π σ) : Type u_2)) ↦ π (↑x : T)) a) (s, none)
have none : ∀ (y : T) (hy : π y = (s, none)),
  ∃ (a : (↑(fibres π σ) : Type u_2)),
    Eq (α := Prod.{u_1, u_3} S (Option X)) ((fun (x : (↑(fibres π σ) : Type u_2)) ↦ π (↑x : T)) a) (s, none)
Tactic: obtain ⟨y, hy⟩ := hπ (s, none)
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
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
⊢ ∃ (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
have pos : ∀ (h : (π t).2 = none),
  ∃ (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: by_cases h : (π t).2 = none
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
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
pos :
  ∀ (h : (π t).2 = none),
    ∃ (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
have neg : ∀ (h : ¬(π t).2 = none),
  ∃ (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: by_cases h : (π t).2 = none
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨n, hn⟩ := Option.ne_none_iff_exists'.mp h
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (hypothesis)
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)) ⋯
⊢ ∃ (a : (↑(S' π) : Type (max u_2 u_3))), y π a = s
have hp : ∀ (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
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
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 π
⊢ CompactSpace (↑(S' π) : Type (max u_2 u_3))
have 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})
Tactic: rw [← isCompact_iff_compactSpace, show S' π =
    ⋂ (n : OnePoint X) (m : OnePoint X), {x | (π (x n).val).1 = (π (x m).val).1} by aesop]
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (hypothesis)
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 π
⊢ 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})
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
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})
have refine_1 : ∀ (n m : OnePoint X),
  Continuous (Y := S) fun (x : (x : OnePoint X) → (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2)) ↦ (π (↑(x n) : T)).1
Tactic: refine (isClosed_iInter fun n ↦ isClosed_iInter fun m ↦ isClosed_eq ?_ ?_).isCompact
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
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
⊢ 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})
have refine_2 : ∀ (n m : OnePoint X),
  Continuous (Y := S) fun (x : (x : OnePoint X) → (↑(Prod.snd ∘ π ⁻¹' {x}) : Type u_2)) ↦ (π (↑(x m) : T)).1
Tactic: refine (isClosed_iInter fun n ↦ isClosed_iInter fun m ↦ isClosed_eq ?_ ?_).isCompact
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (hypothesis)
Goal:
S T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
inst : Epi π
⊢ ∃ (S' : LightProfinite.{0}) (T' : LightProfinite.{0}) (y' : S' ⟶ S) (π' :
    T' ⟶
      tensorObj (𝒞 :=
        CompHausLike.category fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
        S' ℕ∪{∞})
    (g' : T' ⟶ T),
    Epi π' ∧
      Epi y' ∧
        π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π ∧
          IsSplitEpi (X := LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
              (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞}) ∧
            Epi (cover π')
have this : 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)
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
Goal:
R : Type
inst : CommRing R
⊢ InternallyProjective (C := LightCondMod R) (obj (free R) ℕ∪{∞}.toCondensed)
have rw : ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite.{0})
  (g :
    obj (free R)
        (tensorObj (𝒞 :=
            CompHausLike.category fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
            S ℕ∪{∞}).toCondensed ⟶
      B),
  ∃ (S' : LightProfinite.{0}) (π : S' ⟶ S) (_ :
    Function.Surjective (α :=
      (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))
        S')
      (β :=
      (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))
        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))
              S') →
          (fun
                (X :
                  CompHausLike fun (X : TopCat) ↦
                    TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type)) ↦
              (↑X.toTop : Type))
            S))
    (g' :
    obj (free R)
        (tensorObj (𝒞 :=
            CompHausLike.category fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
            S' ℕ∪{∞}).toCondensed ⟶
      A),
    CategoryTheory.Functor.map (free R) (lightProfiniteToLightCondSet.map (π ▷ ℕ∪{∞})) ≫ g = g' ≫ e
Tactic: rw [free_lightProfinite_internallyProjective_iff_tensor_condition' R ℕ∪{∞}]
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
Goal:
R : Type
inst : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f :
  obj (free R)
      (tensorObj (𝒞 :=
          CompHausLike.category fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
          S ℕ∪{∞}).toCondensed ⟶
    Y
T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
g : obj (free R) T.toCondensed ⟶ X
hπ : Epi π
comm : CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' :
  T' ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S' ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split :
  SplitEpi (X := LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
    (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
⊢ ∃ (g' :
    obj (free R)
        (tensorObj (𝒞 :=
            CompHausLike.category fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
            S' ℕ∪{∞}).toCondensed ⟶
      X),
    CategoryTheory.Functor.map (free R) (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
have pos : ∀
  (hS' :
    Nonempty
      (↑(S'.toTop (P := fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
        Type)),
  ∃ (g' :
    obj (free R)
        (tensorObj (𝒞 :=
            CompHausLike.category fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
            S' ℕ∪{∞}).toCondensed ⟶
      X),
    CategoryTheory.Functor.map (free R) (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
Tactic: by_cases hS' : Nonempty S'
-- Lean 4 proof step from Mathlib.Condensed.Light.Sequence (goal)
Goal:
R : Type
inst : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f :
  obj (free R)
      (tensorObj (𝒞 :=
          CompHausLike.category fun (X : TopCat.{0}) ↦
            TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
          S ℕ∪{∞}).toCondensed ⟶
    Y
T : LightProfinite
π :
  T ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S ℕ∪{∞}
g : obj (free R) T.toCondensed ⟶ X
hπ : Epi π
comm : CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' :
  T' ⟶
    tensorObj (𝒞 :=
      CompHausLike.category fun (X : TopCat.{0}) ↦
        TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
      S' ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split :
  SplitEpi (X := LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
    (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
pos :
  ∀
    (hS' :
      Nonempty
        (↑(S'.toTop (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
          Type)),
    ∃ (g' :
      obj (free R)
          (tensorObj (𝒞 :=
              CompHausLike.category fun (X : TopCat.{0}) ↦
                TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
              S' ℕ∪{∞}).toCondensed ⟶
        X),
      CategoryTheory.Functor.map (free R) (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
⊢ ∃ (g' :
    obj (free R)
        (tensorObj (𝒞 :=
            CompHausLike.category fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
            S' ℕ∪{∞}).toCondensed ⟶
      X),
    CategoryTheory.Functor.map (free R) (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
have neg : ∀
  (hS' :
    ¬Nonempty
        (↑(S'.toTop (P := fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
          Type)),
  ∃ (g' :
    obj (free R)
        (tensorObj (𝒞 :=
            CompHausLike.category fun (X : TopCat.{0}) ↦
              TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))
            S' ℕ∪{∞}).toCondensed ⟶
      X),
    CategoryTheory.Functor.map (free R) (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
Tactic: by_cases hS' : Nonempty S'