mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
inst✝ : Epi f
X : Cᵒᵖ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.app X))

Tactic:
← ModuleCat.epi_iff_surjective

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
inst✝ : Epi f
X : Cᵒᵖ
⊢ Epi (f.app X)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M N : PresheafOfModules R
f₁ f₂ : M ⟶ N
h : ∀ (G : PresheafOfModules R), freeYoneda R G → ∀ (h : G ⟶ M), h ≫ f₁ = h ≫ f₂
⊢ f₁ = f₂

Tactic:
ext ⟨X⟩ m

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M N : PresheafOfModules R
f₁ f₂ : M ⟶ N
h : ∀ (G : PresheafOfModules R), freeYoneda R G → ∀ (h : G ⟶ M), h ≫ f₁ = h ≫ f₂
X : C
m : ↑(M.obj (Opposite.op X))
⊢ (ModuleCat.Hom.hom (f₁.app (Opposite.op X))) m = (ModuleCat.Hom.hom (f₂.app (Opposite.op X))) m
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
hf : S.arrows f
⊢ J.Covers S f

Tactic:
rw [Covers, (Sieve.mem_iff_pullback_eq_top f).1 hf]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
hf : S.arrows f
⊢ ⊤ ∈ J Y
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case refine_2.mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W Y : C
h : W ⟶ Z
hh : Presieve.singleton f h
⊢ Presieve.singleton (f ≫ g) (h ≫ g)

Tactic:
cases hh

Goal state after:
case refine_2.mp.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
Y : C
⊢ Presieve.singleton (f ≫ g) (f ≫ g)
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X : C
R : Presieve X
⊢ R ∈ (trivial C).coverings X → R ∈ K.coverings X

Tactic:
rintro ⟨Y, f, hf, rfl⟩
    exact K.has_isos f

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ (ofArrows (fun x ↦ Y) fun x ↦ f) = singleton f

Tactic:
rw [ofArrows_of_unique]

Goal state after:
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
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

Tactic:
ext ij

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)
ij : I × I
⊢ (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij))
      ((ConcreteCategory.hom (firstMap P X π)) x) =
    (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij))
      ((ConcreteCategory.hom (secondMap P X π)) x)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case refine_1
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 : FirstObj P X
t :
  Arrows.PullbackCompatible P π
    ((equivShrink ((i : I) → P.obj (op (X i)))).symm
      ((ConcreteCategory.hom (Types.Small.productIso fun i ↦ P.obj (op (X i))).hom) x))
⊢ (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x

Tactic:
ext ij

Goal state after:
case refine_1
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 : FirstObj P X
t :
  Arrows.PullbackCompatible P π
    ((equivShrink ((i : I) → P.obj (op (X i)))).symm
      ((ConcreteCategory.hom (Types.Small.productIso fun i ↦ P.obj (op (X i))).hom) x))
ij : I × I
⊢ (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij))
      ((ConcreteCategory.hom (firstMap P X π)) x) =
    (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij))
      ((ConcreteCategory.hom (secondMap P X π)) x)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
⊢ (∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂) ∧
      (x.Compatible → ∃ t, x.IsAmalgamation t) →
    x.Compatible → ∃! t, x.IsAmalgamation t

Tactic:
intro z hx

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
z :
  (∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂) ∧
    (x.Compatible → ∃ t, x.IsAmalgamation t)
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : ToType (P.obj (op X))
⊢ (ConcreteCategory.hom ((J.toPlus P).app (op X))) x = mk (Meq.mk S x)

Tactic:
dsimp [mk, toPlus]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : ToType (P.obj (op X))
⊢ (ConcreteCategory.hom (⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P X) (op ⊤))) x =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op S))) ((Meq.equiv P S).symm (Meq.mk S x))
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
⊢ IsSheafFor P R

Tactic:
by
  rw [← isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
  constructor
  · intro x t₁ t₂ ht₁ ht₂
    exact
      hS.isSeparatedFor _ _ _ (isAmalgamation_restrict h x t₁ ht₁)
        (isAmalgamation_restrict h x t₂ ht₂)
  · intro x hx
    use hS.amalgamate _ (hx.restrict h)
    intro W j hj
    apply (trans hj).ext
    intro Y f hf
    rw [← comp_apply, ← Functor.map_comp, ← op_comp, hS.valid_glue (hx.restrict h) _ hf,
      FamilyOfElements.restrict, ← hx (𝟙 _) f (h _ _ hf) _ (id_comp _)]
    simp

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

Goal state before:
pp: case e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
⊢ Multiequalizer.ι ((unop S).index P) I ≫ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P I.Y) (op ⊤) =
    colimit.ι (J.diagram P (unop X)) S ≫ (J.plusObj P).map (Cover.Arrow.map I e.op.unop).f.op

Tactic:
let ee : (J.pullback (I.map e).f).obj S.unop ⟶ ⊤ := homOfLE (OrderTop.le_top _)

Goal state after:
case e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
⊢ Multiequalizer.ι ((unop S).index P) I ≫ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P I.Y) (op ⊤) =
    colimit.ι (J.diagram P (unop X)) S ≫ (J.plusObj P).map (Cover.Arrow.map I e.op.unop).f.op
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: case e_a.e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
⊢ (Multiequalizer.ι ((unop S).index P) I ≫ ⊤.toMultiequalizer P) ≫ (J.diagram P I.Y).map ee.op =
    Multiequalizer.lift ((unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).index P)
      ((J.diagram P (unop X)).obj S) (fun I_1 ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I_1)) ⋯

Tactic:
refine Multiequalizer.hom_ext _ _ _ (fun II => ?_)

Goal state after:
case e_a.e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
II : (unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).shape.L
⊢ ((Multiequalizer.ι ((unop S).index P) I ≫ ⊤.toMultiequalizer P) ≫ (J.diagram P I.Y).map ee.op) ≫
      Multiequalizer.ι ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P) II =
    Multiequalizer.lift ((unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).index P)
        ((J.diagram P (unop X)).obj S) (fun I_1 ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I_1)) ⋯ ≫
      Multiequalizer.ι ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P) II
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
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
⊢ Over.Hom.left g₂ ≫ (Y i₂).hom = (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)).hom

Tactic:
by
            have := Over.w (f i₂)
            dsimp at this ⊢
            rw [reassoc_of% h, this]

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁵ : Category.{v₂, u₂} A
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F✝ G H : A ⥤ B
η : F✝ ⟶ G
γ : G ⟶ H
inst✝³ : J.HasSheafCompose F✝
inst✝² : J.HasSheafCompose G
inst✝¹ : J.HasSheafCompose H
F : A ⥤ B
inst✝ : ∀ (X : C) (S : J.Cover X) (P : Cᵒᵖ ⥤ A), PreservesLimit (S.index P).multicospan F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
X : C
S : J.Cover X
h : IsLimit ((Cone.postcompose (GrothendieckTopology.Cover.multicospanComp F P S).hom).obj (S.multifork (P ⋙ F)))
⊢ Nonempty (IsLimit (S.multifork (P ⋙ F)))

Tactic:
exact ⟨Limits.IsLimit.postcomposeHomEquiv (S.multicospanComp F P) _ h⟩

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 Y : C
f : X ⟶ Y
⊢ IsSheafFor P (singleton f) ↔
    ∀ (x : P.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (P.map p₁.op)) x = (ConcreteCategory.hom (P.map p₂.op)) x) →
        ∃! y, (ConcreteCategory.hom (P.map f.op)) y = x

Tactic:
by
  rw [IsSheafFor, Equiv.forall_congr_left (Presieve.FamilyOfElements.singletonEquiv P f)]
  simp_rw [FamilyOfElements.compatible_singleton_iff,
    FamilyOfElements.isAmalgamation_singleton_iff, FamilyOfElements.singletonEquiv_symm_apply_self]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S Sx : J.Cover X
x : Meq P Sx
Sy : J.Cover X
y : Meq P Sy
h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)
B : J.Cover X := S.bind W
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
he2 : (↑S).arrows e2
he1 : ((fun Y f hf ↦ ↑(W { Y := Y, f := f, hf := hf })) Z e2 he2).arrows e1
hee : e1 ≫ e2 = f
⊢ (↑Sx).arrows f

Tactic:
rw [← hee]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S Sx : J.Cover X
x : Meq P Sx
Sy : J.Cover X
y : Meq P Sy
h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)
B : J.Cover X := S.bind W
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
he2 : (↑S).arrows e2
he1 : ((fun Y f hf ↦ ↑(W { Y := Y, f := f, hf := hf })) Z e2 he2).arrows e1
hee : e1 ≫ e2 = f
⊢ (↑Sx).arrows (e1 ≫ e2)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S Sx : J.Cover X
x : Meq P Sx
Sy : J.Cover X
y : Meq P Sy
h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)
B : J.Cover X := S.bind W
ex : B ⟶ Sx := homOfLE ⋯
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
he2 : (↑S).arrows e2
he1 : ((fun Y f hf ↦ ↑(W { Y := Y, f := f, hf := hf })) Z e2 he2).arrows e1
hee : e1 ≫ e2 = f
⊢ (↑Sy).arrows f

Tactic:
rw [← hee]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S Sx : J.Cover X
x : Meq P Sx
Sy : J.Cover X
y : Meq P Sy
h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)
B : J.Cover X := S.bind W
ex : B ⟶ Sx := homOfLE ⋯
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
he2 : (↑S).arrows e2
he1 : ((fun Y f hf ↦ ↑(W { Y := Y, f := f, hf := hf })) Z e2 he2).arrows e1
hee : e1 ≫ e2 = f
⊢ (↑Sy).arrows (e1 ≫ e2)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
⊢ Function.Injective ⇑(ConcreteCategory.hom ((J.toPlus P).app (op X)))

Tactic:
by
  intro x y h
  simp only [toPlus_eq_mk] at h
  rw [eq_mk_iff_exists] at h
  obtain ⟨W, h1, h2, hh⟩ := h
  apply hsep X W
  intro I
  apply_fun fun e => e I at hh
  exact hh

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ IsIso (J.toSheafify P)

Tactic:
by
  dsimp [toSheafify]
  have := isIso_toPlus_of_isSheaf J P hP
  change (IsIso (toPlus J P ≫ (J.plusFunctor D).map (toPlus J P)))
  infer_instance

Goal state after:
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 β)
⊢ Continuous fun s ↦ (ConcreteCategory.hom (S.ι.app { as := s.fst })) s.snd

Tactic:
by continuity

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

Goal state before:
pp: case e'_2.mpr
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
⊢ (∀ (j : K),
      IsPullback (c'.ι.app (e.inverse.obj j)) (α.app (e.inverse.obj j) ≫ F.map (e.counit.app j)) f (c.ι.app j)) →
    ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))

Tactic:
intro H j
      have : α.app j
          = F'.map (e.unit.app _) ≫ α.app _ ≫ F.map (e.counit.app (e.functor.obj j)) := by
        simp [← Functor.map_comp]
      rw [← Category.id_comp f, this]
      refine IsPullback.paste_vert ?_ (H (e.functor.obj j))
      exact IsPullback.of_vert_isIso ⟨by simp⟩

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

Goal state before:
pp: case mp.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
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
sq_h : CommSq h' αX αZ h
sq_i : CommSq i' αY αZ i
inst✝ : HasPullback αX f
W' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
αW : W' ⟶ W
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
H'' : IsPushout f' g' h' i'
⊢ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i

Tactic:
rwa [← H' f' g' h' i' αW αX αY αZ hf hg sq_h sq_i H''.toCommSq]

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

Goal state before:
pp: case mpr.mpr.h₁
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
H' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
sq_h : CommSq h' αX αZ h
sq_i : CommSq i' αY αZ i
cs : CommSq f' g' h' i'
this : HasPullback αX f := ⋯
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
W'' : C
f'' : W'' ⟶ X'
g'' : W'' ⟶ Y'
αW' : W'' ⟶ W
hf' : IsPullback f'' αW' αX f
hg' : IsPullback g'' αW' αY g
hP : IsPushout f'' g'' h' i'
⊢ (g'' ≫ (Iso.refl Y').hom) ≫ αY = ((IsPullback.isoIsPullback X' W hf' hf).hom ≫ g') ≫ αY

Tactic:
simp [hg.w, hg'.w]

Goal state after: