mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case algebraMap
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
g : N →ₗ[R] N'
r✝ : R
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (liftAlternating fun i ↦ g.compAlternatingMap (f i)) ((algebraMap R (CliffordAlgebra 0)) r✝) =
    g ((liftAlternating f) ((algebraMap R (CliffordAlgebra 0)) r✝))

Tactic:
liftAlternating_algebraMap,

Goal state after:
case algebraMap
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
g : N →ₗ[R] N'
r✝ : R
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ r✝ • (g.compAlternatingMap (f 0)) 0 = g ((liftAlternating f) ((algebraMap R (CliffordAlgebra 0)) r✝))
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case algebraMap
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
g : N →ₗ[R] N'
r✝ : R
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ r✝ • (g.compAlternatingMap (f 0)) 0 = g ((liftAlternating f) ((algebraMap R (CliffordAlgebra 0)) r✝))

Tactic:
liftAlternating_algebraMap,

Goal state after:
case algebraMap
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
g : N →ₗ[R] N'
r✝ : R
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ r✝ • (g.compAlternatingMap (f 0)) 0 = g (r✝ • (f 0) 0)
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r✝ : R
⊢ (liftAlternating (ιMulti R)) ((algebraMap R (CliffordAlgebra 0)) r✝) = (algebraMap R (CliffordAlgebra 0)) r✝

Tactic:
liftAlternating_algebraMap,

Goal state after:
case algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r✝ : R
⊢ r✝ • (ιMulti R 0) 0 = (algebraMap R (CliffordAlgebra 0)) r✝
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
d : ℕ
Y : C
e : Ext Y X d
k : ℕ
⊢ d = n + k → e = 0

Tactic:
hd

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
d : ℕ
Y : C
e : Ext Y X d
k : ℕ
hd : d = n + k
⊢ e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case succ
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext Y X d), d = n + k → e = 0
d : ℕ
Y : C
e : Ext Y X d
hd : d = n + (k + 1)
⊢ e = 0

Tactic:
let ⟨p⟩ := EnoughProjectives.presentation Y

Goal state after:
case succ
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext Y X d), d = n + k → e = 0
d : ℕ
Y : C
e : Ext Y X d
hd : d = n + (k + 1)
p : ProjectivePresentation Y
⊢ e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : injectiveDimension X < ↑n
⊢ HasInjectiveDimensionLT X n

Tactic:
have : injectiveDimension X ∈ _ := csInf_mem ⟨⊤, by simp⟩
    simp only [Set.mem_ofPred_eq] at this
    exact this _ h

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
I B : C
t : IsInitial I
inst✝ : MonoidalClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ t.to B = h ≫ t.to B
⊢ g = h

Tactic:
have := strict_initial t g
    have := strict_initial t h
    exact eq_of_inv_eq_inv (t.hom_ext _ _)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
⊢ IsSiftedOrEmpty C

Tactic:
by
    constructor
    rintro ⟨c₁, c₂⟩
    have : _root_.Nonempty <| StructuredArrow (c₁, c₂) (diag C) :=
      ⟨.mk ((coprod.inl : c₁ ⟶ c₁ ⨿ c₂), (coprod.inr : c₂ ⟶ c₁ ⨿ c₂))⟩
    apply isConnected_of_zigzag
    rintro ⟨_, c, f⟩ ⟨_, c', g⟩
    dsimp only [const_obj_obj, diag_obj] at f g
    use [.mk ((coprod.inl : c₁ ⟶ c₁ ⨿ c₂), (coprod.inr : c₂ ⟶ c₁ ⨿ c₂)), .mk (g.fst, g.snd)]
    simp only [colimit.cocone_x, diag_obj, Prod.mk.eta, List.isChain_cons_cons,
      List.isChain_singleton, and_true, ne_eq, reduceCtorEq, not_false_eq_true,
      List.getLast_cons, List.cons_ne_self, List.getLast_singleton]
    exact ⟨⟨Zag.of_inv <| StructuredArrow.homMk <| coprod.desc f.fst f.snd,
      Zag.of_hom <| StructuredArrow.homMk <| coprod.desc g.fst g.snd⟩, rfl⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) colim
⊢ IsSiftedOrEmpty C

Tactic:
by
  apply final_of_colimit_comp_coyoneda_iso_pUnit
  rintro ⟨c₁, c₂⟩
  calc colimit <| diag C ⋙ coyoneda.obj (op (c₁, c₂))
    _ ≅ colimit <| _ ⋙ (coyoneda.obj _) ⊠ (coyoneda.obj _) :=
      HasColimit.isoOfNatIso <| isoWhiskerLeft _ <| .refl _
    _ ≅ colimit (_ ⊗ _) := HasColimit.isoOfNatIso <| .refl _
    _ ≅ (colimit _) ⊗ (colimit _) := CartesianMonoidalCategory.prodComparisonIso colim _ _
    _ ≅ PUnit ⊗ PUnit :=
      (Coyoneda.colimitCoyonedaIso _) ⊗ᵢ (Coyoneda.colimitCoyonedaIso _)
    _ ≅ PUnit := λ_ _

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
h₁ : IsSifted (AsSmall C)
F : C ⥤ D
inst✝ : F.Final
⊢ IsSifted (AsSmall D)

Tactic:
exact of_final_functor_from_sifted' <|
    AsSmall.equiv.{_, _, max u₁ v₁}.inverse ⋙ F ⋙ AsSmall.equiv.{_, _, max u v}.functor

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mpr.right
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
⊢ ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t

Tactic:
· intro _ c _ _
      exact ⟨c, 𝟙 _, rfl⟩

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

Goal state before:
pp: C✝ : Type u
inst✝¹ : Category.{v, u} C✝
R✝ : C✝ᵒᵖ ⥤ RingCat
C : Type u
inst✝ : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
⊢ IsColimit M.freeYonedaCoproductsCokernelCofork

Tactic:
let S := ShortComplex.mk _ _ M.toFreeYonedaCoproduct_fromFreeYonedaCoproduct

Goal state after:
C✝ : Type u
inst✝¹ : Category.{v, u} C✝
R✝ : C✝ᵒᵖ ⥤ RingCat
C : Type u
inst✝ : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
S : ShortComplex (PresheafOfModules R) :=
  { X₁ := (kernel M.fromFreeYonedaCoproduct).freeYonedaCoproduct, X₂ := M.freeYonedaCoproduct, X₃ := M,
    f := M.toFreeYonedaCoproduct, g := M.fromFreeYonedaCoproduct, zero := ⋯ }
⊢ IsColimit M.freeYonedaCoproductsCokernelCofork
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 R : Sieve X
hS : J.Covers S f
hR : J.Covers R f
⊢ J.Covers (S ⊓ R) f

Tactic:
simpa [covers_iff] using And.intro hS hR

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
H₁ : S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
R : Sieve X
⊢ (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | ∀ {Y_1 : C} (f : Y_1 ⟶ Y), ∃ Z g, S.arrows (g ≫ f)}) →
    R ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}

Tactic:
H₂

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
H₁ : S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
R : Sieve X
H₂ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | ∀ {Y_1 : C} (f : Y_1 ⟶ Y), ∃ Z g, S.arrows (g ≫ f)}
⊢ R ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
J : GrothendieckTopology C
h : IsSheaf J P
⊢ IsSheaf J (P ⋙ uliftFunctor.{w', w})

Tactic:
by
  rwa [isSheaf_comp_uliftFunctor_iff]

Goal state after:
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
s : Presieve X
⊢ (generate (Presieve.map F s)).arrows = Presieve.functorPushforward F s

Tactic:
refine funext fun Z ↦ funext fun u ↦ propext ⟨?_, ?_⟩
  · rintro ⟨_, _, _, ⟨hu⟩, rfl⟩; exact ⟨_, _, _, hu, rfl⟩
  · rintro ⟨_, _, _, hu, rfl⟩; exact ⟨_, _, _, ⟨hu⟩, rfl⟩

Goal state after:
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
S : Sieve X
x : FirstObj P S.arrows
⊢ (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x →
    Presieve.FamilyOfElements.SieveCompatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x)

Tactic:
intro t Y Z f g hf

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ (ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x (g ≫ f) ⋯ =
    (ConcreteCategory.hom (P.map g.op)) ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x f hf)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
S : Sieve Y
⊢ pushforward f S = ⊥ ↔ S = ⊥

Tactic:
simp [(galoisConnection f).l_eq_bot]

Goal state after:
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 Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
U V : Cᵒᵖ
f : U ⟶ V
x✝ : ↑{f | S.arrows (shrinkYonedaObjObjEquiv f)}
⊢ ↑((hom
            ((↾fun x ↦ ⟨(hom ((shrinkYoneda.{v₁, v₁, u₁}.obj X).map f)) ↑x, ⋯⟩) ≫
              (shrinkYonedaObjObjEquiv.subtypeEquiv ⋯).toIso.hom)).toFun
        x✝) =
    ↑((hom ((shrinkYonedaObjObjEquiv.subtypeEquiv ⋯).toIso.hom ≫ ↾fun g ↦ ⟨f.unop ≫ ↑g, ⋯⟩)).toFun x✝)

Tactic:
simp [shrinkYonedaObjObjEquiv_obj_map]

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

Goal state before:
pp: case mpr.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
x : unop (op X)
⊢ Presieve.FamilyOfElements.Compatible fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x

pp: case mpr.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
⊢ (fun t ↦ z.IsAmalgamation t) (↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯)

pp: case mpr.refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
⊢ ∀ (y : (P ⋙ coyoneda.obj (op X)).obj (op Y)),
    (fun t ↦ z.IsAmalgamation t) y → y = ↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯

Tactic:
· intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ h
      exact (ConcreteCategory.congr_hom (hz g₁ g₂ hf₁ hf₂ h)) x

Goal state after:
case mpr.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
⊢ (fun t ↦ z.IsAmalgamation t) (↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯)

case mpr.refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
⊢ ∀ (y : (P ⋙ coyoneda.obj (op X)).obj (op Y)),
    (fun t ↦ z.IsAmalgamation t) y → y = ↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsLimit (S.multifork P)
⊢ IsIso (S.toMultiequalizer P)

Tactic:
let e : P.obj (op X) ≅ multiequalizer (S.index P) :=
      h.conePointUniqueUpToIso (limit.isLimit _)

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsLimit (S.multifork P)
e : P.obj (op X) ≅ multiequalizer (S.index P) := h.conePointUniqueUpToIso (limit.isLimit (S.index P).multicospan)
⊢ IsIso (S.toMultiequalizer P)
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G : Subfunctor F
f : F ⟶ F'
⊢ ∀ {U V : C} (i : U ⟶ V),
    ⇑(ConcreteCategory.hom (f.app U)) '' G.obj U ⊆
      ⇑(ConcreteCategory.hom (F'.map i)) ⁻¹' ⇑(ConcreteCategory.hom (f.app V)) '' G.obj V

Tactic:
rintro Δ Δ' φ _ ⟨x, hx, rfl⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G : Subfunctor F
f : F ⟶ F'
Δ Δ' : C
φ : Δ ⟶ Δ'
x : F.obj Δ
hx : x ∈ G.obj Δ
⊢ (ConcreteCategory.hom (f.app Δ)) x ∈
    ⇑(ConcreteCategory.hom (F'.map φ)) ⁻¹' ⇑(ConcreteCategory.hom (f.app Δ')) '' G.obj Δ'
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
⊢ homOfLe ⋯ ≫ G.sheafifyLift f h = f

Tactic:
ext U s
  apply (h _ ((Subfunctor.homOfLe (G.le_sheafify J)).app U s).prop).isSeparatedFor.ext
  intro V i hi
  have := elementwise_of% f.naturality
  exact (Presieve.IsSheafFor.valid_glue (h _ ((homOfLe (_ : _ ≤ sheafify _ _)).app _ _).2)
    ((G.family_of_elements_compatible _).map _) _ _).trans (this _ _)

Goal state after:
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
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
k : K
i : W.shape.R
⊢ S.ι (W.shape.fst i) ≫ (E.π.app k).app (op (W.shape.fst i).Y) ≫ (W.index (F.obj k).obj).fst i =
    S.ι (W.shape.snd i) ≫ (E.π.app k).app (op (W.shape.snd i).Y) ≫ (W.index (F.obj k).obj).snd i

Tactic:
← (E.π.app k).naturality,

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
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
k : K
i : W.shape.R
⊢ S.ι (W.shape.fst i) ≫ (((Functor.const K).obj E.pt).obj k).map i.r.g₁.op ≫ (E.π.app k).app (op i.r.Z) =
    S.ι (W.shape.snd i) ≫ (E.π.app k).app (op (W.shape.snd i).Y) ≫ (W.index (F.obj k).obj).snd i
Module: Mathlib.CategoryTheory.Limits.ColimitLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) k ≫ colimitLimitToLimitColimit F ≫ limit.π (curry.obj F ⋙ colim) j =
    limit.π ((curry.obj (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k

Tactic:
by
  dsimp [colimitLimitToLimitColimit]
  simp

Goal state after:
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✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
i : W.Arrow
⊢ m ≫ (E.π.app k).app (op X) ≫ (F.obj k).obj.map i.f.op = (m ≫ (W.multifork E.pt).ι i) ≫ (E.π.app k).app (op i.Y)

Tactic:
← (E.π.app k).naturality,

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✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
i : W.Arrow
⊢ m ≫ (((Functor.const K).obj E.pt).obj k).map i.f.op ≫ (E.π.app k).app (op i.Y) =
    (m ≫ (W.multifork E.pt).ι i) ≫ (E.π.app k).app (op i.Y)
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
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
m : { pt := { obj := E.pt, property := ⋯ }, ι := { app := fun x ↦ { hom := E.ι.app x }, naturality := ⋯ } }.pt ⟶ S.pt
hm :
  ∀ (j : K),
    { pt := { obj := E.pt, property := ⋯ }, ι := { app := fun x ↦ { hom := E.ι.app x }, naturality := ⋯ } }.ι.app j ≫
        m =
      S.ι.app j
⊢ m = { hom := hE.desc ((sheafToPresheaf J D).mapCocone S) }

Tactic:
by
            ext1
            exact hE.uniq ((sheafToPresheaf J D).mapCocone S) m.hom fun j =>
              (ObjectProperty.ι _).congr_map (hm j)

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

Goal state before:
pp: case mpr
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
y : ↑Y
⊢ y ∈ {y | ∃ x, (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y} →
    y ∈ Set.range ⇑(ConcreteCategory.hom (pullback.snd f g))

Tactic:
rintro ⟨x, eq⟩
    use (TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨x, y⟩, eq⟩
    rw [pullbackIsoProdSubtype_inv_snd_apply]

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

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
z :
  ∀ (j : J),
    ∃ j_1 y,
      (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) j_1)) y =
        (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
⊢ ∃ a, (ConcreteCategory.hom (colimitLimitToLimitColimit F)) a = x

Tactic:
let k : J → K := fun j => (z j).choose

Goal state after:
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
z :
  ∀ (j : J),
    ∃ j_1 y,
      (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) j_1)) y =
        (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k : J → K := fun j ↦ ⋯.choose
⊢ ∃ a, (ConcreteCategory.hom (colimitLimitToLimitColimit F)) a = x
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
w :
  ∀ {j j' : J} (f : j ⟶ j'),
    ∃ k_1 f_1 g_1,
      (ConcreteCategory.hom (((curry.obj F).obj j').map f_1)) ((ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j'))) (y j')) =
        (ConcreteCategory.hom (((curry.obj F).obj j').map g_1)) ((ConcreteCategory.hom (F.map (f ×ₘ g j))) (y j))
kf : {j j' : J} → (j ⟶ j') → K := fun {j j'} f ↦ ⋯.choose
gf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f := fun {j j'} f ↦ ⋯.choose
hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f := fun {j j'} f ↦ ⋯.choose
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)

Tactic:
have q :
        ((curry.obj F).obj j').map (gf f) (F.map (𝟙 j' ×ₘ g j') (y j')) =
          ((curry.obj F).obj j').map (hf f) (F.map (f ×ₘ g j) (y j)) :=
        (w f).choose_spec.choose_spec.choose_spec

Goal state after:
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
w :
  ∀ {j j' : J} (f : j ⟶ j'),
    ∃ k_1 f_1 g_1,
      (ConcreteCategory.hom (((curry.obj F).obj j').map f_1)) ((ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j'))) (y j')) =
        (ConcreteCategory.hom (((curry.obj F).obj j').map g_1)) ((ConcreteCategory.hom (F.map (f ×ₘ g j))) (y j))
kf : {j j' : J} → (j ⟶ j') → K := fun {j j'} f ↦ ⋯.choose
gf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f := fun {j j'} f ↦ ⋯.choose
hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f := fun {j j'} f ↦ ⋯.choose
j j' : J
f : j ⟶ j'
q :
  (ConcreteCategory.hom (((curry.obj F).obj j').map (gf f))) ((ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j'))) (y j')) =
    (ConcreteCategory.hom (((curry.obj F).obj j').map (hf f))) ((ConcreteCategory.hom (F.map (f ×ₘ g j))) (y j))
⊢ (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)