mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasWeakSheafify J D
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
k : K
⊢ ((presheafToSheaf J D).map (E.ι.app k)).hom =
    ((sheafificationAdjunction J D).counit.app (F.obj k)).hom ≫ toSheafify J (F.obj k).obj ≫ sheafifyMap J (E.ι.app k)

Tactic:
sheafificationAdjunction_counit_app_val,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasWeakSheafify J D
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
k : K
⊢ ((presheafToSheaf J D).map (E.ι.app k)).hom =
    sheafifyLift J (𝟙 (F.obj k).obj) ⋯ ≫ toSheafify J (F.obj k).obj ≫ sheafifyMap J (E.ι.app k)
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
K : Type u_1
inst✝¹ : Category.{v_1, u_1} K
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : J ⥤ C
c : Cocone F
h : IsUniversalColimit c
j : J
⊢ IsPullback (c.ι.app j) ((𝟙 F).app j) (𝟙 c.pt) (c.ι.app j)

Tactic:
have : IsIso (𝟙 c.pt) := inferInstance

Goal state after:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
K : Type u_1
inst✝¹ : Category.{v_1, u_1} K
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : J ⥤ C
c : Cocone F
h : IsUniversalColimit c
j : J
this : IsIso (𝟙 c.pt)
⊢ IsPullback (c.ι.app j) ((𝟙 F).app j) (𝟙 c.pt) (c.ι.app j)
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : IsEmbedding ⇑(ConcreteCategory.hom g)
H : Set.range ⇑(ConcreteCategory.hom f) ⊆ Set.range ⇑(ConcreteCategory.hom g)
esto : ↑(pullback f g) ≃ₜ ↑X :=
  ⋯.toHomeomorph.trans
    { toFun := Subtype.val, invFun := fun x ↦ ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
      continuous_invFun := ⋯ }
⊢ IsIso (pullback.fst f g)

Tactic:
convert! (isoOfHomeo esto).isIso_hom

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
H : Set.range ⇑(ConcreteCategory.hom g) ⊆ Set.range ⇑(ConcreteCategory.hom f)
esto : ↑(pullback f g) ≃ₜ ↑Y :=
  ⋯.toHomeomorph.trans
    { toFun := Subtype.val, invFun := fun x ↦ ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
      continuous_invFun := ⋯ }
⊢ IsIso (pullback.snd f g)

Tactic:
convert! (isoOfHomeo esto).isIso_hom

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

Goal state before:
pp: case pos
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous
    ((range ⇑(ConcreteCategory.hom c.inl)).domRestrict fun x ↦
      if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
        (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
      else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩))

Tactic:
convert_to Continuous (f ∘ h₁.isEmbedding.toHomeomorph.symm)

Goal state after:
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ ((range ⇑(ConcreteCategory.hom c.inl)).domRestrict fun x ↦
      if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
        (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
      else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩)) =
    ⇑(ConcreteCategory.hom f) ∘ ⇑⋯.toHomeomorph.symm

case pos
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
f : X ⟶ T
g : Y ⟶ T
⊢ Continuous (⇑(ConcreteCategory.hom f) ∘ ⇑⋯.toHomeomorph.symm)
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
⊢ ⇑(ConcreteCategory.hom (pullback.snd f g)) '' ⇑(ConcreteCategory.hom (pullback.fst f g)) ⁻¹' U =
    ⇑(ConcreteCategory.hom g) ⁻¹' ⇑(ConcreteCategory.hom f) '' U

Tactic:
by
  ext x
  constructor
  · rintro ⟨y, hy, rfl⟩
    exact
      ⟨(pullback.fst f g) y, hy, CategoryTheory.congr_fun pullback.condition y⟩
  · rintro ⟨y, hy, eq⟩
  -- next 5 lines were
  -- `exact ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq⟩, by simpa, by simp⟩` before https://github.com/leanprover-community/mathlib4/pull/13170
    refine ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq⟩, ?_, ?_⟩
    · simp only [coe_of, Set.mem_preimage]
      convert! hy
      rw [pullbackIsoProdSubtype_inv_fst_apply]
    · rw [pullbackIsoProdSubtype_inv_snd_apply]

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

Goal state before:
pp: case refine_2
J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit c
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
this✝⁴ : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this✝³ : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this✝² : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.1 ((𝟭 C).obj X)))
this✝¹ : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
c'' : Cocone (F' ⋙ Gr) :=
  { pt := pullback (Gr.map f) (adj.unit.app c.pt),
    ι := { app := fun j ↦ pullback.lift (Gr.map (c'.ι.app j)) (Gr.map (α'.app j) ≫ c.ι.app j) ⋯, naturality := ⋯ } }
cf : (Cocone.precompose β.hom).obj c' ⟶ Gl.mapCocone c'' :=
  {
    hom :=
      pullback.lift (inv (adj.counit.app c'.pt)) f ⋯ ≫ (PreservesPullback.iso Gl (Gr.map f) (adj.unit.app c.pt)).inv,
    w := ⋯ }
this✝ :
  cf.hom ≫
      (PreservesPullback.iso Gl (Gr.map f) (adj.unit.app c.pt)).hom ≫
        pullback.fst (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt)) ≫ adj.counit.app c'.pt =
    𝟙 ((Cocone.precompose β.hom).obj c').pt
this : IsIso cf
⊢ ∀ (j : J),
    IsPullback (c''.ι.app j) ((whiskerRight α' Gr).app j) (pullback.snd (Gr.map f) (adj.unit.app c.pt)) (c.ι.app j)

Tactic:
intro j
    apply IsPullback.of_right _ _ (IsPullback.of_hasPullback _ _)
    · dsimp [α', c'']
      simp only [Category.comp_id, Category.id_comp, Category.assoc, Functor.map_comp,
        pullback.lift_fst]
      rw [← Category.comp_id (Gr.map f)]
      refine ((hc' j).map Gr).paste_vert (IsPullback.of_vert_isIso ⟨?_⟩)
      rw [← adj.unit_naturality, Category.comp_id, ← Category.assoc,
        ← Category.id_comp (Gr.map ((Gl.mapCocone c).ι.app j))]
      congr 1
      rw [← cancel_mono (Gr.map (adj.counit.app (F.obj j)))]
      dsimp
      simp only [Category.comp_id, Adjunction.right_triangle_components, Category.id_comp,
        Category.assoc]
    · dsimp [c'']
      simp only [pullback.lift_snd]

Goal state after:
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✝
inst✝² : Adhesive C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
K : C
f g : K ⟶ pushout (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (fst a b) (snd a b) := inr (fst a b) (snd a b)
this✝¹ : Mono u := mono_of_isPushout_of_mono_right (of_hasPushout (fst a b) (snd a b))
this✝ : Mono v := mono_of_isPushout_of_mono_left (of_hasPushout (fst a b) (snd a b))
sq_f_u : IsPullback (fst f u) (snd f u) f u := of_hasPullback f u
sq_f_v : IsPullback (fst f v) (snd f v) f v := of_hasPullback f v
sq_g_u : IsPullback (fst g u) (snd g u) g u := of_hasPullback g u
sq_g_v : IsPullback (fst g v) (snd g v) g v := of_hasPullback g v
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
w✝² : C
f' : w✝² ⟶ pullback f u
w✝¹ : w✝² ⟶ pullback f v
w✝ : w✝² ⟶ pullback a b
p₁ : IsPullback f' w✝ (snd f u) (fst a b)
left✝ : IsPullback w✝¹ w✝ (snd f v) (snd a b)
h₁ : IsPushout f' w✝¹ (fst f u) (fst f v)
this : Mono f' := Eq.mpr (id (congrArg (fun _a ↦ Mono _a) (Eq.symm (isoPullback_hom_fst p₁)))) inferInstance
sq₁₁ : IsPullback (fst m₁ l₁) (snd m₁ l₁) m₁ l₁ := of_hasPullback m₁ l₁
sq₁₂ : IsPullback (fst m₁ l₂) (snd m₁ l₂) m₁ l₂ := of_hasPullback m₁ l₂
⊢ Mono (u ≫ pushout.desc a b ⋯)

Tactic:
by rwa [pushout.inl_desc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
⊢ ∀ (A : C) (f : A ⟶ ⊥_ C), IsIso f

Tactic:
intro A f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ IsIso f
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
⊢ ∀ (A : C) (f : A ⟶ ⊥_ C), IsIso f

Tactic:
intro A f
      suffices IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A)) by
        obtain ⟨l, h₁, h₂⟩ := Limits.BinaryCofan.IsColimit.desc' this (f ≫ initial.to A) (𝟙 A)
        rcases (Category.id_comp _).symm.trans h₂ with rfl
        exact ⟨⟨_, ((Category.id_comp _).symm.trans h₁).symm, initialIsInitial.hom_ext _ _⟩⟩
      refine (H (BinaryCofan.mk (𝟙 _) (𝟙 _)) (mapPair f f) f (by ext ⟨⟨⟩⟩ <;> simp)
        (.of_discrete _) ?_).some
      rintro ⟨⟨⟩⟩ <;> dsimp <;>
        exact IsPullback.of_horiz_isIso ⟨(Category.id_comp _).trans (Category.comp_id _).symm⟩

Goal state after:
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
⊢ P.isLocal f → IsIso f

pp: case mpr
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
⊢ IsIso f → P.isLocal f

Tactic:
· intro hf
    obtain ⟨g, hg⟩ := (hf _ hX).2 (𝟙 X)
    exact ⟨g, hg, (hf _ hY).1 (by simp only [reassoc_of% hg, comp_id])⟩

Goal state after:
case mpr
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
⊢ IsIso f → P.isLocal f
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
φψ : F₁ ⟶ F₃
fac : φ ≫ ψ = φψ
inst✝ : IsLocallyInjective J ψ
⊢ IsLocallyInjective J φψ ↔ IsLocallyInjective J φ

Tactic:
by
  constructor
  · intro
    exact isLocallyInjective_of_isLocallyInjective_fac J fac
  · intro
    rw [← fac]
    infer_instance

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

Goal state before:
pp: case refine_3.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
j : Discrete (Fin n)
⊢ pullback.lift (α.app { as := j.as.succ } ≫ c₁.inj j.as) (c.ι.app { as := j.as.succ }) ⋯ ≫ pullback.fst c₂.inr i =
    α.app { as := j.as.succ } ≫ c₁.ι.app j

Tactic:
· simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, Cofan.inj]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝ : ∀ (i : ι), HasPullback (f i) v
s : (i : ι) → (j : ι') → PullbackCone (f i) (g j)
hs : (i : ι) → (j : ι') → IsLimit (s i j)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun p ↦ (s p.1 p.2).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
he₁ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.fst = (s (i, j).1 (i, j).2).fst ≫ a.inj (i, j).1
he₂ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.snd = (s (i, j).1 (i, j).2).snd ≫ b.inj (i, j).2
c : (i : ι) → Cofan fun j ↦ (s i j).pt :=
  fun i ↦ Cofan.mk (pullback (f i) v) fun j ↦ pullback.lift (s i j).fst ((s i j).snd ≫ b.inj j) ⋯
c' : Cofan fun i ↦ (c i).pt :=
  Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (pullback.fst (f i) v ≫ a.inj i) (pullback.snd (f i) v) ⋯
⊢ d ≅ Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1

Tactic:
refine Cofan.ext e <| fun p ↦ PullbackCone.IsLimit.hom_ext ht ?_ ?_
    · simp [c', c, he₁]
    · simp [c', c, he₂]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
P : Presieve X
r₀ : FamilyOfElements (R₀ ⋙ forget RingCat) P
m₀ : FamilyOfElements (M₀.presheaf ⋙ forget Ab) P
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
⊢ ((r₀.smul m₀).map (whiskerRight φ (forget Ab))).Compatible

Tactic:
intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ fac

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
P : Presieve X
r₀ : FamilyOfElements (R₀ ⋙ forget RingCat) P
m₀ : FamilyOfElements (M₀.presheaf ⋙ forget Ab) P
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : P f₁
h₂ : P f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom ((A ⋙ forget Ab).map g₁.op)) ((r₀.smul m₀).map (whiskerRight φ (forget Ab)) f₁ h₁) =
    (ConcreteCategory.hom ((A ⋙ forget Ab).map g₂.op)) ((r₀.smul m₀).map (whiskerRight φ (forget Ab)) f₂ h₂)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits

Goal state before:
pp: C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝³ : HasWeakSheafify J AddCommGrpCat
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
K : Type w
inst✝¹ : Category.{w', w} K
inst✝ : HasColimitsOfShape K (PresheafOfModules R.obj)
F : K ⥤ SheafOfModules R
⊢ HasColimit F

Tactic:
let e : F ≅ (F ⋙ forget R) ⋙ PresheafOfModules.sheafification (𝟙 R.obj) :=
      Functor.isoWhiskerLeft F
        (asIso (PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).counit).symm

Goal state after:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝³ : HasWeakSheafify J AddCommGrpCat
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
K : Type w
inst✝¹ : Category.{w', w} K
inst✝ : HasColimitsOfShape K (PresheafOfModules R.obj)
F : K ⥤ SheafOfModules R
e : F ≅ (F ⋙ forget R) ⋙ PresheafOfModules.sheafification (𝟙 R.obj) :=
  F.isoWhiskerLeft (asIso (PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).counit).symm
⊢ HasColimit F
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : GrothendieckTopology C
R : Sheaf J✝ RingCat
inst✝¹ : HasWeakSheafify J✝ AddCommGrpCat
inst✝ : J✝.WEqualsLocallyBijective AddCommGrpCat
I J : Type u
⊢ coprod.inr ≫ (freeSumIso I J).hom = freeMap Sum.inr

Tactic:
← dsimp% freeFunctor_map (↾(Sum.inr : J → I ⊕ J))

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : GrothendieckTopology C
R : Sheaf J✝ RingCat
inst✝¹ : HasWeakSheafify J✝ AddCommGrpCat
inst✝ : J✝.WEqualsLocallyBijective AddCommGrpCat
I J : Type u
⊢ coprod.inr ≫ (freeSumIso I J).hom = freeFunctor.map (↾Sum.inr)
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.Compatible
⊢ ∃ t, x.IsAmalgamation t

Tactic:
rw [Presieve.compatible_iff_sieveCompatible] at hx

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
⊢ ∃ t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S T : C
f : S ⟶ T
E : PreZeroHypercover T
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ Presieve.pullbackArrows f E.presieve₀ ≤ (pullback₂ f E).presieve₀

Tactic:
rintro W g ⟨-, -, ⟨i⟩⟩

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S T : C
f : S ⟶ T
E : PreZeroHypercover T
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i) f
Y✝ Y : C
i : E.I₀
⊢ (pullback₂ f E).presieve₀ (pullback.snd (E.f i) f)
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: case refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
⊢ Sieve.functorPushforward F (E.sieve₁' i₁ i₂) ≤
    (E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂)))

pp: case refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
⊢ (E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ≤
    Sieve.functorPushforward F (E.sieve₁' i₁ i₂)

Tactic:
· rw [PreOneHypercover.sieve₁'_eq_sieve₁]
    apply PreOneHypercover.functorPushforward_sieve₁_map_le

Goal state after:
case refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
⊢ (E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ≤
    Sieve.functorPushforward F (E.sieve₁' i₁ i₂)
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
⊢ IsSheafFor (F.op ⋙ P) (ofArrows Y f) ↔ IsSheafFor P (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i))

Tactic:
simp_rw [Presieve.isSheafFor_arrows_iff_pullbacks]

Goal state after:
C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
⊢ (∀ (x : (i : ι) → (F.op ⋙ P).obj (Opposite.op (Y i))),
      Arrows.PullbackCompatible (F.op ⋙ P) f x →
        ∃! t, ∀ (i : ι), (ConcreteCategory.hom ((F.op ⋙ P).map (f i).op)) t = x i) ↔
    ∀ (x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))),
      Arrows.PullbackCompatible P (fun i ↦ F.map (f i)) x →
        ∃! t, ∀ (i : ι), (ConcreteCategory.hom (P.map (F.map (f i)).op)) t = x i
Module: Mathlib.CategoryTheory.Sites.CoverLifting

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
h : F.IsCocontinuous J K
U : D
S : Sieve U
hS : S ∈ K U
X : C
f : X ⟶ G.obj U
hf : (Sieve.functorPullback F (Sieve.pullback (adj.counit.app U) S)).arrows f
⊢ (Sieve.functorPushforward G S).arrows f

Tactic:
refine ⟨F.obj X, F.map f ≫ adj.counit.app _, adj.unit.app _, hf, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
⊢ ∀ {Y Z : C} {f : Y ⟶ W},
    (∃ j h, f ≫ p₁ = h ≫ E.p₁ j ∧ f ≫ p₂ = h ≫ E.p₂ j) →
      ∀ (g : Z ⟶ Y), ∃ j h, (g ≫ f) ≫ p₁ = h ≫ E.p₁ j ∧ (g ≫ f) ≫ p₂ = h ≫ E.p₂ j

Tactic:
by
    rintro Z Z' g ⟨j, h, fac₁, fac₂⟩ φ
    exact ⟨j, φ ≫ h, by simpa using φ ≫= fac₁, by simpa using φ ≫= fac₂⟩

Goal state after: