internlm/Lean-Github huggingface dataset:
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
case intro.intro.intro
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)
Tactic:
intro y hy
Proof state after:
case intro.intro.intro
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
⊢ ∃! t, FamilyOfElements.IsAmalgamation y t
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
case intro.intro.intro
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
⊢ ∃! t, FamilyOfElements.IsAmalgamation y t
Tactic:
refine' ⟨F.map g.op <| y f <| ofArrows.mk (), fun Z h hZ => _, fun z hz => _⟩
Proof state after:
case intro.intro.intro.refine'_1
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
Z : ExtrDisc
h : Z ⟶ X
hZ : ofArrows (fun x => Y) (fun x => f) h
⊢ F.map h.op (F.map g.op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))) = y h hZ

case intro.intro.intro.refine'_2
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
z : F.obj X.op
hz : (fun t => FamilyOfElements.IsAmalgamation y t) z
⊢ z = F.map g.op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
⊢ Epi (toCompHaus.map f)
Tactic:
rw [CompHaus.epi_iff_surjective]
Proof state after:
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
⊢ Function.Surjective ↑(toCompHaus.map f)
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
⊢ Function.Surjective ↑(toCompHaus.map f)
Tactic:
change Function.Surjective f
Proof state after:
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
⊢ Function.Surjective ↑f
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
⊢ Function.Surjective ↑f
Tactic:
rwa [← ExtrDisc.epi_iff_surjective]
Proof state after:
no goals
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
⊢ g ≫ f = 𝟙 X
Tactic:
refine' toCompHaus.map_injective _
Proof state after:
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
⊢ toCompHaus.map (g ≫ f) = toCompHaus.map (𝟙 X)
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
⊢ toCompHaus.map (g ≫ f) = toCompHaus.map (𝟙 X)
Tactic:
rw [map_comp, hg, image_preimage, Projective.factorThru_comp, CategoryTheory.Functor.map_id]
Proof state after:
no goals
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
case intro.intro.intro.refine'_1
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
Z : ExtrDisc
h : Z ⟶ X
hZ : ofArrows (fun x => Y) (fun x => f) h
⊢ F.map h.op (F.map g.op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))) = y h hZ
Tactic:
cases' hZ with u
Proof state after:
case intro.intro.intro.refine'_1.mk
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
u : Unit
⊢ F.map f.op (F.map g.op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))) =
    y f (_ : ofArrows (fun x => Y) (fun x => f) f)
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
case intro.intro.intro.refine'_1.mk
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
u : Unit
⊢ F.map f.op (F.map g.op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))) =
    y f (_ : ofArrows (fun x => Y) (fun x => f) f)
Tactic:
have := hy (f₁ := f) (f₂ := f) (𝟙 Y) (f ≫ g) (ofArrows.mk ()) (ofArrows.mk ()) ?_
Proof state after:
case intro.intro.intro.refine'_1.mk.refine_2
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this✝ : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
u : Unit
this :
  F.map (𝟙 Y).op (y f (_ : ofArrows (fun x => Y) (fun x => f) f)) =
    F.map (f ≫ g).op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))
⊢ F.map f.op (F.map g.op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))) =
    y f (_ : ofArrows (fun x => Y) (fun x => f) f)

case intro.intro.intro.refine'_1.mk.refine_1
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
u : Unit
⊢ 𝟙 Y ≫ f = (f ≫ g) ≫ f
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
case intro.intro.intro.refine'_1.mk.refine_2
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this✝ : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
u : Unit
this :
  F.map (𝟙 Y).op (y f (_ : ofArrows (fun x => Y) (fun x => f) f)) =
    F.map (f ≫ g).op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))
⊢ F.map f.op (F.map g.op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))) =
    y f (_ : ofArrows (fun x => Y) (fun x => f) f)
Tactic:
rw [op_id, F.map_id, types_id_apply] at this
Proof state after:
case intro.intro.intro.refine'_1.mk.refine_2
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this✝ : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
u : Unit
this :
  y f (_ : ofArrows (fun x => Y) (fun x => f) f) = F.map (f ≫ g).op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))
⊢ F.map f.op (F.map g.op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))) =
    y f (_ : ofArrows (fun x => Y) (fun x => f) f)
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
case intro.intro.intro.refine'_1.mk.refine_2
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this✝ : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
u : Unit
this :
  y f (_ : ofArrows (fun x => Y) (fun x => f) f) = F.map (f ≫ g).op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))
⊢ F.map f.op (F.map g.op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))) =
    y f (_ : ofArrows (fun x => Y) (fun x => f) f)
Tactic:
rw [← types_comp_apply (F.map g.op) (F.map f.op), ← F.map_comp, ← op_comp]
Proof state after:
case intro.intro.intro.refine'_1.mk.refine_2
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this✝ : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
u : Unit
this :
  y f (_ : ofArrows (fun x => Y) (fun x => f) f) = F.map (f ≫ g).op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))
⊢ F.map (f ≫ g).op (y f (_ : ofArrows (fun x => Y) (fun x => f) f)) = y f (_ : ofArrows (fun x => Y) (fun x => f) f)
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
case intro.intro.intro.refine'_1.mk.refine_2
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this✝ : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
u : Unit
this :
  y f (_ : ofArrows (fun x => Y) (fun x => f) f) = F.map (f ≫ g).op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))
⊢ F.map (f ≫ g).op (y f (_ : ofArrows (fun x => Y) (fun x => f) f)) = y f (_ : ofArrows (fun x => Y) (fun x => f) f)
Tactic:
exact this.symm
Proof state after:
no goals
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
case intro.intro.intro.refine'_1.mk.refine_1
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
u : Unit
⊢ 𝟙 Y ≫ f = (f ≫ g) ≫ f
Tactic:
rw [Category.id_comp, Category.assoc, hfg, Category.comp_id]
Proof state after:
no goals
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
case intro.intro.intro.refine'_2
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
z : F.obj X.op
hz : (fun t => FamilyOfElements.IsAmalgamation y t) z
⊢ z = F.map g.op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))
Tactic:
have := congr_arg (F.map g.op) <| hz f (ofArrows.mk ())
Proof state after:
case intro.intro.intro.refine'_2
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this✝ : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
z : F.obj X.op
hz : (fun t => FamilyOfElements.IsAmalgamation y t) z
this : F.map g.op (F.map f.op z) = F.map g.op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))
⊢ z = F.map g.op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))
Theorem: ExtrDisc.isSheafForRegularSieve
Proof state before:
case intro.intro.intro.refine'_2
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
proj : Projective (toCompHaus.obj X)
this✝ : Epi (toCompHaus.map f)
g : X ⟶ Y := toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hg : g = toCompHaus.preimage (Projective.factorThru (𝟙 (toCompHaus.obj X)) (toCompHaus.map f))
hfg : g ≫ f = 𝟙 X
y : FamilyOfElements F (ofArrows (fun x => Y) fun x => f)
hy : FamilyOfElements.Compatible y
z : F.obj X.op
hz : (fun t => FamilyOfElements.IsAmalgamation y t) z
this : F.map g.op (F.map f.op z) = F.map g.op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))
⊢ z = F.map g.op (y f (_ : ofArrows (fun x => Y) (fun x => f) f))
Tactic:
rwa [← types_comp_apply (F.map f.op) (F.map g.op), ← F.map_comp, ← op_comp, hfg, op_id,
  F.map_id, types_id_apply] at this
Proof state after:
no goals
Theorem: ExtrDisc.isSheafFor_of_extensiveRegular
Proof state before:
EverythinProj_ExtrDisc : EverythingIsProjective ExtrDisc
X : ExtrDisc
S : Presieve X
hS :
  S ∈
    Coverage.covering
      (ExtensiveRegularCoverage ExtrDisc EverythinProj_ExtrDisc
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst)))
      X
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
hF : PreservesFiniteProducts F
⊢ IsSheafFor F S
Tactic:
cases' hS with hSIso hSSingle
Proof state after:
case inl
EverythinProj_ExtrDisc : EverythingIsProjective ExtrDisc
X : ExtrDisc
S : Presieve X
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
hF : PreservesFiniteProducts F
hSIso : S ∈ ExtensiveSieve X
⊢ IsSheafFor F S

case inr
EverythinProj_ExtrDisc : EverythingIsProjective ExtrDisc
X : ExtrDisc
S : Presieve X
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
hF : PreservesFiniteProducts F
hSSingle : S ∈ RegularSieve X
⊢ IsSheafFor F S
Theorem: ExtrDisc.isSheafFor_of_extensiveRegular
Proof state before:
case inl
EverythinProj_ExtrDisc : EverythingIsProjective ExtrDisc
X : ExtrDisc
S : Presieve X
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
hF : PreservesFiniteProducts F
hSIso : S ∈ ExtensiveSieve X
⊢ IsSheafFor F S
Tactic:
exact isSheafForExtensiveSieve hSIso hF
Proof state after:
no goals
Theorem: ExtrDisc.isSheafFor_of_extensiveRegular
Proof state before:
case inr
EverythinProj_ExtrDisc : EverythingIsProjective ExtrDisc
X : ExtrDisc
S : Presieve X
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
hF : PreservesFiniteProducts F
hSSingle : S ∈ RegularSieve X
⊢ IsSheafFor F S
Tactic:
exact isSheafForRegularSieve hSSingle F
Proof state after:
no goals
Theorem: ExtrDisc.final
Proof state before:
A : Type (u + 2)
inst✝ : Category A
F : ExtrDiscᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) F
Tactic:
rw [← extensiveRegular_generates_coherent]
Proof state after:
A : Type (u + 2)
inst✝ : Category A
F : ExtrDiscᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
⊢ Presheaf.IsSheaf
    (Coverage.toGrothendieck ExtrDisc
      (ExtensiveRegularCoverage ExtrDisc everything_proj
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
    F
Theorem: ExtrDisc.final
Proof state before:
A : Type (u + 2)
inst✝ : Category A
F : ExtrDiscᵒᵖ ⥤ A
hF : PreservesFiniteProducts F
⊢ Presheaf.IsSheaf
    (Coverage.toGrothendieck ExtrDisc
      (ExtensiveRegularCoverage ExtrDisc everything_proj
        (_ :
          ∀ {α : Type} [inst : Fintype α] {X : ExtrDisc} {Z : α → ExtrDisc} (π : (a : α) → Z a ⟶ X) {Y : ExtrDisc}
            (f : Y ⟶ X) (x : IsIso (Sigma.desc π)), IsIso (Sigma.desc fun x_1 => Limits.pullback.fst))))
    F
Tactic:
exact fun E => (Presieve.isSheaf_coverage _ _).2 <| fun S hS => isSheafFor_of_extensiveRegular hS
  ⟨fun J inst => have := hF.1; compPreservesLimitsOfShape _ _⟩
Proof state after:
no goals
Theorem: descOpCompCoprodToProd
Proof state before:
C : Type u_2
inst✝² : Category C
α : Type
inst✝¹ : Finite α
Z : α → C
inst✝ : HasFiniteCoproducts C
X✝ : C
π✝ : (a : α) → Z a ⟶ X✝
X : C
π : (a : α) → Z a ⟶ X
⊢ (Sigma.desc π).op ≫ (CoprodToProd Z).hom = Pi.lift fun a => (π a).op
Tactic:
refine' limit.hom_ext (fun a => _)
Proof state after:
C : Type u_2
inst✝² : Category C
α : Type
inst✝¹ : Finite α
Z : α → C
inst✝ : HasFiniteCoproducts C
X✝ : C
π✝ : (a : α) → Z a ⟶ X✝
X : C
π : (a : α) → Z a ⟶ X
a : Discrete α
⊢ ((Sigma.desc π).op ≫ (CoprodToProd Z).hom) ≫ limit.π (Discrete.functor fun z => (Z z).op) a =
    (Pi.lift fun a => (π a).op) ≫ limit.π (Discrete.functor fun z => (Z z).op) a
Theorem: descOpCompCoprodToProd
Proof state before:
C : Type u_2
inst✝² : Category C
α : Type
inst✝¹ : Finite α
Z : α → C
inst✝ : HasFiniteCoproducts C
X✝ : C
π✝ : (a : α) → Z a ⟶ X✝
X : C
π : (a : α) → Z a ⟶ X
a : Discrete α
⊢ ((Sigma.desc π).op ≫ (CoprodToProd Z).hom) ≫ limit.π (Discrete.functor fun z => (Z z).op) a =
    (Pi.lift fun a => (π a).op) ≫ limit.π (Discrete.functor fun z => (Z z).op) a
Tactic:
simp only [CoprodToProd, Category.assoc, limit.conePointUniqueUpToIso_hom_comp, oppositeFan_pt, 
  oppositeFan_π_app, limit.lift_π, Fan.mk_pt, Fan.mk_π_app, ← op_comp, colimit.ι_desc]
Proof state after:
C : Type u_2
inst✝² : Category C
α : Type
inst✝¹ : Finite α
Z : α → C
inst✝ : HasFiniteCoproducts C
X✝ : C
π✝ : (a : α) → Z a ⟶ X✝
X : C
π : (a : α) → Z a ⟶ X
a : Discrete α
⊢ ((Cofan.mk X π).ι.app { as := a.as }).op = (π a.as).op
Theorem: descOpCompCoprodToProd
Proof state before:
C : Type u_2
inst✝² : Category C
α : Type
inst✝¹ : Finite α
Z : α → C
inst✝ : HasFiniteCoproducts C
X✝ : C
π✝ : (a : α) → Z a ⟶ X✝
X : C
π : (a : α) → Z a ⟶ X
a : Discrete α
⊢ ((Cofan.mk X π).ι.app { as := a.as }).op = (π a.as).op
Tactic:
rfl
Proof state after:
no goals
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
⊢ CoverDense (coherentTopology CompHaus) ExtrDisc.toCompHaus
Tactic:
constructor
Proof state after:
case is_cover

⊢ ∀ (U : CompHaus), Sieve.coverByImage ExtrDisc.toCompHaus U ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) U
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case is_cover

⊢ ∀ (U : CompHaus), Sieve.coverByImage ExtrDisc.toCompHaus U ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) U
Tactic:
intro B
Proof state after:
case is_cover
B : CompHaus
⊢ Sieve.coverByImage ExtrDisc.toCompHaus B ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case is_cover
B : CompHaus
⊢ Sieve.coverByImage ExtrDisc.toCompHaus B ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Tactic:
let T := Presieve.singleton B.presentationπ
Proof state after:
case is_cover
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
⊢ Sieve.coverByImage ExtrDisc.toCompHaus B ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case is_cover
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
⊢ Sieve.coverByImage ExtrDisc.toCompHaus B ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Tactic:
let S := Sieve.generate T
Proof state after:
case is_cover
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
⊢ Sieve.coverByImage ExtrDisc.toCompHaus B ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case is_cover
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
⊢ Sieve.coverByImage ExtrDisc.toCompHaus B ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Tactic:
convert hS
Proof state after:
case h.e'_4
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
⊢ Sieve.coverByImage ExtrDisc.toCompHaus B = S
Theorem: Condensed.ExtrDiscCompHaus.coverDense
Proof state before:
case h.e'_4
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
⊢ Sieve.coverByImage ExtrDisc.toCompHaus B = S
Tactic:
ext Y f
Proof state after:
case h.e'_4.h
B : CompHaus
T : Presieve B := Presieve.singleton (CompHaus.presentationπ B)
S : Sieve B := Sieve.generate T
hS : S ∈ GrothendieckTopology.sieves (coherentTopology CompHaus) B
Y : CompHaus
f : Y ⟶ B
⊢ (Sieve.coverByImage ExtrDisc.toCompHaus B).arrows f ↔ S.arrows f