mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsLimit c
s : Cone F
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
convert! continuous_iff_le_induced.1 (s.π.app j).hom.continuous

Goal state after:
case e'_4.e'_3
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsLimit c
s : Cone F
j : J
e_1✝¹ : TopologicalSpace ↑s.1 = TopologicalSpace ↑(((Functor.const J).obj s.pt).obj j)
e_1✝ : ↑s.1 = ↑(((Functor.const J).obj s.pt).obj j)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case property.refine_3.fst
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ (pullbackCone f g).fst = S.fst
h₂ : m ≫ (pullbackCone f g).snd = S.snd
x : ↑S.pt
⊢ (↑((ConcreteCategory.hom m) x)).1 =
    (↑((ConcreteCategory.hom
            (ofHom
              { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
                continuous_toFun := ⋯ }))
          x)).1

pp: case property.refine_3.snd
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ (pullbackCone f g).fst = S.fst
h₂ : m ≫ (pullbackCone f g).snd = S.snd
x : ↑S.pt
⊢ (↑((ConcreteCategory.hom m) x)).2 =
    (↑((ConcreteCategory.hom
            (ofHom
              { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
                continuous_toFun := ⋯ }))
          x)).2

Tactic:
· simpa using! ConcreteCategory.congr_hom h₁ x

Goal state after:
case property.refine_3.snd
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ (pullbackCone f g).fst = S.fst
h₂ : m ≫ (pullbackCone f g).snd = S.snd
x : ↑S.pt
⊢ (↑((ConcreteCategory.hom m) x)).2 =
    (↑((ConcreteCategory.hom
            (ofHom
              { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
                continuous_toFun := ⋯ }))
          x)).2
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
ι : Type v
β : ι → TopCat
⊢ ∀ (s : Cocone (Discrete.functor β)) (m : (sigmaCofan β).pt ⟶ s.pt),
    (∀ (j : Discrete ι), (sigmaCofan β).ι.app j ≫ m = s.ι.app j) →
      m = ofHom { toFun := fun s_1 ↦ (ConcreteCategory.hom (s.ι.app { as := s_1.fst })) s_1.snd, continuous_toFun := ⋯ }

Tactic:
by
    intro S m h
    ext ⟨i, x⟩
    simp only [← h]
    congr

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mp
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
y : ↑(pullback f₁ f₂)
⊢ (∃ y_1, (ConcreteCategory.hom i₁) y_1 = (ConcreteCategory.hom (pullback.fst f₁ f₂ ≫ i₁)) y) ∧
    ∃ y_1, (ConcreteCategory.hom i₂) y_1 = (ConcreteCategory.hom (pullback.snd f₁ f₂ ≫ i₂)) y

Tactic:
exact ⟨exists_apply_eq_apply _ _, exists_apply_eq_apply _ _⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ (const J).map e.inv.hom = c.ι
j : J
⊢ IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j)

Tactic:
rw [← Category.comp_id (α.app j)]

Goal state after:
J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ (const J).map e.inv.hom = c.ι
j : J
⊢ IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.hom) (c.ι.app j)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (const J).map e.inv.hom = c.ι
j : J
| IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j)

Tactic:
rw [← Category.comp_id (α.app j)]

Goal state after:
J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (const J).map e.inv.hom = c.ι
j : J
| IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.hom) (c.ι.app j)
Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan X
hc : IsColimit c
inst✝ : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial (s hij).pt
d : Cofan X
hd : IsColimit d
i : ι
⊢ Mono (d.inj i)

Tactic:
rw [show d.inj i = c.inj i ≫ (hd.uniqueUpToIso hc).inv.hom by simp]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
X : ι → C
c : Cofan X
hc : IsColimit c
inst✝ : ∀ (i : ι), Mono (c.inj i)
s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)
hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)
H : {i j : ι} → (hij : i ≠ j) → IsInitial (s hij).pt
d : Cofan X
hd : IsColimit d
i : ι
⊢ Mono (c.inj i ≫ (hd.uniqueUpToIso hc).inv.hom)
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
hf : P.isLocal f
⊢ IsIso f

Tactic:
obtain ⟨g, hg⟩ := (hf _ hX).2 (𝟙 X)

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hX : P X
hY : P Y
hf : P.isLocal f
g : Y ⟶ X
hg : (fun g ↦ f ≫ g) g = 𝟙 X
⊢ IsIso f
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: J : Type v'
inst✝⁵ : Category.{u', v'} J
C : Type u
inst✝⁴ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
D : Type u''
inst✝³ : Category.{v'', u''} D
inst✝² : Adhesive C
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts C
⊢ ∀ {W X Y Z : D ⥤ C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Mono f] (H : IsPushout f g h i), H.IsVanKampen

Tactic:
intro W X Y Z f g h i hf H

Goal state after:
J : Type v'
inst✝⁵ : Category.{u', v'} J
C : Type u
inst✝⁴ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
D : Type u''
inst✝³ : Category.{v'', u''} D
inst✝² : Adhesive C
inst✝¹ : HasPullbacks C
inst✝ : HasPushouts C
W X Y Z : D ⥤ C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ H.IsVanKampen
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u''
inst✝⁵ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁴ : Adhesive D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
inst✝³ : PreservesLimitsOfShape WalkingCospan F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : ReflectsColimitsOfShape WalkingSpan F
⊢ ∀ {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Mono f] (H : IsPushout f g h i), H.IsVanKampen

Tactic:
intro W X Y Z f g h i hf H

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u''
inst✝⁵ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁴ : Adhesive D
H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Mono f], HasPullback f g
H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
inst✝³ : PreservesLimitsOfShape WalkingCospan F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape WalkingSpan F
inst✝ : ReflectsColimitsOfShape WalkingSpan F
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
hf : Mono f
H : IsPushout f g h i
⊢ H.IsVanKampen
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
⊢ P ≤ P.isLocal.isLocal

Tactic:
by
  rw [← le_isLocal_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsIso (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι ↔
    IsIso { hom := (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι }

Tactic:
exact isIso_iff_of_reflects_iso (f := Sheaf.imageι f) (F := sheafToPresheaf J (Type w))

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings

Goal state before:
pp: C : Type u'
inst✝¹ : Category.{v', u'} C
J : GrothendieckTopology C
R R' : Cᵒᵖ ⥤ RingCat
α : R ⟶ R'
M₁ M₂ : PresheafOfModules R'
hM₂ : Presheaf.IsSheaf J M₂.presheaf
inst✝ : Presheaf.IsLocallySurjective J α
g : (restrictScalars α).obj M₁ ⟶ (restrictScalars α).obj M₂
X : Cᵒᵖ
r' : ↑(R'.obj X)
m : ↑(M₁.obj X)
⊢ ∀ (Y : C) (f : Y ⟶ Opposite.unop X),
    (Presheaf.imageSieve α r').arrows f →
      (ConcreteCategory.hom (M₂.presheaf.map f.op)) ((ConcreteCategory.hom (((toPresheaf R).map g).app X)) (r' • m)) =
        (ConcreteCategory.hom (M₂.presheaf.map f.op)) (r' • (ConcreteCategory.hom (((toPresheaf R).map g).app X)) m)

Tactic:
rintro Y p ⟨r : R.obj _, hr⟩

Goal state after:
C : Type u'
inst✝¹ : Category.{v', u'} C
J : GrothendieckTopology C
R R' : Cᵒᵖ ⥤ RingCat
α : R ⟶ R'
M₁ M₂ : PresheafOfModules R'
hM₂ : Presheaf.IsSheaf J M₂.presheaf
inst✝ : Presheaf.IsLocallySurjective J α
g : (restrictScalars α).obj M₁ ⟶ (restrictScalars α).obj M₂
X : Cᵒᵖ
r' : ↑(R'.obj X)
m : ↑(M₁.obj X)
Y : C
p : Y ⟶ Opposite.unop X
r : ↑(R.obj (Opposite.op Y))
hr : (ConcreteCategory.hom (α.app (Opposite.op Y))) r = (ConcreteCategory.hom (R'.map p.op)) r'
⊢ (ConcreteCategory.hom (M₂.presheaf.map p.op)) ((ConcreteCategory.hom (((toPresheaf R).map g).app X)) (r' • m)) =
    (ConcreteCategory.hom (M₂.presheaf.map p.op)) (r' • (ConcreteCategory.hom (((toPresheaf R).map g).app X)) m)
Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
s : Cofork (Sigma.map' f fun x ↦ 𝟙 R) 0
m : (sigmaConstCokernelCofork R f).pt ⟶ s.pt
hm : Cofork.π (sigmaConstCokernelCofork R f) ≫ m = s.π
⊢ m = Sigma.desc fun x ↦ Sigma.ι (fun x ↦ R) ↑x ≫ s.π

Tactic:
ext ⟨b, hb⟩

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
s : Cofork (Sigma.map' f fun x ↦ 𝟙 R) 0
m : (sigmaConstCokernelCofork R f).pt ⟶ s.pt
hm : Cofork.π (sigmaConstCokernelCofork R f) ≫ m = s.π
b : β
hb : b ∈ (Set.range f)ᶜ
⊢ Sigma.ι (fun x ↦ R) ⟨b, hb⟩ ≫ m = Sigma.ι (fun x ↦ R) ⟨b, hb⟩ ≫ Sigma.desc fun x ↦ Sigma.ι (fun x ↦ R) ↑x ≫ s.π
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j k : Bicone J
f g : BiconeHom J j k
⊢ Decidable (f = g)

Tactic:
cases f <;> cases g

Goal state after:
case left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable (left_id = left_id)

case right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable (right_id = right_id)

case left.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable (left j✝ = left j✝)

case right.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable (right j✝ = right j✝)

case diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝¹ f✝ : j✝ ⟶ k✝
⊢ Decidable (diagram f✝¹ = diagram f✝)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
W✝ X✝ Y✝ Z✝ : Bicone J
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
cases f <;> cases g

Goal state after:
case left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
h : Bicone.left ⟶ Z✝
⊢ (BiconeHom.left_id ≫ BiconeHom.left_id) ≫ h = BiconeHom.left_id ≫ BiconeHom.left_id ≫ h

case left_id.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
h : Bicone.diagram j✝ ⟶ Z✝
⊢ (BiconeHom.left_id ≫ BiconeHom.left j✝) ≫ h = BiconeHom.left_id ≫ BiconeHom.left j✝ ≫ h

case right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
h : Bicone.right ⟶ Z✝
⊢ (BiconeHom.right_id ≫ BiconeHom.right_id) ≫ h = BiconeHom.right_id ≫ BiconeHom.right_id ≫ h

case right_id.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
h : Bicone.diagram j✝ ⟶ Z✝
⊢ (BiconeHom.right_id ≫ BiconeHom.right j✝) ≫ h = BiconeHom.right_id ≫ BiconeHom.right j✝ ≫ h

case left.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
h : Bicone.diagram k✝ ⟶ Z✝
⊢ (BiconeHom.left j✝ ≫ BiconeHom.diagram f✝) ≫ h = BiconeHom.left j✝ ≫ BiconeHom.diagram f✝ ≫ h

case right.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
h : Bicone.diagram k✝ ⟶ Z✝
⊢ (BiconeHom.right j✝ ≫ BiconeHom.diagram f✝) ≫ h = BiconeHom.right j✝ ≫ BiconeHom.diagram f✝ ≫ h

case diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝¹ : J
f✝¹ : j✝ ⟶ k✝¹
k✝ : J
f✝ : k✝¹ ⟶ k✝
h : Bicone.diagram k✝ ⟶ Z✝
⊢ (BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝) ≫ h = BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝ ≫ h
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
S T : C
E✝¹ : PreZeroHypercover S
F✝¹ : PreZeroHypercover S
E✝ : PreZeroHypercover S
F✝ : PreZeroHypercover S
G : PreZeroHypercover S
E F : PreZeroHypercover S
e : E ≅ F
i : E.I₀
⊢ e.hom.h₀ i ≫ e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯ = 𝟙 (E.X i) ∧
    (e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯) ≫ e.hom.h₀ i = 𝟙 (F.X (e.hom.s₀ i))

Tactic:
rw [hom_inv_h₀_assoc, eqToHom_trans, eqToHom_refl, Category.assoc,
    ← eqToHom_naturality _ (by simp), inv_hom_h₀_assoc]

Goal state after:
case h
C : Type u
inst✝ : Category.{v, u} C
S T : C
E✝¹ : PreZeroHypercover S
F✝¹ : PreZeroHypercover S
E✝ : PreZeroHypercover S
F✝ : PreZeroHypercover S
G : PreZeroHypercover S
E F : PreZeroHypercover S
e : E ≅ F
i : E.I₀
⊢ 𝟙 (E.X i) = 𝟙 (E.X i) ∧ eqToHom ⋯ ≫ eqToHom ⋯ = 𝟙 (F.X (e.hom.s₀ i))
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
⊢ ∃ W x x, True

pp: case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
⊢ ∃ W h, h ≫ f = h ≫ g

Tactic:
· let U := IsCofiltered.min (T.obj A) (T.obj B)
    let A' : StructuredArrow U.right F := .mk (IsCofiltered.minToLeft (T.obj A) (T.obj B)).right
    let B' : StructuredArrow U.right F := .mk (IsCofiltered.minToRight (T.obj A) (T.obj B)).right
    refine ⟨.mk <| U.hom ≫ G.map (IsCofiltered.min A' B').hom,
      StructuredArrow.homMk (IsCofiltered.minToLeft A' B').right ?_,
      StructuredArrow.homMk (IsCofiltered.minToRight A' B').right ?_, trivial⟩
    · simp [← Functor.map_comp, A', T]
    · simp [← Functor.map_comp, B', T]

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
⊢ ∃ W h, h ≫ f = h ≫ g
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
⊢ ∃ W h, h ≫ f = h ≫ g

Tactic:
let U := IsCofiltered.eq (T.map f) (T.map g)

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
U : StructuredArrow X G := IsCofiltered.eq (T.map f) (T.map g)
⊢ ∃ W h, h ≫ f = h ≫ g
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case refine_1
C : Type u_2
inst✝ : Category.{v_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
y₁ y₂ : P.obj (Opposite.op X)
h₁ : x.IsAmalgamation y₁
h₂ : x.IsAmalgamation y₂
Y : C
g : Y ⟶ X
hg : S g
⊢ (ConcreteCategory.hom (P.map g.op)) y₁ = (ConcreteCategory.hom (P.map g.op)) y₂

Tactic:
simp only [← h2 hg, op_comp, P.map_comp, types_comp_apply, h₁ _ (h1 _), h₂ _ (h1 _)]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S : Sieve T
⊢ S ∈ J.toCoverage.toGrothendieck T ↔ ∃ R ∈ J.coverings T, R ≤ S.arrows

Tactic:
Coverage.mem_toGrothendieck

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S : Sieve T
⊢ J.toCoverage.Saturate T S ↔ ∃ R ∈ J.coverings T, R ≤ S.arrows
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → Presieve.FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg ↦ x (gg ≫ g) ⋯
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), (y g).IsAmalgamation (z hg)
q : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg ↦ z hg
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
h₁ : (Sieve.pullback f R).arrows f₁
h₂ : (Sieve.pullback f R).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback g₁ (Sieve.pullback (f₁ ≫ f) S)).arrows gg
⊢ (gg ≫ g₁) ≫ f₁ = (gg ≫ g₂) ≫ f₂

Tactic:
simp only [Category.assoc, h]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : G.PreservesLeftKanExtension F L
inst✝ : L.HasLeftKanExtension F
⊢ whiskerRight (L.leftKanExtensionUnit F) G ≫
      (L.associator (L.leftKanExtension F) G).hom ≫ L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F L).hom =
    L.leftKanExtensionUnit (F ⋙ G)

Tactic:
by
  simpa [leftKanExtensionCompIsoOfPreserves] using
    descOfIsLeftKanExtension_fac
      (α := whiskerRight (L.leftKanExtensionUnit F) G ≫ (Functor.associator _ _ _).hom)
      (β := L.leftKanExtensionUnit (F ⋙ G))

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E✝ : Type u₃
inst✝ : Category.{v₃, u₃} E✝
X : C
E : PreOneHypercover X
F : C ⥤ D
x✝¹ x✝ : (PreZeroHypercover.map F E.toPreZeroHypercover).I₀
j : E.I₁ x✝¹ x✝
⊢ F.map (E.p₁ j) ≫ (PreZeroHypercover.map F E.toPreZeroHypercover).f x✝¹ =
    F.map (E.p₂ j) ≫ (PreZeroHypercover.map F E.toPreZeroHypercover).f x✝

Tactic:
by simpa using! F.congr_map (E.w j)

Goal state after: