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

Goal state before:
pp: case succ
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)

Tactic:
let ⟨I', _, f', _⟩ := EnoughInjectives.presentation N
    have : Module.Injective R' I' := Module.injective_module_of_injective_object R' I'
    have injf' : Function.Injective f'.hom := (mono_iff_injective f').mp ‹_›
    let S' : ShortComplex (ModuleCat.{v} R') :=
      ModuleCat.shortComplexOfCompEqZero _ _ f'.hom.exact_map_mkQ_range.linearMap_comp_eq_zero
    have exactS' := ModuleCat.shortComplex_shortExact S'
      f'.hom.exact_map_mkQ_range injf' (Submodule.mkQ_surjective _)
    let I : ModuleCat.{v} R :=
      let := Module.compHom I' eR.toRingHom
      ModuleCat.of R I'
    let eI : I ≃ₛₗ[RingHomClass.toRingHom eR] I' := {
      __ := AddEquiv.refl I
      map_smul' r i := rfl }
    have : Injective (ModuleCat.of R I) := by
      rw [← Module.injective_iff_injective_object]
      exact Module.Injective.of_ringEquiv eR.symm eI.symm
    let f : M →ₗ[R] I := eI.symm.toLinearMap.comp (f'.hom.comp e.toLinearMap)
    have injf : Function.Injective f := by simpa [f]
    let S : ShortComplex (ModuleCat.{v} R) :=
      ModuleCat.shortComplexOfCompEqZero _ _ f.exact_map_mkQ_range.linearMap_comp_eq_zero
    have exactS := ModuleCat.shortComplex_shortExact S
      f.exact_map_mkQ_range injf (Submodule.mkQ_surjective _)
    let eCoker : ModuleCat.of R (I ⧸ f.range) ≃ₛₗ[RingHomClass.toRingHom eR]
      ModuleCat.of R' (I' ⧸ f'.hom.range) :=
      Submodule.Quotient.equiv _ _ eI
        (by simp [f, ← Submodule.map_symm_eq_iff eI, LinearMap.range_comp])
    exact (exactS.hasInjectiveDimensionLT_X₃_iff n inferInstance).symm.trans
      ((ih eCoker).trans (exactS'.hasInjectiveDimensionLT_X₃_iff n inferInstance))

Goal state after:
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 : ℕ
⊢ (ComplexShape.down ℕ).Rel (n + 2) (n + 1)

Tactic:
by dsimp; lia

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

Goal state before:
pp: C : Type u'
inst✝ : Category.{v', u'} C
R R' : Cᵒᵖ ⥤ RingCat
M' : PresheafOfModules R'
α : R ⟶ R'
X Y : Cᵒᵖ
f : X ⟶ Y
r : ↑(R.obj X)
x : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj (M'.obj X))
eq :
  (RingCat.Hom.hom (α.app Y)) ((RingCat.Hom.hom (R.map f)) r) =
    (RingCat.Hom.hom (R'.map f)) ((RingCat.Hom.hom (α.app X)) r)
⊢ (ConcreteCategory.hom (R'.map f)) ((ConcreteCategory.hom (α.app X)) r) • (ConcreteCategory.hom (M'.map f)) x =
    (RingHom.id ↑(R.obj X)) r • (ConcreteCategory.hom (M'.map f)) x

Tactic:
rw [← eq]

Goal state after:
C : Type u'
inst✝ : Category.{v', u'} C
R R' : Cᵒᵖ ⥤ RingCat
M' : PresheafOfModules R'
α : R ⟶ R'
X Y : Cᵒᵖ
f : X ⟶ Y
r : ↑(R.obj X)
x : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj (M'.obj X))
eq :
  (RingCat.Hom.hom (α.app Y)) ((RingCat.Hom.hom (R.map f)) r) =
    (RingCat.Hom.hom (R'.map f)) ((RingCat.Hom.hom (α.app X)) r)
⊢ (RingCat.Hom.hom (α.app Y)) ((RingCat.Hom.hom (R.map f)) r) • (ConcreteCategory.hom (M'.map f)) x =
    (RingHom.id ↑(R.obj X)) r • (ConcreteCategory.hom (M'.map f)) x
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : InitiallySmall J
i : J
⊢ ∃ j ∈ Set.range (fromInitialModel J).obj, Nonempty (j ⟶ i)

Tactic:
obtain ⟨f⟩ : Nonempty (CostructuredArrow (fromInitialModel J) i) := IsConnected.is_nonempty

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : InitiallySmall J
i : J
f : CostructuredArrow (fromInitialModel J) i
⊢ ∃ j ∈ Set.range (fromInitialModel J).obj, Nonempty (j ⟶ i)
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✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitCurrySwapCompLimIsoLimitCurryCompLim G).hom ≫ limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j

Tactic:
dsimp [limitCurrySwapCompLimIsoLimitCurryCompLim, Equivalence.counit]

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✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (((limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫
          (HasLimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).hom) ≫
        (limitIsoLimitCurryCompLim G).hom) ≫
      limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
m : ModuleColimit hcR hcM
m' : ModuleColimit hcR hcM'
m'' : ModuleColimit hcR hcM''
U : Cᵒᵖ
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
x' : (M'.presheaf ⋙ forget AddCommGrpCat).obj U
x'' : (M''.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  (ConcreteCategory.hom
        ((((forget AddCommGrpCat).mapCocone cM).tensor
                (((forget AddCommGrpCat).mapCocone cM').tensor ((forget AddCommGrpCat).mapCocone cM''))).ι.app
          U))
      (x, x', x'') =
    (m, m', m'')
⊢ ∃ U x x' x'', ιM x = m ∧ ιM x' = m' ∧ ιM x'' = m''

Tactic:
rw [Prod.ext_iff, Prod.ext_iff] at h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
m : ModuleColimit hcR hcM
m' : ModuleColimit hcR hcM'
m'' : ModuleColimit hcR hcM''
U : Cᵒᵖ
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
x' : (M'.presheaf ⋙ forget AddCommGrpCat).obj U
x'' : (M''.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  ((ConcreteCategory.hom
            ((((forget AddCommGrpCat).mapCocone cM).tensor
                    (((forget AddCommGrpCat).mapCocone cM').tensor ((forget AddCommGrpCat).mapCocone cM''))).ι.app
              U))
          (x, x', x'')).1 =
      (m, m', m'').1 ∧
    ((ConcreteCategory.hom
                ((((forget AddCommGrpCat).mapCocone cM).tensor
                        (((forget AddCommGrpCat).mapCocone cM').tensor ((forget AddCommGrpCat).mapCocone cM''))).ι.app
                  U))
              (x, x', x'')).2.1 =
        (m, m', m'').2.1 ∧
      ((ConcreteCategory.hom
                ((((forget AddCommGrpCat).mapCocone cM).tensor
                        (((forget AddCommGrpCat).mapCocone cM').tensor ((forget AddCommGrpCat).mapCocone cM''))).ι.app
                  U))
              (x, x', x'')).2.2 =
        (m, m', m'').2.2
⊢ ∃ U x x' x'', ιM x = m ∧ ιM x' = m' ∧ ιM x'' = m''
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
r₁ r₂ : ↑cR.pt
m : ModuleColimit hcR hcM
U : Cᵒᵖ
a₁ a₂ : (R ⋙ forget RingCat).obj U
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  (ConcreteCategory.hom
        ((((forget RingCat).mapCocone cR).tensor
                (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
          U))
      (a₁, a₂, x) =
    (r₁, r₂, m)
⊢ ∃ U a₁ a₂ x, (ιR cR) a₁ = r₁ ∧ (ιR cR) a₂ = r₂ ∧ ιM x = m

Tactic:
rw [Prod.ext_iff, Prod.ext_iff] at h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
r₁ r₂ : ↑cR.pt
m : ModuleColimit hcR hcM
U : Cᵒᵖ
a₁ a₂ : (R ⋙ forget RingCat).obj U
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  ((ConcreteCategory.hom
            ((((forget RingCat).mapCocone cR).tensor
                    (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
              U))
          (a₁, a₂, x)).1 =
      (r₁, r₂, m).1 ∧
    ((ConcreteCategory.hom
                ((((forget RingCat).mapCocone cR).tensor
                        (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
                  U))
              (a₁, a₂, x)).2.1 =
        (r₁, r₂, m).2.1 ∧
      ((ConcreteCategory.hom
                ((((forget RingCat).mapCocone cR).tensor
                        (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
                  U))
              (a₁, a₂, x)).2.2 =
        (r₁, r₂, m).2.2
⊢ ∃ U a₁ a₂ x, (ιR cR) a₁ = r₁ ∧ (ιR cR) a₂ = r₂ ∧ ιM x = m
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
r : ↑cR.pt
m₁ : ModuleColimit hcR hcM
m₂ : ModuleColimit hcR hcM'
U : Cᵒᵖ
a : (R ⋙ forget RingCat).obj U
x₁ : (M.presheaf ⋙ forget AddCommGrpCat).obj U
x₂ : (M'.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  (ConcreteCategory.hom
        ((((forget RingCat).mapCocone cR).tensor
                (((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM'))).ι.app
          U))
      (a, x₁, x₂) =
    (r, m₁, m₂)
⊢ ∃ U a x₁ x₂, (ιR cR) a = r ∧ ιM x₁ = m₁ ∧ ιM x₂ = m₂

Tactic:
rw [Prod.ext_iff, Prod.ext_iff] at h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
r : ↑cR.pt
m₁ : ModuleColimit hcR hcM
m₂ : ModuleColimit hcR hcM'
U : Cᵒᵖ
a : (R ⋙ forget RingCat).obj U
x₁ : (M.presheaf ⋙ forget AddCommGrpCat).obj U
x₂ : (M'.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  ((ConcreteCategory.hom
            ((((forget RingCat).mapCocone cR).tensor
                    (((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM'))).ι.app
              U))
          (a, x₁, x₂)).1 =
      (r, m₁, m₂).1 ∧
    ((ConcreteCategory.hom
                ((((forget RingCat).mapCocone cR).tensor
                        (((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM'))).ι.app
                  U))
              (a, x₁, x₂)).2.1 =
        (r, m₁, m₂).2.1 ∧
      ((ConcreteCategory.hom
                ((((forget RingCat).mapCocone cR).tensor
                        (((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM'))).ι.app
                  U))
              (a, x₁, x₂)).2.2 =
        (r, m₁, m₂).2.2
⊢ ∃ U a x₁ x₂, (ιR cR) a = r ∧ ιM x₁ = m₁ ∧ ιM x₂ = m₂
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
X : F.PartialRightAdjointSource
⊢ F.partialRightAdjointMap (𝟙 X) = 𝟙 (F.partialRightAdjointObj X)

Tactic:
apply F.partialRightAdjointHomEquiv.injective
    simp [partialRightAdjointHomEquiv_map]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ F' F'' : C ⥤ Type w
G✝ G' F G H : Subfunctor F✝
h₁ : F ≤ H
h₂ : G ≤ H
U : C
⊢ { obj := fun U ↦ F.obj U ⊔ G.obj U, map := ⋯ }.obj U ⊆ H.obj U

Tactic:
rintro x (h | h)

Goal state after:
case inl
C : Type u
inst✝ : Category.{v, u} C
F✝ F' F'' : C ⥤ Type w
G✝ G' F G H : Subfunctor F✝
h₁ : F ≤ H
h₂ : G ≤ H
U : C
x : F✝.obj U
h : x ∈ F.obj U
⊢ x ∈ H.obj U

case inr
C : Type u
inst✝ : Category.{v, u} C
F✝ F' F'' : C ⥤ Type w
G✝ G' F G H : Subfunctor F✝
h₁ : F ≤ H
h₂ : G ≤ H
U : C
x : F✝.obj U
h : x ∈ G.obj U
⊢ x ∈ H.obj U
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (Pretopology C)
X : C
S : Presieve X
⊢ S ∈ (sInf T).coverings X ↔ ∀ t ∈ T, S ∈ t.coverings X

Tactic:
by
  change S ∈ sInf ((fun J : Pretopology C ↦ J.coverings) '' T) X ↔ _
  simp

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
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
⊢ x.sieveExtend f ⋯ = x f hf

Tactic:
have h := (le_generate R Y _ hf).choose_spec
  unfold FamilyOfElements.sieveExtend
  rw [t h.choose (𝟙 _) _ hf _]
  · simp
  · rw [id_comp]
    exact h.choose_spec.choose_spec.2

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
x✝¹ : C
x✝ : x✝¹ ⟶ X
h : (generate R).arrows x✝
⊢ ⋯.choose ≫ ⋯.choose = x✝

Tactic:
exact h.choose_spec.choose_spec.choose_spec.2

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

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

Tactic:
← id_mem_iff_eq_top,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Sieve X
f : Y ⟶ X
⊢ S.arrows f ↔ (pullback f S).arrows (𝟙 Y)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom)
            ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).inv) a)).Compatible →
        ∃! x, (ConcreteCategory.hom (forkMap P S.arrows)) x = (firstObjEqFamily P S.arrows).toEquiv.symm a

Tactic:
simp only [Iso.inv_hom_id_apply]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      a.Compatible → ∃! x, (ConcreteCategory.hom (forkMap P S.arrows)) x = (firstObjEqFamily P S.arrows).toEquiv.symm a
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
⊢ B ≤ Sx

Tactic:
rintro Y f ⟨Z, e1, e2, he2, he1, 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 f
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 ⋯
⊢ B ≤ Sy

Tactic:
rintro Y f ⟨Z, e1, e2, he2, he1, 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 f
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
x y : CD (P.obj (op X))
h : ∃ W h1 h2, (Meq.mk ⊤ x).refine h1 = (Meq.mk ⊤ y).refine h2
⊢ x = y

Tactic:
obtain ⟨W, h1, h2, hh⟩ := h

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)
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
x y : CD (P.obj (op X))
W : J.Cover X
h1 h2 : W ⟶ ⊤
hh : (Meq.mk ⊤ x).refine h1 = (Meq.mk ⊤ y).refine h2
⊢ x = y
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf J G'.toFunctor
U : Cᵒᵖ
x : F.obj U
hx : x ∈ (sheafify J G).obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection x).arrows i
⊢ (ConcreteCategory.hom (F.map i.op)) x =
    (ConcreteCategory.hom (F.map i.op)) ↑((ConcreteCategory.hom ((G.sheafifyLift (homOfLe h) hG').app U)) ⟨x, hx⟩)

Tactic:
have :=
    congr_arg (fun f : G.toFunctor ⟶ G'.toFunctor => (NatTrans.app f (op V) ⟨_, hi⟩).1)
      (G.to_sheafifyLift (Subfunctor.homOfLe h) hG')

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf J G'.toFunctor
U : Cᵒᵖ
x : F.obj U
hx : x ∈ (sheafify J G).obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection x).arrows i
this :
  ↑((ConcreteCategory.hom ((homOfLe ⋯ ≫ G.sheafifyLift (homOfLe h) hG').app (op V)))
        ⟨(ConcreteCategory.hom (F.map i.op)) x, hi⟩) =
    ↑((ConcreteCategory.hom ((homOfLe h).app (op V))) ⟨(ConcreteCategory.hom (F.map i.op)) x, hi⟩)
⊢ (ConcreteCategory.hom (F.map i.op)) x =
    (ConcreteCategory.hom (F.map i.op)) ↑((ConcreteCategory.hom ((G.sheafifyLift (homOfLe h) hG').app U)) ⟨x, hx⟩)