mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
⊢ M →ₗ[R] ↥(⋀[R]^1 M)

Tactic:
have h (m : M) : (fun (_ : Fin 1) ↦ m) = update (fun _ ↦ 0) 0 m := by
      ext i
      fin_cases i
      rfl
    exact
      { toFun := fun m ↦ ιMulti _ _ (fun _ ↦ m)
        map_add' := fun m₁ m₂ ↦ by
          rw [h]; nth_rw 2 [h]; nth_rw 3 [h]
          simp only [Fin.isValue, AlternatingMap.map_update_add]
        map_smul' := fun r m ↦ by
          dsimp
          rw [h]; nth_rw 2 [h]
          simp only [Fin.isValue, AlternatingMap.map_update_smul] }

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : SymmetricCategory D
F G : C ⥤ D
⊢ (β_ F G).hom ≫ (β_ G F).hom = 𝟙 (F ⊗ G)

Tactic:
ext X; apply symmetry

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

Goal state before:
pp: case a.a
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| (D.obj j).π.app k ≫ (F.obj j).map fk

pp: case a.a
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| (F.map fj).app k'

pp: case a
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| s.π.app j

Tactic:
← (D.obj j).π.naturality

Goal state after:
case a.a
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| ((const K).obj (D.obj j).pt).map fk ≫ (D.obj j).π.app k'

case a.a
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| (F.map fj).app k'

case a
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| s.π.app j
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:
exact ⟨c, 𝟙 _, rfl⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
⊢ (freeAdjunction R).homEquiv F G = freeHomEquiv

Tactic:
simp [freeAdjunction, Adjunction.mkOfHomEquiv_homEquiv]

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

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ colimit.ι (F.flip.obj k) j ≫
      colimit.ι (F.flip ⋙ colim) k ≫
        (colimitUncurryIsoColimitCompColim F.flip).inv ≫
          (HasColimit.isoOfNatIso F.uncurryObjFlip).hom ≫
            (HasColimit.isoOfEquivalence (Prod.braiding K J)
                  (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj x.2).obj x.1)) ⋯)).hom ≫
              (colimitUncurryIsoColimitCompColim F).hom =
    colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j

Tactic:
(Mathlib.Tactic.Conv.convLHS
 "conv_lhs"
 []
 []
 "=>"
 (Tactic.Conv.convSeq
  (Tactic.Conv.convSeq1Indented
   [(choice
     (Mathlib.Tactic.Slice.convSlice___ "slice" (num "1") (group) (num "3"))
     (Mathlib.Tactic.Slice.slice "slice" (num "1") (num "3")))])))

Goal state after:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ (((colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k ≫ (colimitUncurryIsoColimitCompColim F.flip).inv) ≫
          (HasColimit.isoOfNatIso F.uncurryObjFlip).hom) ≫
        (HasColimit.isoOfEquivalence (Prod.braiding K J)
            (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj x.2).obj x.1)) ⋯)).hom) ≫
      (colimitUncurryIsoColimitCompColim F).hom =
    colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
k : K
j : J
⊢ colimit.ι (F.obj j) k ≫
      colimit.ι (F ⋙ colim) j ≫
        (((colimitUncurryIsoColimitCompColim F).inv ≫
              (HasColimit.isoOfEquivalence (Prod.braiding K J)
                  (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj x.2).obj x.1)) ⋯)).inv) ≫
            (HasColimit.isoOfNatIso F.uncurryObjFlip).inv) ≫
          (colimitUncurryIsoColimitCompColim F.flip).hom =
    colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k

Tactic:
(Mathlib.Tactic.Conv.convLHS
 "conv_lhs"
 []
 []
 "=>"
 (Tactic.Conv.convSeq
  (Tactic.Conv.convSeq1Indented
   [(choice
     (Mathlib.Tactic.Slice.convSlice___ "slice" (num "1") (group) (num "3"))
     (Mathlib.Tactic.Slice.slice "slice" (num "1") (num "3")))])))

Goal state after:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
k : K
j : J
⊢ (((colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j ≫ (colimitUncurryIsoColimitCompColim F).inv) ≫
          (HasColimit.isoOfEquivalence (Prod.braiding K J)
              (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj x.2).obj x.1)) ⋯)).inv) ≫
        (HasColimit.isoOfNatIso F.uncurryObjFlip).inv) ≫
      (colimitUncurryIsoColimitCompColim F.flip).hom =
    colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫
      colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k ≫
        ((colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).inv ≫
            (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).hom) ≫
          (colimitIsoColimitCurryCompColim G).hom =
    colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j

Tactic:
(Mathlib.Tactic.Conv.convLHS
 "conv_lhs"
 []
 []
 "=>"
 (Tactic.Conv.convSeq
  (Tactic.Conv.convSeq1Indented
   [(choice
     (Mathlib.Tactic.Slice.convSlice___ "slice" (num "1") (group) (num "3"))
     (Mathlib.Tactic.Slice.slice "slice" (num "1") (num "3")))])))

Goal state after:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ ((colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫
          colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k ≫
            (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).inv) ≫
        (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).hom) ≫
      (colimitIsoColimitCurryCompColim G).hom =
    colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ colimit.ι ((curry.obj G).obj j) k ≫
      colimit.ι (curry.obj G ⋙ colim) j ≫
        (colimitIsoColimitCurryCompColim G).inv ≫
          (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).inv ≫
            (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Tactic:
(Mathlib.Tactic.Conv.convLHS
 "conv_lhs"
 []
 []
 "=>"
 (Tactic.Conv.convSeq
  (Tactic.Conv.convSeq1Indented
   [(choice
     (Mathlib.Tactic.Slice.convSlice___ "slice" (num "1") (group) (num "3"))
     (Mathlib.Tactic.Slice.slice "slice" (num "1") (num "3")))])))

Goal state after:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ ((colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j ≫ (colimitIsoColimitCurryCompColim G).inv) ≫
        (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).inv) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ ((colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j ≫ (colimitIsoColimitCurryCompColim G).inv) ≫
        (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).inv) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Tactic:
rw [colimitIsoColimitCurryCompColim_ι_ι_inv, HasColimit.ι_isoOfEquivalence_inv]

Goal state after:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ (G.map ((Prod.braiding K J).counitInv.app (j, k)) ≫
        (Iso.refl (Prod.swap K J ⋙ G)).hom.app ((Prod.braiding K J).inverse.obj (j, k)) ≫
          colimit.ι (Prod.swap K J ⋙ G) ((Prod.braiding K J).inverse.obj (j, k))) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
g : (F ⋙ coyoneda.obj (op c.pt)).obj Y
j j' : J
φ : j ⟶ j'
this : (R.map φ).hom ≫ c.ι.app j' = c.ι.app j
⊢ F.partialLeftAdjointHomEquiv
      (F.partialLeftAdjointMap (R.map φ) ≫ F.partialLeftAdjointHomEquiv.symm (c.ι.app j' ≫ g)) =
    c.ι.app j ≫ g

Tactic:
partialLeftAdjointHomEquiv_map_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
g : (F ⋙ coyoneda.obj (op c.pt)).obj Y
j j' : J
φ : j ⟶ j'
this : (R.map φ).hom ≫ c.ι.app j' = c.ι.app j
⊢ (R.map φ).hom ≫ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointHomEquiv.symm (c.ι.app j' ≫ g)) = c.ι.app j ≫ g
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y Y' : C
g : Y ⟶ Y'
f : Y' ⟶ c'.pt
j : J
⊢ {
          toFun := fun f ↦
            hc.lift
              { pt := F.1 Y, π := { app := fun j ↦ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j), naturality := ⋯ } },
          invFun := fun g ↦
            hc'.lift
              { pt := Y, π := { app := fun j ↦ F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j), naturality := ⋯ } },
          left_inv := ⋯, right_inv := ⋯ }
        (g ≫ f) ≫
      c.π.app j =
    (ConcreteCategory.hom ((F.op ⋙ yoneda.obj c.pt).map g.op))
        ({
            toFun := fun f ↦
              hc.lift
                { pt := F.1 Y',
                  π := { app := fun j ↦ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j), naturality := ⋯ } },
            invFun := fun g ↦
              hc'.lift
                { pt := Y',
                  π := { app := fun j ↦ F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j), naturality := ⋯ } },
            left_inv := ⋯, right_inv := ⋯ }
          f) ≫
      c.π.app j

Tactic:
by
    dsimp
    simp only [IsLimit.fac, partialRightAdjointHomEquiv_comp, assoc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
⊢ IsSheafFor P (Sieve.pullback f (generate R)).arrows

Tactic:
← pullbackArrows_comm,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
⊢ IsSheafFor P (generate (pullbackArrows f R)).arrows
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
W : C
⊢ pullbackArrows f (singleton g) = singleton (pullback.snd g f)

Tactic:
ext h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
W : C
h : W ⟶ Y
⊢ pullbackArrows f (singleton g) h ↔ singleton (pullback.snd g f) h
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst✝ : ∀ (i : ι), HasPullback (g i) f
T : C
⊢ (ofArrows (fun i ↦ pullback (g i) f) fun x ↦ pullback.snd (g x) f) = pullbackArrows f (ofArrows Z g)

Tactic:
ext h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst✝ : ∀ (i : ι), HasPullback (g i) f
T : C
h : T ⟶ Y
⊢ ofArrows (fun i ↦ pullback (g i) f) (fun x ↦ pullback.snd (g x) f) h ↔ pullbackArrows f (ofArrows Z g) h
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✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X✝
Y✝ Z✝ : D
g : Z✝ ⟶ Y✝
X : C
α : X ⟶ X✝
β : Y✝ ⟶ F.obj X
hα : R.arrows α
⊢ Presieve.functorPushforward F R.arrows (g ≫ β ≫ F.map α)

Tactic:
exact ⟨X, α, g ≫ β, hα, by simp⟩

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X✝
hf : R.arrows f
⊢ (functorPullback F S).arrows f

Tactic:
apply hle

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X✝
hf : R.arrows f
⊢ (functorPushforward F R).arrows (F.map f)
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case h.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
T : J.Cover X := ⋯
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := ⋯
⊢ ∀ (y : E ⟶ P.obj (op X)), x.IsAmalgamation y → y = hh.lift K

Tactic:
intro e he

Goal state after:
case h.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
T : J.Cover X := ⟨S, hS⟩
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun I ↦ x I.f ⋯) ⋯
e : E ⟶ P.obj (op X)
he : x.IsAmalgamation e
⊢ e = hh.lift K
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
⊢ (G.preimage p).image p = G

Tactic:
by
  apply le_antisymm
  · rw [image_le_iff]
  · intro i x hx
    simp only [NatTrans.epi_iff_epi_app, epi_iff_surjective] at hp
    obtain ⟨y, rfl⟩ := hp _ x
    exact ⟨y, hx, rfl⟩

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

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
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ J.plusFunctor D ⋙ J.plusFunctor D ⋙ (whiskeringRight Cᵒᵖ D E).obj F ≅
    (whiskeringRight Cᵒᵖ D E).obj F ⋙ J.sheafification E

Tactic:
refine isoWhiskerLeft (J.plusFunctor D) (J.plusFunctorWhiskerRightIso _) ≪≫ ?_

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ J.plusFunctor D ⋙ (whiskeringRight Cᵒᵖ D E).obj F ⋙ J.plusFunctor E ≅
    (whiskeringRight Cᵒᵖ D E).obj F ⋙ J.sheafification E
Module: Mathlib.Topology.Category.TopCat.Basic

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso g
⊢ IsOpenEmbedding (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f)) ↔ IsOpenEmbedding ⇑(ConcreteCategory.hom f)

Tactic:
simp only
  exact isOpenEmbedding_iff_comp_isIso f g

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cone F
hc : IsLimit c
⊢ c.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.obj j).str

Tactic:
let c' := coneOfConeForget ((forget).mapCone c)

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cone F
hc : IsLimit c
c' : Cone F := coneOfConeForget (forget.mapCone c)
⊢ c.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.obj j).str
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case h.left
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : ↑(Y ⨯ Z)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom prod.fst) x
x₂ : ↑X
hx₂ : (ConcreteCategory.hom g) x₂ = (ConcreteCategory.hom prod.snd) x
⊢ (ConcreteCategory.hom (limit.π (pair Y Z) { as := WalkingPair.left }))
      ((ConcreteCategory.hom (prod.map f g)) ((ConcreteCategory.hom (W.prodIsoProd X).inv) (x₁, x₂))) =
    (ConcreteCategory.hom (limit.π (pair Y Z) { as := WalkingPair.left })) x

Tactic:
rw [← ConcreteCategory.comp_apply]
      erw [Limits.prod.map_fst]
      rw [ConcreteCategory.comp_apply, TopCat.prodIsoProd_inv_fst_apply]
      exact hx₁

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
⊢ IsVanKampenColimit (asEmptyCocone X)

Tactic:
by
  intro F' c' α f hf hα
  have : F' = Functor.empty C := by apply Functor.hext <;> rintro ⟨⟨⟩⟩
  subst this
  have := h.isIso_to f
  refine ⟨by rintro _ ⟨⟨⟩⟩,
    fun _ => ⟨IsColimit.ofIsoColimit h (Cocone.ext (asIso f).symm <| by rintro ⟨⟨⟩⟩)⟩⟩

Goal state after: