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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ generate (Presieve.map F (Presieve.ofArrows Y f)) = ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)

Tactic:
Presieve.map_ofArrows

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ generate (Presieve.ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)) =
    ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
⊢ (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x →
    Presieve.FamilyOfElements.PullbackCompatible ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x)

Tactic:
intro t

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
t : (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x
⊢ Presieve.FamilyOfElements.PullbackCompatible ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
⊢ (functorPushforward (𝟭 C) R).arrows f → R.arrows f

Tactic:
intro hf
    obtain ⟨X, g, h, hg, rfl⟩ := hf
    exact R.downward_closed hg h

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
| ∀ (a : Presieve.FamilyOfElements P R),
    ((ConcreteCategory.hom (firstObjEqFamily P R).hom) ((firstObjEqFamily P R).toEquiv.symm a)).Compatible →
      ∃! x, (ConcreteCategory.hom (forkMap P R)) x = (firstObjEqFamily P R).toEquiv.symm a

Tactic:
a,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
a : Presieve.FamilyOfElements P R
| ((ConcreteCategory.hom (firstObjEqFamily P R).hom) ((firstObjEqFamily P R).toEquiv.symm a)).Compatible →
    ∃! x, (ConcreteCategory.hom (forkMap P R)) x = (firstObjEqFamily P R).toEquiv.symm a
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
⊢ ∀ (a : P.obj (op X)),
    x.IsAmalgamation a ↔ (ConcreteCategory.hom (forkMap P R)) a = (firstObjEqFamily P R).toEquiv.symm x

Tactic:
intro t

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
⊢ x.IsAmalgamation t ↔ (ConcreteCategory.hom (forkMap P R)) t = (firstObjEqFamily P R).toEquiv.symm x
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ Arrows.PullbackCompatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x) →
    (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x

Tactic:
intro t

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
t : Arrows.PullbackCompatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x)
⊢ (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x →
    Arrows.PullbackCompatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x)

Tactic:
intro t

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
t : (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x
⊢ Arrows.PullbackCompatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
⊢ ∀ (a : P.obj (op B)),
    (∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) a = x i) ↔
      (ConcreteCategory.hom (forkMap P X π)) a =
        (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm ((equivShrink ((j : I) → P.obj (op (X j)))) x)

Tactic:
intro t

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
⊢ (∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    (ConcreteCategory.hom (forkMap P X π)) t =
      (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm ((equivShrink ((j : I) → P.obj (op (X j)))) x)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P (generate R).arrows
hx : x.Compatible
⊢ ∀ (a : P.obj (op X)), (FamilyOfElements.restrict ⋯ x).IsAmalgamation a → x.IsAmalgamation a

Tactic:
intro t

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P (generate R).arrows
hx : x.Compatible
t : P.obj (op X)
⊢ (FamilyOfElements.restrict ⋯ x).IsAmalgamation t → x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P (generate R).arrows
hx : x.Compatible
t : P.obj (op X)
ht : (FamilyOfElements.restrict ⋯ x).IsAmalgamation t
⊢ x.IsAmalgamation t

Tactic:
simpa [hx] using isAmalgamation_sieveExtend _ _ ht

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P R
hx : x.Compatible
⊢ ∀ (a : P.obj (op X)), x.sieveExtend.IsAmalgamation a → x.IsAmalgamation a

Tactic:
intro t

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P R
hx : x.Compatible
t : P.obj (op X)
⊢ x.sieveExtend.IsAmalgamation t → x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
⊢ ∀ (y : P.obj (op X)), (fun t ↦ x.IsAmalgamation t) y → y = x (𝟙 X) ⋯

Tactic:
intro t

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
t : P.obj (op X)
⊢ (fun t ↦ x.IsAmalgamation t) t → t = x (𝟙 X) ⋯
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
e : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f) ≃
  Subtype (Arrows.Compatible P fun i ↦ (Over.map p).map (f i)) :=
  { toFun := fun s ↦ ⟨fun i ↦ ↑s i, ⋯⟩, invFun := fun s ↦ ⟨fun i ↦ ↑s i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ IsSheafFor ((Over.map p).op ⋙ P) (ofArrows Y f) ↔
    IsSheafFor P (ofArrows (fun i ↦ (Over.map p).obj (Y i)) fun i ↦ (Over.map p).map (f i))

Tactic:
simp only [isSheafFor_ofArrows_iff_bijective_toCompabible,
    ← e.bijective.of_comp_iff']

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
e : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f) ≃
  Subtype (Arrows.Compatible P fun i ↦ (Over.map p).map (f i)) :=
  { toFun := fun s ↦ ⟨fun i ↦ ↑s i, ⋯⟩, invFun := fun s ↦ ⟨fun i ↦ ↑s i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ Function.Bijective (⇑e ∘ Arrows.toCompatible ((Over.map p).op ⋙ P) f) ↔
    Function.Bijective (Arrows.toCompatible P fun i ↦ (Over.map p).map (f i))
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
i : C
x : F.obj i
hx : x ∈ G.obj i
hp : ∀ (k : C), Function.Surjective ⇑(ConcreteCategory.hom (p.app k))
⊢ x ∈ ((G.preimage p).image p).obj i

Tactic:
obtain ⟨y, rfl⟩ := hp _ x

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
i : C
hp : ∀ (k : C), Function.Surjective ⇑(ConcreteCategory.hom (p.app k))
y : F'.obj i
hx : (ConcreteCategory.hom (p.app i)) y ∈ G.obj i
⊢ (ConcreteCategory.hom (p.app i)) y ∈ ((G.preimage p).image p).obj i
Module: Mathlib.CategoryTheory.Sites.Sheafification

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ toSheafify J P ≫ sheafifyLift J η hQ = η

Tactic:
by
  rw [toSheafify, sheafifyLift, Adjunction.homEquiv_counit]
  change _ ≫ (sheafToPresheaf J D).map _ ≫ _ = _
  simp only [Adjunction.unit_naturality_assoc]
  change _ ≫ (sheafificationAdjunction J D).unit.app ((sheafToPresheaf J D).obj ⟨Q, hQ⟩) ≫ _ = _
  change _ ≫ _ ≫ (sheafToPresheaf J D).map _ = _
  rw [sheafificationAdjunction J D |>.right_triangle_components (Y := ⟨Q, hQ⟩)]
  simp

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

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

Tactic:
refine ⟨?_, ?_, ?_⟩

Goal state after:
case property.refine_1
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ofHom
        { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
          continuous_toFun := ⋯ } ≫
      (pullbackCone f g).fst =
    S.fst

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

case property.refine_3
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},
    m ≫ (pullbackCone f g).fst = S.fst →
      m ≫ (pullbackCone f g).snd = S.snd →
        m =
          ofHom
            { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
              continuous_toFun := ⋯ }
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : IsInducing ⇑(ConcreteCategory.hom f)
hg : IsInducing ⇑(ConcreteCategory.hom g)
⊢ induced (⇑(ConcreteCategory.hom prod.fst)) W.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str =
    induced (⇑(ConcreteCategory.hom prod.fst)) W.str ⊓
      induced (⇑(ConcreteCategory.hom prod.snd)) (induced (⇑(ConcreteCategory.hom g)) Z.str)

Tactic:
← hg.eq_induced

Goal state after:
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : IsInducing ⇑(ConcreteCategory.hom f)
hg : IsInducing ⇑(ConcreteCategory.hom g)
⊢ induced (⇑(ConcreteCategory.hom prod.fst)) W.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str =
    induced (⇑(ConcreteCategory.hom prod.fst)) W.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ IsEmbedding ⇑(ConcreteCategory.hom (pullback.snd f g))

Tactic:
convert!
    (homeoOfIso (asIso (pullback.snd (𝟙 S) g))).isEmbedding.comp
      (pullback_map_isEmbedding (i₂ := 𝟙 Y) f g (𝟙 S) g H (homeoOfIso (Iso.refl _)).isEmbedding
        (𝟙 _) rfl (by simp))
  simp [homeoOfIso, ← coe_comp]

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
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝⁴ : ∀ (i j : J) (X : C) (f : X ⟶ F.obj j) (g : i ⟶ j), PreservesLimit (cospan f (F.map g)) G
inst✝³ : ∀ (i : J) (X : C) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) G
inst✝² : ReflectsLimitsOfShape WalkingCospan G
inst✝¹ : PreservesColimitsOfShape J G
inst✝ : ReflectsColimitsOfShape J G
H : IsVanKampenColimit (G.mapCocone c)
⊢ IsVanKampenColimit c

Tactic:
intro F' c' α f h hα
  refine (Iff.trans ?_ (H (G.mapCocone c') (whiskerRight α G) (G.map f)
      (by ext j; simpa using! G.congr_map (NatTrans.congr_app h j))
      (hα.whiskerRight G))).trans (forall_congr' fun j => ?_)
  · exact ⟨fun h => ⟨isColimitOfPreserves G h.some⟩, fun h => ⟨isColimitOfReflects G h.some⟩⟩
  · exact IsPullback.map_iff G (NatTrans.congr_app h.symm j)

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mpr
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
H : IsPushout f g h i
⊢ IsVanKampenColimit (PushoutCocone.mk h i ⋯) → H.IsVanKampen

Tactic:
· introv H W' hf hg hh hi w
    refine
      Iff.trans ?_ ((H w.cocone ⟨by rintro (_ | _ | _); exacts [αW, αX, αY], ?_⟩ αZ ?_ ?_).trans ?_)
    rotate_left
    · rintro i _ (_ | _ | _)
      · dsimp; simp only [Functor.map_id, Category.comp_id, Category.id_comp]
      exacts [hf.w, hg.w]
    · ext (_ | _ | _)
      · simp [hh.w, hf.w_assoc]
      exacts [hh.w.symm, hi.w.symm]
    · rintro i _ (_ | _ | _)
      · dsimp; simp_rw [Functor.map_id]
        exact IsPullback.of_horiz_isIso ⟨by rw [Category.comp_id, Category.id_comp]⟩
      exacts [hf, hg]
    · constructor
      · intro h; exact ⟨h WalkingCospan.left, h WalkingCospan.right⟩
      · rintro ⟨h₁, h₂⟩ (_ | _ | _)
        · dsimp; rw [PushoutCocone.condition_zero]; exact hf.paste_horiz h₁
        exacts [h₁, h₂]
    · exact ⟨fun h => h.2, fun h => ⟨w, h⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_2.h₁
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ (BinaryCofan.mk (c.inr ≫ fE) iY).inl ≫ m =
    (BinaryCofan.mk (c.inr ≫ fE) iY).inl ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl

pp: case mp.refine_2.h₂
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ m =
    (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl

Tactic:
· dsimp
        rw [Category.assoc, e₂, eq_comm]; exact h.fac _ ⟨WalkingPair.left⟩

Goal state after:
case mp.refine_2.h₂
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ m =
    (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
c : Cofan fun x ↦ pullback f (π x) := Cofan.mk Y fun x ↦ pullback.fst f (π x)
hau : IsUniversalColimit (Cofan.mk X π)
⊢ ∀ (i : α),
    c.inj i ≫ (Iso.refl c.pt).hom ≫ (PullbackCone.mk (𝟙 Y) f ⋯).snd =
      PullbackCone.snd (limit.cone (cospan f (π i))) ≫ (Cofan.mk X π).inj i

Tactic:
by simp [pullback.condition, c]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F G : Sheaf J A
f : F ⟶ G
inst✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : J.HasSheafCompose (forget A)
⊢ IsLocallyInjective f ∧ IsLocallySurjective f ↔ IsIso f

Tactic:
by
  constructor
  · rintro ⟨_, _⟩
    rw [← isIso_iff_of_reflects_iso f (sheafCompose J (forget A)),
      ← isLocallyBijective_iff_isIso']
    constructor <;> infer_instance
  · intro
    constructor <;> infer_instance

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

Goal state before:
pp: case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
⊢ ∀ (t : Cofan fun k ↦ if k = i then X i else ⊥_ C) (j : ι),
    (Cofan.mk (X i) fun k ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫ eqToHom ⋯ ≫ t.inj i =
      t.inj j

Tactic:
intro t

Goal state after:
case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
t : Cofan fun k ↦ if k = i then X i else ⊥_ C
⊢ ∀ (j : ι),
    (Cofan.mk (X i) fun k ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫ eqToHom ⋯ ≫ t.inj i =
      t.inj j
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2.refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
⊢ ∀ (t : Cofan fun k ↦ if k = i then X i else ⊥_ C)
    (m : (Cofan.mk (X i) fun k ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).pt ⟶ t.pt),
    (∀ (j : ι),
        (Cofan.mk (X i) fun k ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫ m = t.inj j) →
      m = eqToHom ⋯ ≫ t.inj i

Tactic:
intro t

Goal state after:
case refine_2.refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
t : Cofan fun k ↦ if k = i then X i else ⊥_ C
⊢ ∀ (m : (Cofan.mk (X i) fun k ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).pt ⟶ t.pt),
    (∀ (j : ι),
        (Cofan.mk (X i) fun k ↦ if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).inj j ≫ m = t.inj j) →
      m = eqToHom ⋯ ≫ t.inj i
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasProjectiveDimensionLT X n
⊢ HasProjectiveDimensionLT X m

Tactic:
let := HasExt.standard C
  rw [hasProjectiveDimensionLT_iff]
  intro i hi Y e
  exact e.eq_zero_of_hasProjectiveDimensionLT n (by lia)

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
⊢ (∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P) → J₁ = J₂

Tactic:
intro h
    apply le_antisymm
    · apply le_topology_of_closedSieves_isSheaf
      rw [h]
      apply classifier_isSheaf
    · apply le_topology_of_closedSieves_isSheaf
      rw [← h]
      apply classifier_isSheaf

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C D : Type u₁
inst✝¹⁰ : SmallCategory C
inst✝⁹ : SmallCategory D
E : Type u₂
inst✝⁸ : Category.{u₁, u₂} E
FE : E → E → Type u_1
CE : E → Type u₁
inst✝⁷ : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)
inst✝⁶ : ConcreteCategory E FE
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
F : C ⥤ D
inst✝ : RepresentablyFlat F
⊢ PreservesFiniteLimits F.op.lan

Tactic:
by
  apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{u₁}
  intro J _ _
  apply preservesLimitsOfShape_of_evaluation (F.op.lan : (Cᵒᵖ ⥤ E) ⥤ Dᵒᵖ ⥤ E) J
  intro K
  have : IsFiltered (CostructuredArrow F.op K) :=
    IsFiltered.of_equivalence (structuredArrowOpEquivalence F (unop K))
  exact preservesLimitsOfShape_of_natIso (lanEvaluationIsoColim _ _ _).symm

Goal state after: