mathlib-initiative/mathlib-tactics huggingface dataset:
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)
f : M₁ ⟶ M₂
g : M₃ ⟶ M₄
X Y : Cᵒᵖ
φ : X ⟶ Y
m₁ : ↑(M₁.obj X)
m₃ : ↑(M₃.obj X)
⊢ (ConcreteCategory.hom (f.app Y ⊗ₘ g.app Y)) ((ModuleCat.Hom.hom ((tensorObj M₁ M₃).map φ)) (m₁ ⊗ₜ[↑(R.obj X)] m₃)) =
    (ModuleCat.Hom.hom ((tensorObj M₂ M₄).map φ)) ((ModuleCat.Hom.hom (f.app X ⊗ₘ g.app X)) (m₁ ⊗ₜ[↑(R.obj X)] m₃))

Tactic:
tensorObj_map_tmul

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)
f : M₁ ⟶ M₂
g : M₃ ⟶ M₄
X Y : Cᵒᵖ
φ : X ⟶ Y
m₁ : ↑(M₁.obj X)
m₃ : ↑(M₃.obj X)
⊢ (ConcreteCategory.hom (f.app Y ⊗ₘ g.app Y))
      ((ConcreteCategory.hom (M₁.map φ)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₃.map φ)) m₃) =
    (ModuleCat.Hom.hom ((tensorObj M₂ M₄).map φ)) ((ModuleCat.Hom.hom (f.app X ⊗ₘ g.app X)) (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)
f : M₁ ⟶ M₂
g : M₃ ⟶ M₄
X Y : Cᵒᵖ
φ : X ⟶ Y
m₁ : ↑(M₁.obj X)
m₃ : ↑(M₃.obj X)
⊢ (ConcreteCategory.hom (f.app Y)) ((ConcreteCategory.hom (M₁.map φ)) m₁) ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)]
      (ConcreteCategory.hom (g.app Y)) ((ConcreteCategory.hom (M₃.map φ)) m₃) =
    (ModuleCat.Hom.hom ((tensorObj M₂ M₄).map φ)) ((ModuleCat.Hom.hom (f.app X ⊗ₘ g.app X)) (m₁ ⊗ₜ[↑(R.obj X)] m₃))

Tactic:
tensorObj_map_tmul

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)
f : M₁ ⟶ M₂
g : M₃ ⟶ M₄
X Y : Cᵒᵖ
φ : X ⟶ Y
m₁ : ↑(M₁.obj X)
m₃ : ↑(M₃.obj X)
⊢ (ConcreteCategory.hom (f.app Y)) ((ConcreteCategory.hom (M₁.map φ)) m₁) ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)]
      (ConcreteCategory.hom (g.app Y)) ((ConcreteCategory.hom (M₃.map φ)) m₃) =
    (ConcreteCategory.hom (M₂.map φ)) ((ModuleCat.Hom.hom (f.app X)) (m₁, m₃).1) ⊗ₜ[↑(R.obj Y)]
      (ConcreteCategory.hom (M₄.map φ)) ((ModuleCat.Hom.hom (g.app X)) (m₁, m₃).2)
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₃ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝² x✝¹ : Cᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ∀ (m₁ : ↑(M₁.obj x✝²)) (m₂ : ↑(M₂.obj x✝²)) (m₃ : ↑(M₃.obj x✝²)),
    (ConcreteCategory.hom
          ((Monoidal.tensorObj (Monoidal.tensorObj M₁ M₂) M₃).map x✝ ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map x✝))).map
              (α_ (M₁.obj x✝¹) (M₂.obj x✝¹) (M₃.obj x✝¹)).hom))
        (m₁ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj x✝²)] m₂ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj x✝²)] m₃) =
      (ConcreteCategory.hom
          ((α_ (M₁.obj x✝²) (M₂.obj x✝²) (M₃.obj x✝²)).hom ≫ (Monoidal.tensorObj M₁ (Monoidal.tensorObj M₂ M₃)).map x✝))
        (m₁ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj x✝²)] m₂ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj x✝²)] m₃)

Tactic:
by intros; rfl

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

Goal state before:
pp: case refine_1
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
⊢ IsIso (f ≫ g)

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:
· infer_instance

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
⊢ (Presieve.singleton g).bind Ti = Presieve.singleton (f ≫ g)
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
Fs : S.arrows.cocone.pt ⟶ s.pt
HFs : ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j
H : ∃! t, (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation t
⊢ (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation Fs

Tactic:
exact fun _ f hf => HFs ⟨Over.mk f, hf⟩

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : Nonempty (IsColimit S.arrows.cocone)
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
⊢ x.Compatible → ∃! t, x.IsAmalgamation t

Tactic:
hx

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : Nonempty (IsColimit S.arrows.cocone)
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
⊢ Nonempty (IsColimit S.arrows.cocone) → ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows

Tactic:
intro H W x hx

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : Nonempty (IsColimit S.arrows.cocone)
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
Z : C
v : Z ⟶ B
⊢ ⟨Z, v⟩ ∈ (fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) '' s.uncurry →
    ⟨Z, v⟩ ∈ (pullbackArrows b s).uncurry

Tactic:
rintro ⟨⟨Y, u⟩, hu, h⟩

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
Z : C
v : Z ⟶ B
Y : C
u : Y ⟶ X
hu : ⟨Y, u⟩ ∈ s.uncurry
h : (fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩ = ⟨Z, v⟩
⊢ ⟨Z, v⟩ ∈ (pullbackArrows b s).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (ofArrows Y f).uncurry ↔ ⟨Z, v⟩ ∈ Set.range fun i ↦ ⟨Y i, f i⟩

Tactic:
simp only [Set.mem_range, Sigma.mk.injEq]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (ofArrows Y f).uncurry ↔ ∃ y, Y y = Z ∧ f y ≍ v
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
h : ⊤ = ⊥
⊢ False

Tactic:
simp [← bot_apply (𝟙 X), ← h]

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hu : ∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone S.arrows.cocone.op))
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
⊢ x.SieveCompatible → ∃! t, x.IsAmalgamation t

Tactic:
hx

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hu : ∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone S.arrows.cocone.op))
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
hx : x.SieveCompatible
⊢ ∃! t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
z :
  (∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂) ∧
    (x.Compatible → ∃ t, x.IsAmalgamation t)
⊢ x.Compatible → ∃! t, x.IsAmalgamation t

Tactic:
hx

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
z :
  (∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂) ∧
    (x.Compatible → ∃ t, x.IsAmalgamation t)
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P (generate R).arrows
⊢ x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
hx

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P (generate R).arrows
hx : x.Compatible
⊢ ∃ t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P R
⊢ x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
hx

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P R
hx : x.Compatible
⊢ ∃ t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
⊢ x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
hx

Goal state after:
case right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible
⊢ ∃ t, x.IsAmalgamation t
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
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
⊢ x.Compatible → ∃! t, x.IsAmalgamation t

Tactic:
hx

Goal state after:
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, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case h.right.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
b : T.shape.R
⊢ e ≫ (T.multifork P).π.app (WalkingMulticospan.right b) = K.π.app (WalkingMulticospan.right b)

Tactic:
· rw [← K.w (WalkingMulticospan.Hom.fst b), ←
        (T.multifork P).w (WalkingMulticospan.Hom.fst b), ← assoc]
      congr 1
      apply he

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

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.plusObj P ⟶ Q
hγ : J.toPlus P ≫ γ = η
⊢ γ = J.plusLift η hQ

Tactic:
dsimp only [plusLift]
  rw [Iso.eq_comp_inv, ← hγ, plusMap_comp]
  simp

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

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
i : C
x : F.obj i
⊢ x ∈ G.obj i → x ∈ ((G.preimage p).image p).obj i

Tactic:
hx

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
i : C
x : F.obj i
hx : x ∈ G.obj i
⊢ x ∈ ((G.preimage p).image p).obj i
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
A' : Type u₂
inst✝⁵ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P✝ : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
inst✝³ : HasProducts A
inst✝² : HasProducts A'
inst✝¹ : HasPullbacks C
P : Cᵒᵖ ⥤ A
s : A ⥤ Type (max v₁ u₁)
inst✝ : ∀ (J : Type (max v₁ u₁)), PreservesLimitsOfShape (Discrete J) s
U : C
R : Presieve U
e : parallelPair (s.map (firstMap R P)) (s.map (secondMap R P)) ≅
  parallelPair (Equalizer.Presieve.firstMap (P ⋙ s) R) (Equalizer.Presieve.secondMap (P ⋙ s) R) :=
  parallelPair.ext (PreservesProduct.iso s fun f ↦ P.obj (op f.fst))
    (PreservesProduct.iso s fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) ⋯ ⋯
⊢ (Iso.refl ((Cone.postcompose e.hom).obj (Fork.ofι (s.map (forkMap R P)) ⋯)).pt).hom ≫
      (Fork.ofι (Equalizer.forkMap (P ⋙ s) R) ⋯).ι =
    Fork.ι ((Cone.postcompose e.hom).obj (Fork.ofι (s.map (forkMap R P)) ⋯))

Tactic:
dsimp [Equalizer.forkMap, forkMap, e, Fork.ι]

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁶ : Category.{v₂, u₂} A
A' : Type u₂
inst✝⁵ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P✝ : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
inst✝³ : HasProducts A
inst✝² : HasProducts A'
inst✝¹ : HasPullbacks C
P : Cᵒᵖ ⥤ A
s : A ⥤ Type (max v₁ u₁)
inst✝ : ∀ (J : Type (max v₁ u₁)), PreservesLimitsOfShape (Discrete J) s
U : C
R : Presieve U
e : parallelPair (s.map (firstMap R P)) (s.map (secondMap R P)) ≅
  parallelPair (Equalizer.Presieve.firstMap (P ⋙ s) R) (Equalizer.Presieve.secondMap (P ⋙ s) R) :=
  parallelPair.ext (PreservesProduct.iso s fun f ↦ P.obj (op f.fst))
    (PreservesProduct.iso s fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) ⋯ ⋯
⊢ (𝟙 (s.obj (P.obj (op U))) ≫ Pi.lift fun f ↦ s.map (P.map (↑f.snd).op)) =
    s.map (Pi.lift fun f ↦ P.map (↑f.snd).op) ≫ piComparison s fun f ↦ P.obj (op f.fst)
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
B : Type u₃
inst✝³ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝² : HasLimitsOfSize.{v₁, max v₁ u₁, v₂, u₂} A
inst✝¹ : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
inst✝ : s.ReflectsIsomorphisms
⊢ IsSheaf J P ↔ IsSheaf J (P ⋙ s)

Tactic:
let : ReflectsLimitsOfSize s := reflectsLimits_of_reflectsIsomorphisms
  exact ⟨isSheaf_comp_of_isSheaf J P s, isSheaf_of_isSheaf_comp J P s⟩

Goal state after:
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
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
⊢ x''.Compatible

Tactic:
intro V₁ V₂ V₃ g₁ g₂ g₃ g₄ S₁ S₂ e

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
S₁ : S'.arrows g₃
S₂ : S'.arrows g₄
e : g₁ ≫ g₃ = g₂ ≫ g₄
⊢ (ConcreteCategory.hom (F.map g₁.op)) (x'' g₃ S₁) = (ConcreteCategory.hom (F.map g₂.op)) (x'' g₄ S₂)
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:
by
        rintro Y f ⟨Z, e1, e2, he2, he1, hee⟩
        rw [← hee]
        apply leOfHom (h1 ⟨_, _, he2⟩)
        exact he1

Goal state after:
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
⊢ x ∈ (sheafify J G).obj U → x ∈ G'.obj U

Tactic:
hx

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
⊢ x ∈ G'.obj U
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: case e_a
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) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
x✝ : Cᵒᵖ
a : ⊤.shape.L
⊢ (F.map (⊤.toMultiequalizer P) ≫ (J.diagramCompIso F P (unop x✝)).hom.app (op ⊤)) ≫
      Multiequalizer.ι (⊤.index (P ⋙ F)) a =
    ⊤.toMultiequalizer (P ⋙ F) ≫ Multiequalizer.ι (⊤.index (P ⋙ F)) a

Tactic:
rw [Category.assoc, diagramCompIso_hom_ι, ← F.map_comp]

Goal state after:
case e_a
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) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
x✝ : Cᵒᵖ
a : ⊤.shape.L
⊢ F.map (⊤.toMultiequalizer P ≫ Multiequalizer.ι ((unop (op ⊤)).index P) a) =
    ⊤.toMultiequalizer (P ⋙ F) ≫ Multiequalizer.ι (⊤.index (P ⋙ F)) a
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
a✝ : HasLimit F
⊢ HasLimit (F ⋙ forget)

pp: case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
a✝ : HasLimit (F ⋙ forget)
⊢ HasLimit F

Tactic:
· infer_instance

Goal state after:
case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
a✝ : HasLimit (F ⋙ forget)
⊢ HasLimit 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
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
⊢ J.toSheafify P ≫ γ = η → γ = J.sheafifyLift η hQ

Tactic:
intro h
  apply plusLift_unique
  apply plusLift_unique
  rw [← Category.assoc, ← plusMap_toPlus]
  exact h

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
η γ : J.sheafify P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toSheafify P ≫ η = J.toSheafify P ≫ γ
⊢ η = γ

Tactic:
apply J.plus_hom_ext _ _ hQ

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 (J.plusObj P) ≫ η = J.toPlus (J.plusObj P) ≫ γ