Theorem: ExtrDisc.isSheafForRegularSieve (ExtrDisc/ExplicitSheaves.lean)

State before:
X : ExtrDisc
S : Presieve X
hS : S ∈ RegularSieve X
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
⊢ IsSheafFor F S
Tactic:
obtain ⟨Y, f, rfl, hf⟩ := hS
State after:
case intro.intro.intro
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)

State before:
case intro.intro.intro
X : ExtrDisc
F : ExtrDiscᵒᵖ ⥤ Type (u + 1)
Y : ExtrDisc
f : Y ⟶ X
hf : Epi f
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)
Tactic:
have proj : Projective (toCompHaus.obj X) := inferInstanceAs (Projective X.compHaus)
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)
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)

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)
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)
Tactic:
have : Epi (toCompHaus.map f) := by
  rw [CompHaus.epi_iff_surjective]
  change Function.Surjective f
  rwa [← ExtrDisc.epi_iff_surjective]
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)
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)

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)
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)
Tactic:
set g := toCompHaus.preimage <| Projective.factorThru (𝟙 _) (toCompHaus.map f) with hg
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))
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)

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))
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)
Tactic:
have hfg : g ≫ f = 𝟙 _ := by
  refine' toCompHaus.map_injective _
  rw [map_comp, hg, image_preimage, Projective.factorThru_comp, CategoryTheory.Functor.map_id]
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
⊢ IsSheafFor F (ofArrows (fun x => Y) fun x => f)

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
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

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 => _⟩
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))

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]
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)

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
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

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]
State after:
no goals

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 _
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)

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]
State after:
no goals

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
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)

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 ()) ?_
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

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
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)

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]
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)

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
State after:
no goals

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]
State after:
no goals

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 ())
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))

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
State after:
no goals