awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Condensed.Explicit (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
FA : A → A → Type u_2
CA : A → Type u_3
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_3 : ReflectsFiniteLimits.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} CompHausᵒᵖ A
inst_4 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ IsSheaf (coherentTopology CompHaus) (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
have rw : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA)) ∧
  EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
Tactic: rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition]
-- Lean 4 proof step from Mathlib.Condensed.Light.Basic (goal)
Goal:
C : Type w
inst : Category.{v, w} C
X Y : LightCondensed.{u, v, w} C
f g : X ⟶ Y
h : ∀ (S : LightProfiniteᵒᵖ), f.hom.app S = g.hom.app S
⊢ f = g
have h₁ : f.hom = g.hom
Tactic: apply Sheaf.hom_ext
-- Lean 4 proof step from Mathlib.Condensed.Light.Epi (goal)
Goal:
R : Type u
inst : Ring R
X Y : LightCondMod R
f_1 : X ⟶ Y
X_1 Y_1 : LightCondMod R
f : X_1 ⟶ Y_1
hf : Epi (X := Functor.obj (LightCondensed.forget R) X_1) (CategoryTheory.Functor.map (LightCondensed.forget R) f)
⊢ Epi f
have rw : ∀
  (hf :
    IsLocallySurjective (FA := TypeCat.Fun) (F₁ := Functor.obj (LightCondensed.forget R) X_1)
      (CategoryTheory.Functor.map (LightCondensed.forget R) f)),
  IsLocallySurjective (FA := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CA := ModuleCat.carrier)
    f
Tactic: rw [← Sheaf.isLocallySurjective_iff_epi'] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Condensed.Light.Epi (goal)
Goal:
R : Type u
inst : Ring R
X Y : LightCondMod R
f_1 : X ⟶ Y
X_1 Y_1 : LightCondMod R
f : X_1 ⟶ Y_1
hf : Epi f
⊢ Epi (X := Functor.obj (LightCondensed.forget R) X_1) (CategoryTheory.Functor.map (LightCondensed.forget R) f)
have rw : ∀
  (hf :
    IsLocallySurjective (FA := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CA :=
      ModuleCat.carrier) f),
  IsLocallySurjective (FA := TypeCat.Fun) (F₁ := Functor.obj (LightCondensed.forget R) X_1)
    (CategoryTheory.Functor.map (LightCondensed.forget R) f)
Tactic: rw [← Sheaf.isLocallySurjective_iff_epi'] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Condensed.Light.Epi (hypothesis)
Goal:
R : Type u
inst : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst_1 : Epi f
S : LightProfinite
p : Functor.obj (LightCondensed.free R) S.toCondensed ⟶ Y
⊢ ∃ (T : LightProfinite.{u}) (π : T ⟶ S) (g : Functor.obj (LightCondensed.free R) T.toCondensed ⟶ X),
    Epi π ∧ CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ LightCondensed.free R) π ≫ p = g ≫ f
have this : Epi (X := Functor.obj (LightCondensed.forget R) X) (CategoryTheory.Functor.map (LightCondensed.forget R) f)
Tactic: have : Epi ((LightCondensed.forget _).map f) := inferInstance
-- Lean 4 proof step from Mathlib.Condensed.Light.Epi (goal)
Goal:
R : Type u_1
inst : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ Epi (X := Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0)) (c.π.app (Opposite.op 0))
have apply : Epi (X := Functor.obj (forget R) (Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0)))
  (CategoryTheory.Functor.map (forget R) (c.π.app (Opposite.op 0)))
Tactic: apply Functor.epi_of_epi_map (forget R)
-- Lean 4 proof step from Mathlib.Condensed.Light.Epi (goal)
Goal:
R : Type u_1
inst : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ Epi (X := Functor.obj (forget R) (Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0)))
    (CategoryTheory.Functor.map (forget R) (c.π.app (Opposite.op 0)))
have change : Epi (X :=
  Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) (Cone.pt (F := F ⋙ forget R) (Functor.mapCone (forget R) c)))
    (Opposite.op 0))
  (NatTrans.app (Cone.π (Functor.mapCone (forget R) c)) (Opposite.op 0))
Tactic: change Epi (((forget R).mapCone c).π.app ⟨0⟩)
-- Lean 4 proof step from Mathlib.Condensed.Light.Epi (goal)
Goal:
R : Type u_1
inst : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ Epi (X :=
    Functor.obj (C := ℕᵒᵖ)
      (Functor.obj (Functor.const ℕᵒᵖ) (Cone.pt (F := F ⋙ forget R) (Functor.mapCone (forget R) c))) (Opposite.op 0))
    (NatTrans.app (Cone.π (Functor.mapCone (forget R) c)) (Opposite.op 0))
have h : ∀ (G : ℕᵒᵖ ⥤ LightProfinite),
  (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE sorry).op)) →
    EffectiveEpi (X := G.obj (Opposite.op 0)) (Y := limit G) (limit.π G (Opposite.op 0))
Tactic: apply coherentTopology.epi_π_app_zero_of_epi
-- Lean 4 proof step from Mathlib.Condensed.Light.Epi (goal)
Goal:
R : Type u_1
inst : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
h :
  ∀ (G : ℕᵒᵖ ⥤ LightProfinite),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) →
      EffectiveEpi (X := G.obj (Opposite.op 0)) (Y := limit G) (limit.π G (Opposite.op 0))
⊢ Epi (X :=
    Functor.obj (C := ℕᵒᵖ)
      (Functor.obj (Functor.const ℕᵒᵖ) (Cone.pt (F := F ⋙ forget R) (Functor.mapCone (forget R) c))) (Opposite.op 0))
    (NatTrans.app (Cone.π (Functor.mapCone (forget R) c)) (Opposite.op 0))
have hc₁ : IsLimit (F := F ⋙ forget R) (Functor.mapCone (forget R) c)
Tactic: apply coherentTopology.epi_π_app_zero_of_epi
-- Lean 4 proof step from Mathlib.Condensed.Light.Epi (goal)
Goal:
R : Type u_1
inst : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
h :
  ∀ (G : ℕᵒᵖ ⥤ LightProfinite),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) →
      EffectiveEpi (X := G.obj (Opposite.op 0)) (Y := limit G) (limit.π G (Opposite.op 0))
hc₁ : IsLimit (F := F ⋙ forget R) (Functor.mapCone (forget R) c)
⊢ Epi (X :=
    Functor.obj (C := ℕᵒᵖ)
      (Functor.obj (Functor.const ℕᵒᵖ) (Cone.pt (F := F ⋙ forget R) (Functor.mapCone (forget R) c))) (Opposite.op 0))
    (NatTrans.app (Cone.π (Functor.mapCone (forget R) c)) (Opposite.op 0))
have hF₁ : ∀ (n : ℕ), Epi ((F ⋙ forget R).map (homOfLE sorry).op)
Tactic: apply coherentTopology.epi_π_app_zero_of_epi
-- Lean 4 proof step from Mathlib.Condensed.Light.Epi (hypothesis)
Goal:
R : Type u_1
inst : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ IsLimit (F := F ⋙ forget R) (Functor.mapCone (forget R) c)
have this : Functor.IsRightAdjoint (D := LightCondMod R) (forget R)
Tactic: have := (freeForgetAdjunction R).isRightAdjoint
-- Lean 4 proof step from Mathlib.Condensed.Light.Epi (goal)
Goal:
n_1 : ℕ
R : Type u
inst : Ring R
M N : ℕ → LightCondMod R
f : (n : ℕ) → M n ⟶ N n
inst_1 : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi ((Functor.ofOpSequence (X := functorObj M N) (functorMap f)).map (homOfLE ⋯).op)
have simp : Epi (X := functorObj M N (n + 1)) (functorMap f n)
Tactic: simp only [Nat.succ_eq_add_one, Functor.ofOpSequence_obj, homOfLE_leOfHom,
      Functor.ofOpSequence_map_homOfLE_succ]
-- Lean 4 proof step from Mathlib.Condensed.Light.Epi (goal)
Goal:
n : ℕ
R : Type u
inst : Ring R
M N : ℕ → LightCondMod R
f_1 : (n : ℕ) → M n ⟶ N n
inst_1 : ∀ (n : ℕ), Epi (f_1 n)
X Y : Discrete ℕ ⥤ LightCondMod R
f : X ⟶ Y
h : Epi f
⊢ Eq (α := Functor.obj lim X ⟶ Functor.obj lim Y) (CategoryTheory.Functor.map lim f)
    (CategoryStruct.comp (Y := ∏ᶜ fun (j : ℕ) ↦ X.obj { as := j }) (Iso.inv (Pi.isoLimit X))
      (CategoryStruct.comp (Y := ∏ᶜ fun (x : ℕ) ↦ Y.obj { as := x }) (Limits.Pi.map fun (x : ℕ) ↦ f.app { as := x })
        (Iso.hom (Pi.isoLimit Y))))
have w : ∀ (j : Discrete ℕ),
  Eq (α := Functor.obj lim X ⟶ Y.obj j) (CategoryTheory.Functor.map lim f ≫ limit.π Y j)
    (CategoryStruct.comp (Y := limit Y)
      (CategoryStruct.comp (Y := ∏ᶜ fun (j : ℕ) ↦ X.obj { as := j }) (Iso.inv (Pi.isoLimit X))
        (CategoryStruct.comp (Y := ∏ᶜ fun (x : ℕ) ↦ Y.obj { as := x }) (Limits.Pi.map fun (x : ℕ) ↦ f.app { as := x })
          (Iso.hom (Pi.isoLimit Y))))
      (limit.π Y j))
Tactic: apply limit.hom_ext
-- Lean 4 proof step from Mathlib.Condensed.Light.Epi (goal)
Goal:
n : ℕ
R : Type u
inst : Ring R
M N : ℕ → LightCondMod R
f_1 : (n : ℕ) → M n ⟶ N n
inst_1 : ∀ (n : ℕ), Epi (f_1 n)
X Y : Discrete ℕ ⥤ LightCondMod R
f : X ⟶ Y
h : Epi f
this :
  Eq (α := Functor.obj lim X ⟶ Functor.obj lim Y) (CategoryTheory.Functor.map lim f)
    (CategoryStruct.comp (Y := ∏ᶜ fun (j : ℕ) ↦ X.obj { as := j }) (Iso.inv (Pi.isoLimit X))
      (CategoryStruct.comp (Y := ∏ᶜ fun (x : ℕ) ↦ Y.obj { as := x }) (Limits.Pi.map fun (x : ℕ) ↦ f.app { as := x })
        (Iso.hom (Pi.isoLimit Y))))
⊢ Epi (X := Functor.obj lim X) (CategoryTheory.Functor.map lim f)
have rw : Epi (X := Functor.obj lim X) (Y := Functor.obj lim Y)
  (CategoryStruct.comp (Y := ∏ᶜ fun (j : ℕ) ↦ X.obj { as := j }) (Iso.inv (Pi.isoLimit X))
    (CategoryStruct.comp (Y := ∏ᶜ fun (x : ℕ) ↦ Y.obj { as := x }) (Limits.Pi.map fun (x : ℕ) ↦ f.app { as := x })
      (Iso.hom (Pi.isoLimit Y))))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Condensed.Light.Explicit (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} LightProfiniteᵒᵖ A
inst_1 : PreservesFiniteProducts F
hF : EqualizerCondition F
⊢ IsSheaf (coherentTopology LightProfinite) F
have rw : PreservesFiniteProducts F ∧ EqualizerCondition F
Tactic: rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition F]
-- Lean 4 proof step from Mathlib.Condensed.Light.Explicit (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
FA : A → A → Type u_2
CA : A → Type u_3
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_3 : ReflectsFiniteLimits.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} LightProfiniteᵒᵖ A
inst_4 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ IsSheaf (coherentTopology LightProfinite) F
have apply : IsSheaf (coherentTopology LightProfinite) (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
Tactic: apply isSheaf_coherent_of_hasPullbacks_of_comp F (CategoryTheory.forget A)
-- Lean 4 proof step from Mathlib.Condensed.Light.Explicit (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
FA : A → A → Type u_2
CA : A → Type u_3
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_3 : ReflectsFiniteLimits.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} LightProfiniteᵒᵖ A
inst_4 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ IsSheaf (coherentTopology LightProfinite) (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
have rw : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA)) ∧
  EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
Tactic: rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition]
-- Lean 4 proof step from Mathlib.Condensed.Light.InternallyProjective (goal)
Goal:
R : Type u
inst : CommRing R
A B P : LightCondMod R
S : LightProfinite
e : A ⟶ B
x : (↑((P ⟹ A).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u)
⊢ Eq (α := (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X :=
            (P ⟹ A).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))
            (NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map (ihom P) e)) (Opposite.op S)) :
          (a : (↑((P ⟹ A).obj.obj (Opposite.op S)) : Type u)) → (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u))
        x :
      (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u))
    (((ihomPoints R P B S).symm :
          (a : P ⊗ (free R).obj S.toCondensed ⟶ B) → (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u))
        ((ihomPoints R P A S : (a : (↑((P ⟹ A).obj.obj (Opposite.op S)) : Type u)) → P ⊗ (free R).obj S.toCondensed ⟶ A)
            x ≫
          e) :
      (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u))
have a : Eq (α :=
  tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
      (obj (free R) S.toCondensed) ⟶
    B)
  ((ihomPoints R P B S : (a : (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u)) → P ⊗ (free R).obj S.toCondensed ⟶ B)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X :=
              (P ⟹ A).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S))
              (NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map (ihom P) e)) (Opposite.op S)) :
            (a : (↑((P ⟹ A).obj.obj (Opposite.op S)) : Type u)) → (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u))
          x :
        (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u)) :
    tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
        (obj (free R) S.toCondensed) ⟶
      B)
  ((ihomPoints R P B S : (a : (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u)) → P ⊗ (free R).obj S.toCondensed ⟶ B)
      (((ihomPoints R P B S).symm :
            (a : P ⊗ (free R).obj S.toCondensed ⟶ B) → (↑((P ⟹ B).obj.obj (Opposite.op S)) : Type u))
          ((ihomPoints R P A S :
                (a : (↑((P ⟹ A).obj.obj (Opposite.op S)) : Type u)) → P ⊗ (free R).obj S.toCondensed ⟶ A)
              x ≫
            e) :
        (↑((P ⟹ B).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u)) :
    tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
        (obj (free R) S.toCondensed) ⟶
      B)
Tactic: apply (ihomPoints R P B S).injective
-- Lean 4 proof step from Mathlib.Condensed.Light.InternallyProjective (hypothesis)
Goal:
R : Type u
inst : CommRing R
P : LightCondMod R
h_1 : InternallyProjective P
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g :
  tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
      (obj (free R) S.toCondensed) ⟶
    B
h : isInternallyProjective P
⊢ ∃ (S' : LightProfinite.{u}) (π : S' ⟶ S) (_ :
    Function.Surjective (α :=
      (fun
            (X :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
        S')
      (β :=
      (fun
            (X :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
        S)
      (⇑(ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u)))
            (CC :=
            fun
              (X :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u))
            π) :
        (a :
            (fun
                  (X :
                    CompHausLike fun (X : TopCat) ↦
                      TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
                (↑X.toTop : Type u))
              S') →
          (fun
                (X :
                  CompHausLike fun (X : TopCat) ↦
                    TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
              (↑X.toTop : Type u))
            S))
    (g' :
    tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (Presheaf.IsSheaf (coherentTopology LightProfinite))) P
        (obj (free R) S'.toCondensed) ⟶
      A),
    P ◁ CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ free R) π ≫ g = g' ≫ e
have hh : Epi (X := P ⟹ A) (CategoryTheory.Functor.map (ihom P) e)
Tactic: have hh := h.1 e
-- 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)).2 = x
⊢ (fibres π σ)ᶜ = ⋃ (i : X), (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {(↑i : OnePoint X)}
have h : ∀ (x : T),
  x ∈ (fibres π σ)ᶜ ↔
    Membership.mem (γ := Set T) (⋃ (i : X), (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {(↑i : OnePoint X)}) x
Tactic: ext x
-- 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)).2 = x
x : T
⊢ x ∈ (fibres π σ)ᶜ ↔
    Membership.mem (γ := Set T) (⋃ (i : X), (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {(↑i : OnePoint X)}) x
have h : (¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x) ↔
  ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)
Tactic: simp only [Set.mem_compl_iff, mem_fibres_iff, not_or, not_exists, Set.mem_iUnion,
    Set.mem_inter_iff, Set.mem_range, Set.mem_preimage, Function.comp_apply,
    Set.mem_singleton_iff]
-- 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)).2 = x
x : T
⊢ (¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x) ↔
    ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)
have h : (¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x) →
  ∀ (h₁ : ¬(π x).2 = none) (h₂ : ∀ (x_2 : X) (x_3 : S), ¬σ (Option.some x_2) x_3 = x),
    ∃ (i : X), (∀ (x_2 : S), ¬σ (Option.some i) x_2 = x) ∧ (π x).2 = (↑i : OnePoint X)
Tactic: refine ⟨fun ⟨h₁, h₂⟩ ↦ ?_, fun ⟨n, hn, hn'⟩ ↦ ?_⟩
-- 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)).2 = x
x : T
h :
  (¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x) →
    ∀ (h₁ : ¬(π x).2 = none) (h₂ : ∀ (x_2 : X) (x_3 : S), ¬σ (Option.some x_2) x_3 = x),
      ∃ (i : X), (∀ (x_2 : S), ¬σ (Option.some i) x_2 = x) ∧ (π x).2 = (↑i : OnePoint X)
⊢ (¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x) ↔
    ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)
have h₁ : (∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)) →
  ∀ (n : X) (hn : ∀ (x_2 : S), ¬σ (Option.some n) x_2 = x) (hn' : (π x).2 = (↑n : OnePoint X)),
    ¬(π x).2 = none ∧ ∀ (x_2 : X) (x_3 : S), ¬σ (Option.some x_2) x_3 = x
Tactic: refine ⟨fun ⟨h₁, h₂⟩ ↦ ?_, fun ⟨n, hn, hn'⟩ ↦ ?_⟩
-- 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)).2 = x
x : T
h : ¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
h₁ : ¬(π x).2 = none
h₂ : ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
⊢ ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)
have h : ∀ (n : X) (hn : (π x).2 = Option.some n),
  ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)
Tactic: obtain ⟨n, hn⟩ := Option.ne_none_iff_exists'.mp h₁
-- 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)).2 = x
x : T
h : ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
hn' : (π x).2 = (↑n : OnePoint X)
⊢ ¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
have h : ∀ (i : X) (s : S) (h : σ (Option.some i) s = x), σ (Option.some n) s = x
Tactic: refine ⟨by simpa [hn'] using Option.isSome_iff_ne_none.mp rfl, fun i s h ↦ hn s ?_⟩
-- 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 (Option X)
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
h_1 : ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
hn' : (π x).2 = (↑n : OnePoint X)
i : X
s : S
h : σ (Option.some i) s = x
⊢ σ (Option.some n) s = x
have hn'₁ : Option.some i = (↑n : OnePoint X)
Tactic: rw [← h, hσ'] at hn'
Cleared hypotheses: hn', h
-- 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)).2 = x
x : T
h_1 : ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
i : X
s : S
hn' : Option.some i = (↑n : OnePoint X)
h : σ (Option.some i) s = x
⊢ σ (Option.some n) s = x
have h₁ : σ (Option.some n) s = σ (Option.some i) s
Tactic: rw [← h, Option.some_injective _ hn'.symm]
-- 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)).2 = x
x : T
h_1 : ∃ (i : X), (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = (↑i : OnePoint X)
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
i : X
s : S
hn' : Option.some i = (↑n : OnePoint X)
h : σ (Option.some i) s = x
h₁ : σ (Option.some n) s = σ (Option.some i) s
⊢ σ (Option.some n) s = x
have h₂ : σ (Option.some i) s = σ (Option.some i) s
Tactic: rw [← h, Option.some_injective _ hn'.symm]