mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
this :
  ι.map
      (ι.preimage
        (Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
          kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n)))) =
    Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
      kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))
⊢ ι.map ((Λ.chainComplex X).d (n + 2) (n + 1)) =
    ι.map (Λ.chainComplexXIso X n).hom ≫
      Λ.π.app (kernel (ι.map ((Λ.chainComplex X).d (n + 1) n))) ≫ kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))

Tactic:
← this,

Goal state after:
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
this :
  ι.map
      (ι.preimage
        (Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
          kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n)))) =
    Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
      kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))
⊢ ι.map ((Λ.chainComplex X).d (n + 2) (n + 1)) =
    ι.map (Λ.chainComplexXIso X n).hom ≫
      ι.map
        (ι.preimage
          (Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
            kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))))
Module: Mathlib.Algebra.Category.ModuleCat.Localization

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
⊢ Limits.PreservesFiniteLimits (localizedModuleFunctor S)

Tactic:
have := ((Functor.exact_tfae _).out 1 3).mp (ModuleCat.localizedModuleFunctor_map_exact S)
  exact this.1

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Localization

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Submonoid R
M₁ M₂ M₃ : ModuleCat R
f₁ : M₁ ⟶ M₂
f₂ : M₂ ⟶ M₃
h₁ : IsLocalizedModule S (Hom.hom f₁)
h₂ : IsLocalizedModule S (Hom.hom (f₁ ≫ f₂))
⊢ Function.Bijective ⇑↑(IsLocalizedModule.linearEquiv S (Hom.hom f₁) (Hom.hom f₂ ∘ₗ Hom.hom f₁))

Tactic:
exact (IsLocalizedModule.linearEquiv ..).bijective

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: case succ.zero
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
hn : (Λ.chainComplexMap (f ≫ g)).f 0 = (Λ.chainComplexMap f ≫ Λ.chainComplexMap g).f 0
⊢ (Λ.chainComplexXOneIso X).hom ≫
      Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Z) (ι.map (Λ.F.map (f ≫ g))) (f ≫ g) ⋯) ≫ (Λ.chainComplexXOneIso Z).inv =
    ((Λ.chainComplexXOneIso X).hom ≫
        Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯) ≫ (Λ.chainComplexXOneIso Y).inv) ≫
      (Λ.chainComplexXOneIso Y).hom ≫
        Λ.F.map (kernel.map (Λ.π.app Y) (Λ.π.app Z) (ι.map (Λ.F.map g)) g ⋯) ≫ (Λ.chainComplexXOneIso Z).inv

Tactic:
simp only [chainComplexMap_f_succ_succ, assoc, Iso.cancel_iso_hom_left,
        Iso.inv_hom_id_assoc, ← Λ.F.map_comp_assoc, Iso.cancel_iso_inv_right_assoc]

Goal state after:
case succ.zero
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
hn : (Λ.chainComplexMap (f ≫ g)).f 0 = (Λ.chainComplexMap f ≫ Λ.chainComplexMap g).f 0
⊢ Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Z) (ι.map (Λ.F.map (f ≫ g))) (f ≫ g) ⋯) =
    Λ.F.map
      (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯ ≫
        kernel.map (Λ.π.app Y) (Λ.π.app Z) (ι.map (Λ.F.map g)) g ⋯)
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: case succ.succ
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
hn : (Λ.chainComplexMap (f ≫ g)).f (n + 1) = (Λ.chainComplexMap f ≫ Λ.chainComplexMap g).f (n + 1)
⊢ (Λ.chainComplexMap (f ≫ g)).f (n + 1 + 1) = (Λ.chainComplexMap f).f (n + 1 + 1) ≫ (Λ.chainComplexMap g).f (n + 1 + 1)

Tactic:
simp only [chainComplexMap_f_succ_succ, assoc, Iso.cancel_iso_hom_left,
        Iso.inv_hom_id_assoc, ← Λ.F.map_comp_assoc, Iso.cancel_iso_inv_right_assoc]

Goal state after:
case succ.succ
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
hn : (Λ.chainComplexMap (f ≫ g)).f (n + 1) = (Λ.chainComplexMap f ≫ Λ.chainComplexMap g).f (n + 1)
⊢ Λ.F.map
      (kernel.map (ι.map ((Λ.chainComplex X).d (n + 1) n)) (ι.map ((Λ.chainComplex Z).d (n + 1) n))
        (ι.map ((Λ.chainComplexMap (f ≫ g)).f (n + 1))) (ι.map ((Λ.chainComplexMap (f ≫ g)).f n)) ⋯) =
    Λ.F.map
      (kernel.map (ι.map ((Λ.chainComplex X).d (n + 1) n)) (ι.map ((Λ.chainComplex Y).d (n + 1) n))
          (ι.map ((Λ.chainComplexMap f).f (n + 1))) (ι.map ((Λ.chainComplexMap f).f n)) ⋯ ≫
        kernel.map (ι.map ((Λ.chainComplex Y).d (n + 1) n)) (ι.map ((Λ.chainComplex Z).d (n + 1) n))
          (ι.map ((Λ.chainComplexMap g).f (n + 1))) (ι.map ((Λ.chainComplexMap g).f n)) ⋯)
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
η μ : f ⟶ g
⊢ ∃ Z h, η ≫ h = μ ≫ h

Tactic:
· refine ⟨.mk (f.hom ≫ F.map (η.right ≫ IsFiltered.coeqHom η.right μ.right)),
      StructuredArrow.homMk (IsFiltered.coeqHom η.right μ.right) (by simp), ?_⟩
    simpa using IsFiltered.coeq_condition _ _

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofiltered D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
⊢ Nonempty C

Tactic:
by
      have : Nonempty D := IsCofiltered.nonempty
      obtain ⟨c, -⟩ := h (Classical.arbitrary D)
      exact ⟨c⟩

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
G : J × K ⥤ C
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
i : G ≅ uncurry.obj (curry.obj G)
this : HasLimit (uncurry.obj (curry.obj G))
⊢ limit G ≅ limit (curry.obj G ⋙ lim)

Tactic:
trans limit (uncurry.obj ((@curry J _ K _ C _).obj G))

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
G : J × K ⥤ C
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
i : G ≅ uncurry.obj (curry.obj G)
this : HasLimit (uncurry.obj (curry.obj G))
⊢ limit G ≅ limit (uncurry.obj (curry.obj G))

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
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
i : G ≅ uncurry.obj (curry.obj G)
this : HasLimit (uncurry.obj (curry.obj G))
⊢ limit (uncurry.obj (curry.obj G)) ≅ limit (curry.obj G ⋙ lim)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
m : ↑(M.obj X)
⊢ (ModuleCat.Hom.hom ((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).map (λ_ (M.obj Y)).inv))
      ((ModuleCat.Hom.hom (M.map f)) m) =
    (ModuleCat.Hom.hom ((Monoidal.tensorObj (unit (R ⋙ forget₂ CommRingCat RingCat)) M).map f))
      ((ModuleCat.Hom.hom (λ_ (M.obj X)).inv) m)

Tactic:
erw [leftUnitor_inv_apply, leftUnitor_inv_apply, tensorObj_map_tmul, (R.map f).hom.map_one]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
m : ↑(M.obj X)
⊢ 1 ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)] (ModuleCat.Hom.hom (M.map f)) m =
    1 ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M.map f)) m
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
hS : S ∈ {⊤}
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {⊤}
⊢ R ∈ {⊤}

Tactic:
rw [Set.mem_singleton_iff, ← Sieve.id_mem_iff_eq_top] at hS
    simpa using hR hS

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
D : Type u₁
inst✝ : Category.{v₁, u₁} D
S : J.Cover X
P : Cᵒᵖ ⥤ D
⊢ ∀ (b : S.shape.R), P.map (S.shape.fst b).f.op ≫ (S.index P).fst b = P.map (S.shape.snd b).f.op ≫ (S.index P).snd b

Tactic:
by
      intro I
      dsimp
      simp only [← P.map_comp, ← op_comp, I.r.w]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y = s.ι.app X_1 ≫ ((Functor.const S.arrows.category).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z) ⋯
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁ ⋯
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂ ⋯
hF :
  S.arrows.diagram.map (ObjectProperty.homMk F) ≫ s.ι.app { obj := Over.mk (g₂ ≫ f₂), property := hgf₂ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const S.arrows.category).obj s.pt).map (ObjectProperty.homMk F)
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }

Tactic:
have hF₁ := @Hs ⟨Over.mk (g₁ ≫ f₁), hgf₁⟩ ⟨Over.mk f₁, hf₁⟩ (ObjectProperty.homMk F₁)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y = s.ι.app X_1 ≫ ((Functor.const S.arrows.category).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z) ⋯
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁ ⋯
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂ ⋯
hF :
  S.arrows.diagram.map (ObjectProperty.homMk F) ≫ s.ι.app { obj := Over.mk (g₂ ≫ f₂), property := hgf₂ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const S.arrows.category).obj s.pt).map (ObjectProperty.homMk F)
hF₁ :
  S.arrows.diagram.map (ObjectProperty.homMk F₁) ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const S.arrows.category).obj s.pt).map (ObjectProperty.homMk F₁)
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }
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))
e : S ⟶ ⊤ := ⋯
⊢ (ConcreteCategory.hom ((J.diagram P X).map e.op))
      ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I ↦ P.map I.f.op) ⋯)) x) =
    (Meq.equiv P S).symm (Meq.mk S x)

Tactic:
dsimp [diagram]

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))
e : S ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom
        (Multiequalizer.lift (S.index P) (multiequalizer (⊤.index P))
          (fun I ↦ Multiequalizer.ι (⊤.index P) (Cover.Arrow.map I e)) ⋯))
      ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I ↦ P.map I.f.op) ⋯)) x) =
    (Meq.equiv P S).symm (Meq.mk S x)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case e'_2
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 T : J.Cover X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
I : (unop W).Arrow
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ : ToType (P.obj (op I.Y)) = CD (((unop W).index P).left I)
⊢ ↑(x.refine h1.unop) I =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x))

Tactic:
dsimp [diagram]

Goal state after:
case e'_2
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 T : J.Cover X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
I : (unop W).Arrow
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ : ToType (P.obj (op I.Y)) = CD (((unop W).index P).left I)
⊢ ↑x { Y := I.Y, f := I.f, hf := ⋯ } =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom
          (Multiequalizer.lift ((unop W).index P) (multiequalizer (S.index P))
            (fun I ↦ Multiequalizer.ι (S.index P) (Cover.Arrow.map I h1.unop)) ⋯))
        ((Meq.equiv P S).symm x))
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case e'_3
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 T : J.Cover X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
I : (unop W).Arrow
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ : ToType (P.obj (op I.Y)) = CD (((unop W).index P).left I)
⊢ ↑(y.refine h2.unop) I =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))

Tactic:
dsimp [diagram]

Goal state after:
case e'_3
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 T : J.Cover X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
I : (unop W).Arrow
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ : ToType (P.obj (op I.Y)) = CD (((unop W).index P).left I)
⊢ ↑y { Y := I.Y, f := I.f, hf := ⋯ } =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom
          (Multiequalizer.lift ((unop W).index P) (multiequalizer (T.index P))
            (fun I ↦ Multiequalizer.ι (T.index P) (Cover.Arrow.map I h2.unop)) ⋯))
        ((Meq.equiv P T).symm y))
Module: Mathlib.CategoryTheory.Subfunctor.Sieves

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
V W : C
i : V ⟶ unop U
hi : (ConcreteCategory.hom (F.map i.op)) s ∈ G.obj (op V)
j : W ⟶ V
⊢ (ConcreteCategory.hom (F.map (j ≫ i).op)) s ∈ G.obj (op W)

Tactic:
by
    simpa using G.map _ hi

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
⊢ ∀ {U V : Cᵒᵖ} (i : U ⟶ V),
    {s | G.sieveOfSection s ∈ J (unop U)} ⊆ ⇑(ConcreteCategory.hom (F.map i)) ⁻¹' {s | G.sieveOfSection s ∈ J (unop V)}

Tactic:
by
    rintro U V i s hs
    refine J.superset_covering ?_ (J.pullback_stable i.unop hs)
    intro _ _ h
    dsimp at h ⊢
    rwa [← comp_apply, ← Functor.map_comp]

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

Goal state before:
pp: case e'_2
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✝ T : J.Cover X
x : Meq P S✝
y : Meq P T
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ (ConcreteCategory.hom (Multiequalizer.ι ((unop (op S)).index P) i))
      ((ConcreteCategory.hom ((J.diagram P X).map h1.op)) ((Meq.equiv P S✝).symm x)) =
    ↑(x.refine h1) i

Tactic:
dsimp [diagram]

Goal state after:
case e'_2
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✝ T : J.Cover X
x : Meq P S✝
y : Meq P T
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ (ConcreteCategory.hom (Multiequalizer.ι (S.index P) i))
      ((ConcreteCategory.hom
          (Multiequalizer.lift (S.index P) (multiequalizer (S✝.index P))
            (fun I ↦ Multiequalizer.ι (S✝.index P) (Cover.Arrow.map I h1)) ⋯))
        ((Meq.equiv P S✝).symm x)) =
    ↑x { Y := i.Y, f := i.f, hf := ⋯ }