mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommSemiring S
inst✝¹ : Semiring R
inst✝ : Algebra S R
p✝ : Submodule S R
i j : ℕ
p q : R
hp : p ∈ p✝ ^ i
hq : q ∈ p✝ ^ j
⊢ p * q ∈ p✝ ^ (i + j)

Tactic:
rw [pow_add]
    exact Submodule.mul_mem_mul hp hq

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: case inl.inl
α : Type u_1
n : ℕ
h1 : 0 < n
val✝ : Fintype α
h2 : n < Nat.card α
h : (Nat.card α).choose n = 0
⊢ False

pp: case inl.inr
α : Type u_1
n : ℕ
h1 : 0 < n
val✝ : Fintype α
h2 : n < Nat.card α
h : (Nat.card α).choose n = 1
⊢ False

Tactic:
· rw [Nat.choose_eq_zero_iff] at h
      exact (lt_self_iff_false n).mp (lt_trans h2 h)

Goal state after:
case inl.inr
α : Type u_1
n : ℕ
h1 : 0 < n
val✝ : Fintype α
h2 : n < Nat.card α
h : (Nat.card α).choose n = 1
⊢ False
Module: Mathlib.Algebra.Category.ModuleCat.ExteriorPower

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
n : ℕ
f g : M.exteriorPower n ⟶ N
h : mk.postcomp f = mk.postcomp g
⊢ f = g

Tactic:
by
  ext : 1
  exact exteriorPower.linearMap_ext h

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁸ : CommRing R
M : Type u2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : IsCentralScalar R M
inst✝¹ : Module Rᵐᵒᵖ N
inst✝ : IsCentralScalar R N
f : M →ₗ[R] N
⊢ toTrivSqZeroExt.comp (map f) = (TrivSqZeroExt.map f).comp toTrivSqZeroExt

Tactic:
apply hom_ext

Goal state after:
R : Type u1
inst✝⁸ : CommRing R
M : Type u2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : IsCentralScalar R M
inst✝¹ : Module Rᵐᵒᵖ N
inst✝ : IsCentralScalar R N
f : M →ₗ[R] N
⊢ (toTrivSqZeroExt.comp (map f)).toLinearMap ∘ₗ ι R = ((TrivSqZeroExt.map f).comp toTrivSqZeroExt).toLinearMap ∘ₗ ι R
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: case trans
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
c d x✝ y✝ z✝ : (j : C) × F.obj j
a✝¹ : Relation.EqvGen F.ColimitTypeRel x✝ y✝
a✝ : Relation.EqvGen F.ColimitTypeRel y✝ z✝
ih₁ : Zigzag x✝.fst y✝.fst
ih₂ : Zigzag y✝.fst z✝.fst
⊢ Zigzag x✝.fst z✝.fst

Tactic:
exact ih₁.trans ih₂

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
⊢ (Functor.diag D).Final

Tactic:
let : D × D ≌ C × C := Equivalence.prod e e

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
this : D × D ≌ C × C := e.prod e
⊢ (Functor.diag D).Final
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFilteredOrEmpty J
⊢ FinallySmall J ↔ ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)

Tactic:
refine ⟨fun _ => FinallySmall.exists_small_weakly_terminal_set _, fun h => ?_⟩
  rcases h with ⟨s, hs, hs'⟩
  exact finallySmall_of_small_weakly_terminal_set s hs'

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Colimits

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : MonoidalCategory C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst✝⁴ : Category.{v_2, u_2} J
inst✝³ : Category.{v_3, u_3} J₁
inst✝² : Category.{v_4, u_4} J₂
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst✝¹ : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst✝ : IsSifted J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ IsColimit (c₁.tensor c₂)

Tactic:
by
  refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).1
    ((Functor.Final.isColimitWhiskerEquiv (Functor.diag J) _).2 (hc₁.tensor₂ hc₂))
  · exact NatIso.ofComponents (fun _ ↦ Iso.refl _) (fun _ ↦ by simp)
  · exact Cocone.ext (Iso.refl _)

Goal state after:
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₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X : Cᵒᵖ
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ModuleCat.Hom.hom (tensorObjMap M₁ M₂ (𝟙 X))) (m₁ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X)] m₂) =
    (ModuleCat.Hom.hom
        ((ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map (𝟙 X))) ⋯).inv.app
          (M₁.obj X ⊗ M₂.obj X)))
      (m₁ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X)] m₂)

Tactic:
dsimp [tensorObjMap]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X : Cᵒᵖ
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ConcreteCategory.hom (M₁.map (𝟙 X))) m₁ ⊗ₜ[↑(R.obj X)] (ConcreteCategory.hom (M₂.map (𝟙 X))) m₂ =
    m₁ ⊗ₜ[↑(R.obj X)] m₂
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₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ Y✝ Z✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
m₁ : ↑(M₁.obj X✝)
m₂ : ↑(M₂.obj X✝)
⊢ (ModuleCat.Hom.hom (tensorObjMap M₁ M₂ (f ≫ g))) (m₁ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X✝)] m₂) =
    (ModuleCat.Hom.hom
        (tensorObjMap M₁ M₂ f ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).map
              (tensorObjMap M₁ M₂ g) ≫
            (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))
                    (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map g))
                    (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map (f ≫ g))) ⋯).inv.app
              (M₁.obj Z✝ ⊗ M₂.obj Z✝)))
      (m₁ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X✝)] m₂)

Tactic:
dsimp [tensorObjMap]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ Y✝ Z✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
m₁ : ↑(M₁.obj X✝)
m₂ : ↑(M₂.obj X✝)
⊢ (ConcreteCategory.hom (M₁.map (f ≫ g))) m₁ ⊗ₜ[↑(R.obj Z✝)] (ConcreteCategory.hom (M₂.map (f ≫ g))) m₂ =
    (ConcreteCategory.hom (M₁.map g)) ((ConcreteCategory.hom (M₁.map f)) m₁) ⊗ₜ[↑(R.obj Z✝)]
      (ConcreteCategory.hom (M₂.map g)) ((ConcreteCategory.hom (M₂.map f)) m₂)
Module: Mathlib.CategoryTheory.Sites.Pretopology

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

Tactic:
apply funext

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
i : (i : ι) × j (g i) ⋯
⊢ (ofArrows Z g).bind (fun x f H ↦ ofArrows (W f H) (k f H)) (k (g i.fst) ⋯ i.snd ≫ g i.fst)

Tactic:
exact bind_comp _ (ofArrows.mk _) (ofArrows.mk _)

Goal state after:
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 (firstMap P S)) ((firstObjEqFamily P S.arrows).toEquiv.symm a) =
          (ConcreteCategory.hom (secondMap P S)) ((firstObjEqFamily P S.arrows).toEquiv.symm a) →
        ∃! x, (ConcreteCategory.hom (forkMap P S.arrows)) x = (firstObjEqFamily P S.arrows).toEquiv.symm a

Tactic:
← compatible_iff

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),
      ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom)
            ((firstObjEqFamily P S.arrows).toEquiv.symm a)).Compatible →
        ∃! x, (ConcreteCategory.hom (forkMap P S.arrows)) x = (firstObjEqFamily P S.arrows).toEquiv.symm a
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
R : Presieve X
inst✝ : R.HasPairwisePullbacks
fg : ((Y : C) × { f // R f }) × (Z : C) × { g // R g }
x✝ : P.obj (op X)
this : HasPullback ↑fg.1.snd ↑fg.2.snd
⊢ (ConcreteCategory.hom (P.map (↑fg.1.snd).op ≫ P.map (pullback.fst ↑fg.1.snd ↑fg.2.snd).op)).toFun x✝ =
    (ConcreteCategory.hom (P.map (↑fg.2.snd).op ≫ P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd).op)).toFun x✝

Tactic:
rw [← P.map_comp, ← op_comp, pullback.condition]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
fg : ((Y : C) × { f // R f }) × (Z : C) × { g // R g }
x✝ : P.obj (op X)
this : HasPullback ↑fg.1.snd ↑fg.2.snd
⊢ (ConcreteCategory.hom (P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd ≫ ↑fg.2.snd).op)).toFun x✝ =
    (ConcreteCategory.hom (P.map (↑fg.2.snd).op ≫ P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd).op)).toFun x✝
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
R : Presieve X
inst✝ : R.HasPairwisePullbacks
⊢ Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      (ConcreteCategory.hom (firstMap P R)) ((firstObjEqFamily P R).toEquiv.symm a) =
          (ConcreteCategory.hom (secondMap P R)) ((firstObjEqFamily P R).toEquiv.symm a) →
        ∃! x, (ConcreteCategory.hom (forkMap P R)) x = (firstObjEqFamily P R).toEquiv.symm a

Tactic:
← compatible_iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
⊢ Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      ((ConcreteCategory.hom (firstObjEqFamily P R).hom) ((firstObjEqFamily P R).toEquiv.symm a)).Compatible →
        ∃! x, (ConcreteCategory.hom (forkMap P R)) x = (firstObjEqFamily P R).toEquiv.symm a
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve (Z i)
T W : C
v : T ⟶ W
v' : W ⟶ X
hv' : (Sieve.ofArrows Z f).arrows v'
S : C
u : T ⟶ S
u' : S ⟶ Z (Sieve.ofArrows.i hv')
h : R (Sieve.ofArrows.i hv') u'
hu : u ≫ u' = v ≫ Sieve.ofArrows.h hv'
⊢ (Sieve.generate (bindOfArrows Z f R)).arrows (u ≫ u' ≫ f (Sieve.ofArrows.i hv'))

Tactic:
exact ⟨S, u, u' ≫ f _, ⟨_, _, h⟩, rfl⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ Presieve.IsSheafFor F (Presieve.singleton f) ↔ Nonempty (IsLimit (Fork.ofι (F.map f.op) ⋯))

Tactic:
have h (x : F.obj (op X)) : (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
      p₁ ≫ f = p₂ ≫ f → F.map p₁.op x = F.map p₂.op x) ↔ F.map c.fst.op x = F.map c.snd.op x := by
    refine ⟨fun H ↦ H _ _ c.condition, fun H Z p₁ p₂ h ↦ ?_⟩
    rw [← PullbackCone.IsLimit.lift_fst hc _ _ h, op_comp, Functor.map_comp, comp_apply, H]
    simp [← comp_apply, ← Functor.map_comp, ← op_comp]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h :
  ∀ (x : F.obj (op X)),
    (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
        p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x) ↔
      (ConcreteCategory.hom (F.map c.fst.op)) x = (ConcreteCategory.hom (F.map c.snd.op)) x
⊢ Presieve.IsSheafFor F (Presieve.singleton f) ↔ Nonempty (IsLimit (Fork.ofι (F.map f.op) ⋯))
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
hx₁ : x₁.Compatible
this : ∀ (t₂ : P₂.obj (op X)), x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂)
t₂ : P₂.obj (op X)
ht₂ : x₂.IsAmalgamation t₂
⊢ x₁.IsAmalgamation (e.symm t₂)

Tactic:
by simpa only [this] using ht₂

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ P.map f.op ≫ P.map (pullback.fst f g).op = P.map g.op ≫ P.map (pullback.snd f g).op

Tactic:
rw [← P.map_comp, ← op_comp, pullback.condition]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ P.map (pullback.snd f g ≫ g).op = P.map g.op ≫ P.map (pullback.snd f g).op
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
⊢ Compatible P π x ↔ PullbackCompatible P π x

Tactic:
refine ⟨fun t i j ↦ ?_, fun t i j Z gi gj comm ↦ ?_⟩

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
t : Compatible P π x
i j : I
⊢ (ConcreteCategory.hom (P.map (pullback.fst (π i) (π j)).op)) (x i) =
    (ConcreteCategory.hom (P.map (pullback.snd (π i) (π j)).op)) (x j)

case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
t : PullbackCompatible P π x
i j : I
Z : C
gi : Z ⟶ X i
gj : Z ⟶ X j
comm : gi ≫ π i = gj ≫ π j
⊢ (ConcreteCategory.hom (P.map gi.op)) (x i) = (ConcreteCategory.hom (P.map gj.op)) (x j)
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 : Subfunctor F
h : Presieve.IsSheaf J F
⊢ Presieve.IsSheaf J G.toFunctor ↔ ∀ (U : Cᵒᵖ) (s : F.obj U), G.sieveOfSection s ∈ J (unop U) → s ∈ G.obj U

Tactic:
← G.eq_sheafify_iff h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F
⊢ G = sheafify J G ↔ ∀ (U : Cᵒᵖ) (s : F.obj U), G.sieveOfSection s ∈ J (unop U) → s ∈ G.obj U
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
h : Presieve.IsSheaf J F'
l₁ l₂ : (sheafify J G).toFunctor ⟶ F'
e : homOfLe ⋯ ≫ l₁ = homOfLe ⋯ ≫ l₂
U : Cᵒᵖ
s : (sheafify J G).toFunctor.obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection ↑s).arrows i
⊢ (ConcreteCategory.hom (l₁.app (op V))) ({ toFun := fun x ↦ ⟨(ConcreteCategory.hom (F.map i.op)) ↑x, ⋯⟩ } s) =
    (ConcreteCategory.hom (l₂.app (op V))) ({ toFun := fun x ↦ ⟨(ConcreteCategory.hom (F.map i.op)) ↑x, ⋯⟩ } s)

Tactic:
exact ConcreteCategory.congr_hom (congr_app e <| op V) ⟨_, hi⟩

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
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
S : J.Cover X
s : Meq (J.plusObj P) S
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
II : (S.bind T).Relation
⊢ (II.r.g₁ ≫ II.fst.toMiddleHom) ≫ { Y := II.fst.middle, f := II.fst.fromMiddleHom, hf := ⋯ }.f =
    (II.r.g₂ ≫ II.snd.toMiddleHom) ≫ { Y := II.snd.middle, f := II.snd.fromMiddleHom, hf := ⋯ }.f

Tactic:
by simpa only [Category.assoc, Cover.Arrow.middle_spec] using II.r.w

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

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
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : sheafify J P ⟶ Q
h : (sheafificationAdjunction J D).unit.app P ≫ γ = η
⊢ γ = sheafifyLift J η hQ

Tactic:
rw [sheafifyLift]

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
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : sheafify J P ⟶ Q
h : (sheafificationAdjunction J D).unit.app P ≫ γ = η
⊢ γ = (((sheafificationAdjunction J D).homEquiv P { obj := Q, property := hQ }).symm η).hom
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
⊢ ∀ (b : W.shape.R),
    (S.ι (W.shape.fst b) ≫ (E.π.app k).app (op (W.shape.fst b).Y)) ≫ (W.index (F.obj k).obj).fst b =
      (S.ι (W.shape.snd b) ≫ (E.π.app k).app (op (W.shape.snd b).Y)) ≫ (W.index (F.obj k).obj).snd b

Tactic:
by
            intro i
            simp only [Category.assoc]
            erw [← (E.π.app k).naturality, ← (E.π.app k).naturality]
            dsimp
            simp only [← Category.assoc]
            congr 1
            apply S.condition

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.sheafify P ⟶ Q
h : J.toSheafify P ≫ γ = η
⊢ (J.toPlus P ≫ J.toPlus (J.plusObj P)) ≫ γ = η

Tactic:
← plusMap_toPlus

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.sheafify P ⟶ Q
h : J.toSheafify P ≫ γ = η
⊢ (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ γ = η
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : J.sheafify P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toSheafify P ≫ η = J.toSheafify P ≫ γ
⊢ (J.toPlus P ≫ J.toPlus (J.plusObj P)) ≫ η = (J.toPlus P ≫ J.toPlus (J.plusObj P)) ≫ γ

Tactic:
← plusMap_toPlus

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : J.sheafify P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toSheafify P ≫ η = J.toSheafify P ≫ γ
⊢ (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ η = (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ γ
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ IsColimit (X.binaryCofan Y)

Tactic:
refine Limits.BinaryCofan.isColimitMk (fun s => ofHom
    { toFun := Sum.elim s.inl s.inr, continuous_toFun := ?_ }) ?_ ?_ ?_
  · fun_prop
  · intro s
    ext
    rfl
  · intro s
    ext
    rfl
  · intro s m h₁ h₂
    ext (x | x)
    exacts [ConcreteCategory.congr_hom h₁ x, ConcreteCategory.congr_hom h₂ x]

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

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : J ⥤ C
⊢ ∀ (c'_1 : Cocone F') (α : F' ⟶ F) (f : c'_1.pt ⟶ c'.pt),
    α ≫ c'.ι = c'_1.ι ≫ (const J).map f →
      NatTrans.Equifibered α →
        (∀ (j : J), IsPullback (c'_1.ι.app j) (α.app j) f (c'.ι.app j)) → Nonempty (IsColimit c'_1)

Tactic:
c''

Goal state after:
J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
⊢ ∀ (α : F' ⟶ F) (f : c''.pt ⟶ c'.pt),
    α ≫ c'.ι = c''.ι ≫ (const J).map f →
      NatTrans.Equifibered α → (∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)) → Nonempty (IsColimit c'')
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
⊢ ∀ (c'_1 : Cocone F') (α : F' ⟶ F) (f : c'_1.pt ⟶ c'.pt),
    α ≫ c'.ι = c'_1.ι ≫ (const J).map f →
      NatTrans.Equifibered α →
        (Nonempty (IsColimit c'_1) ↔ ∀ (j : J), IsPullback (c'_1.ι.app j) (α.app j) f (c'.ι.app j))

Tactic:
c''

Goal state after:
J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
⊢ ∀ (α : F' ⟶ F) (f : c''.pt ⟶ c'.pt),
    α ≫ c'.ι = c''.ι ≫ (const J).map f →
      NatTrans.Equifibered α → (Nonempty (IsColimit c'') ↔ ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j))
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mp
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : ↑Y
⊢ x ∈ ⇑(ConcreteCategory.hom (pullback.snd f g)) '' ⇑(ConcreteCategory.hom (pullback.fst f g)) ⁻¹' U →
    x ∈ ⇑(ConcreteCategory.hom g) ⁻¹' ⇑(ConcreteCategory.hom f) '' U

Tactic:
rintro ⟨y, hy, rfl⟩
    exact
      ⟨(pullback.fst f g) y, hy, CategoryTheory.congr_fun pullback.condition y⟩

Goal state after: