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
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝³ : X₁✝ ⟶ Y₁✝
x✝² : X₂✝ ⟶ Y₂✝
x✝¹ : Y₁✝ ⟶ Z₁✝
x✝ : Y₂✝ ⟶ Z₂✝
X✝ : Cᵒᵖ
⊢ ((x✝³ ⊗ₘ x✝²) ≫ (x✝¹ ⊗ₘ x✝)).app X✝ = (x✝³ ≫ x✝¹ ⊗ₘ x✝² ≫ x✝).app X✝

Tactic:
apply tensorHom_comp_tensorHom

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
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝² : X₁✝ ⟶ Y₁✝
x✝¹ : X₂✝ ⟶ Y₂✝
x✝ : X₃✝ ⟶ Y₃✝
X✝ : Cᵒᵖ
⊢ (((x✝² ⊗ₘ x✝¹) ⊗ₘ x✝) ≫ (α_ Y₁✝ Y₂✝ Y₃✝).hom).app X✝ = ((α_ X₁✝ X₂✝ X₃✝).hom ≫ (x✝² ⊗ₘ x✝¹ ⊗ₘ x✝)).app X✝

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝² : X₁✝ ⟶ Y₁✝
x✝¹ : X₂✝ ⟶ Y₂✝
x✝ : X₃✝ ⟶ Y₃✝
X✝ : Cᵒᵖ
⊢ (((x✝² ⊗ₘ x✝¹) ⊗ₘ x✝) ≫ (α_ Y₁✝ Y₂✝ Y₃✝).hom).app X✝ = ((α_ X₁✝ X₂✝ X₃✝).hom ≫ (x✝² ⊗ₘ x✝¹ ⊗ₘ x✝)).app X✝
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
X✝¹ Y✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : X✝¹ ⟶ Y✝
X✝ : Cᵒᵖ
⊢ (𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)) ◁ x✝ ≫ (λ_ Y✝).hom).app X✝ = ((λ_ X✝¹).hom ≫ x✝).app X✝

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X✝¹ Y✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : X✝¹ ⟶ Y✝
X✝ : Cᵒᵖ
⊢ (𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)) ◁ x✝ ≫ (λ_ Y✝).hom).app X✝ = ((λ_ X✝¹).hom ≫ x✝).app X✝
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
X✝¹ Y✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : X✝¹ ⟶ Y✝
X✝ : Cᵒᵖ
⊢ (x✝ ▷ 𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)) ≫ (ρ_ Y✝).hom).app X✝ = ((ρ_ X✝¹).hom ≫ x✝).app X✝

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X✝¹ Y✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : X✝¹ ⟶ Y✝
X✝ : Cᵒᵖ
⊢ (x✝ ▷ 𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)) ≫ (ρ_ Y✝).hom).app X✝ = ((ρ_ X✝¹).hom ≫ x✝).app X✝
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
x✝³ x✝² x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ : Cᵒᵖ
⊢ ((α_ x✝³ x✝² x✝¹).hom ▷ x✝ ≫ (α_ x✝³ (x✝² ⊗ x✝¹) x✝).hom ≫ x✝³ ◁ (α_ x✝² x✝¹ x✝).hom).app X✝ =
    ((α_ (x✝³ ⊗ x✝²) x✝¹ x✝).hom ≫ (α_ x✝³ x✝² (x✝¹ ⊗ x✝)).hom).app X✝

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
x✝³ x✝² x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ : Cᵒᵖ
⊢ ((α_ x✝³ x✝² x✝¹).hom ▷ x✝ ≫ (α_ x✝³ (x✝² ⊗ x✝¹) x✝).hom ≫ x✝³ ◁ (α_ x✝² x✝¹ x✝).hom).app X✝ =
    ((α_ (x✝³ ⊗ x✝²) x✝¹ x✝).hom ≫ (α_ x✝³ x✝² (x✝¹ ⊗ x✝)).hom).app X✝
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
x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ : Cᵒᵖ
⊢ ((α_ x✝¹ (𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat))) x✝).hom ≫ x✝¹ ◁ (λ_ x✝).hom).app X✝ =
    ((ρ_ x✝¹).hom ▷ x✝).app X✝

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ : Cᵒᵖ
⊢ ((α_ x✝¹ (𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat))) x✝).hom ≫ x✝¹ ◁ (λ_ x✝).hom).app X✝ =
    ((ρ_ x✝¹).hom ▷ x✝).app X✝
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
R : Presieve X
hR : R ∈ {R | Sieve.generate R ∈ J X}
⊢ pullbackArrows f R ∈ {R | Sieve.generate R ∈ J Y}

Tactic:
simpa [Sieve.pullbackArrows_comm] using J.pullback_stable f hR

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

Goal state before:
pp: case mk
C : Type u
inst✝ : Category.{v, u} C
J₂ : GrothendieckTopology C
sieves✝ : (X : C) → Set (Sieve X)
top_mem'✝ : ∀ (X : C), ⊤ ∈ sieves✝ X
pullback_stable'✝ : ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X), S ∈ sieves✝ X → Sieve.pullback f S ∈ sieves✝ Y
transitive'✝ :
  ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ sieves✝ X →
      ∀ (R : Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves✝ Y) → R ∈ sieves✝ X
h :
  (fun J X ↦ J.sieves X)
      { sieves := sieves✝, top_mem' := top_mem'✝, pullback_stable' := pullback_stable'✝, transitive' := transitive'✝ } =
    (fun J X ↦ J.sieves X) J₂
⊢ { sieves := sieves✝, top_mem' := top_mem'✝, pullback_stable' := pullback_stable'✝, transitive' := transitive'✝ } = J₂

Tactic:
;

Goal state after:
case mk
C : Type u
inst✝ : Category.{v, u} C
J₂ : GrothendieckTopology C
sieves✝ : (X : C) → Set (Sieve X)
top_mem'✝ : ∀ (X : C), ⊤ ∈ sieves✝ X
pullback_stable'✝ : ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X), S ∈ sieves✝ X → Sieve.pullback f S ∈ sieves✝ Y
transitive'✝ :
  ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ sieves✝ X →
      ∀ (R : Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves✝ Y) → R ∈ sieves✝ X
h :
  (fun J X ↦ J.sieves X)
      { sieves := sieves✝, top_mem' := top_mem'✝, pullback_stable' := pullback_stable'✝, transitive' := transitive'✝ } =
    (fun J X ↦ J.sieves X) J₂
⊢ { sieves := sieves✝, top_mem' := top_mem'✝, pullback_stable' := pullback_stable'✝, transitive' := transitive'✝ } = J₂
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: case mk.mk
C : Type u
inst✝ : Category.{v, u} C
sieves✝¹ : (X : C) → Set (Sieve X)
top_mem'✝¹ : ∀ (X : C), ⊤ ∈ sieves✝¹ X
pullback_stable'✝¹ : ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X), S ∈ sieves✝¹ X → Sieve.pullback f S ∈ sieves✝¹ Y
transitive'✝¹ :
  ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ sieves✝¹ X →
      ∀ (R : Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves✝¹ Y) → R ∈ sieves✝¹ X
sieves✝ : (X : C) → Set (Sieve X)
top_mem'✝ : ∀ (X : C), ⊤ ∈ sieves✝ X
pullback_stable'✝ : ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X), S ∈ sieves✝ X → Sieve.pullback f S ∈ sieves✝ Y
transitive'✝ :
  ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ sieves✝ X →
      ∀ (R : Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves✝ Y) → R ∈ sieves✝ X
h :
  (fun J X ↦ J.sieves X)
      { sieves := sieves✝¹, top_mem' := top_mem'✝¹, pullback_stable' := pullback_stable'✝¹,
        transitive' := transitive'✝¹ } =
    (fun J X ↦ J.sieves X)
      { sieves := sieves✝, top_mem' := top_mem'✝, pullback_stable' := pullback_stable'✝, transitive' := transitive'✝ }
⊢ { sieves := sieves✝¹, top_mem' := top_mem'✝¹, pullback_stable' := pullback_stable'✝¹, transitive' := transitive'✝¹ } =
    { sieves := sieves✝, top_mem' := top_mem'✝, pullback_stable' := pullback_stable'✝, transitive' := transitive'✝ }

Tactic:
;

Goal state after:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
sieves✝¹ : (X : C) → Set (Sieve X)
top_mem'✝¹ : ∀ (X : C), ⊤ ∈ sieves✝¹ X
pullback_stable'✝¹ : ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X), S ∈ sieves✝¹ X → Sieve.pullback f S ∈ sieves✝¹ Y
transitive'✝¹ :
  ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ sieves✝¹ X →
      ∀ (R : Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves✝¹ Y) → R ∈ sieves✝¹ X
sieves✝ : (X : C) → Set (Sieve X)
top_mem'✝ : ∀ (X : C), ⊤ ∈ sieves✝ X
pullback_stable'✝ : ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X), S ∈ sieves✝ X → Sieve.pullback f S ∈ sieves✝ Y
transitive'✝ :
  ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ sieves✝ X →
      ∀ (R : Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves✝ Y) → R ∈ sieves✝ X
h :
  (fun J X ↦ J.sieves X)
      { sieves := sieves✝¹, top_mem' := top_mem'✝¹, pullback_stable' := pullback_stable'✝¹,
        transitive' := transitive'✝¹ } =
    (fun J X ↦ J.sieves X)
      { sieves := sieves✝, top_mem' := top_mem'✝, pullback_stable' := pullback_stable'✝, transitive' := transitive'✝ }
⊢ { sieves := sieves✝¹, top_mem' := top_mem'✝¹, pullback_stable' := pullback_stable'✝¹, transitive' := transitive'✝¹ } =
    { sieves := sieves✝, top_mem' := top_mem'✝, pullback_stable' := pullback_stable'✝, transitive' := transitive'✝ }
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
i : X ⟶ Y
inst✝ : IsIso i
S : Sieve Y
H : Sieve.pullback i S ∈ J X
⊢ S = Sieve.pullback (𝟙 Y) S

Tactic:
Sieve.pullback_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
i : X ⟶ Y
inst✝ : IsIso i
S : Sieve Y
H : Sieve.pullback i S ∈ J X
⊢ S = S
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: case refine_2
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ (↾fun i ↦ Classical.choose ⋯) ≫ (Fork.ofι f w).ι = s.ι

pp: case refine_3
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ ∀ {m : s.pt ⟶ (Fork.ofι f w).pt}, m ≫ (Fork.ofι f w).ι = s.ι → m = ↾fun i ↦ Classical.choose ⋯

Tactic:
· ext i
      exact (Classical.choose_spec (t (s.ι i) (congr_hom s.condition i))).1

Goal state after:
case refine_3
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ ∀ {m : s.pt ⟶ (Fork.ofι f w).pt}, m ≫ (Fork.ofι f w).ι = s.ι → m = ↾fun i ↦ Classical.choose ⋯
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : (hom g) y = (hom h) y
y' : PUnit.{u + 1} ⟶ Y := ↾fun x ↦ y
x✝ : PUnit.{u + 1}
⊢ (hom (y' ≫ g)).toFun x✝ = (hom (y' ≫ h)).toFun x✝

Tactic:
;

Goal state after:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : (hom g) y = (hom h) y
y' : PUnit.{u + 1} ⟶ Y := ↾fun x ↦ y
x✝ : PUnit.{u + 1}
⊢ (hom (y' ≫ g)).toFun x✝ = (hom (y' ≫ h)).toFun x✝
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
x : { x // (hom g) x = (hom h) x }
⊢ (hom (↾Subtype.val ≫ g)).toFun x = (hom (↾Subtype.val ≫ h)).toFun x

Tactic:
;

Goal state after:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
x : { x // (hom g) x = (hom h) x }
⊢ (hom (↾Subtype.val ≫ g)).toFun x = (hom (↾Subtype.val ≫ h)).toFun x
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
s : Fork g h
m✝ : s.pt ⟶ (Fork.ofι (↾Subtype.val) ⋯).pt
hm : m✝ ≫ (Fork.ofι (↾Subtype.val) ⋯).ι = s.ι
x : s.pt
⊢ (hom m✝).toFun x = (hom (↾fun i ↦ ⟨(hom s.ι) i, ⋯⟩)).toFun x

Tactic:
;

Goal state after:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
s : Fork g h
m✝ : s.pt ⟶ (Fork.ofι (↾Subtype.val) ⋯).pt
hm : m✝ ≫ (Fork.ofι (↾Subtype.val) ⋯).ι = s.ι
x : s.pt
⊢ (hom m✝).toFun x = (hom (↾fun i ↦ ⟨(hom s.ι) i, ⋯⟩)).toFun x
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (singleton u).uncurry ↔ ⟨Z, v⟩ ∈ {⟨Y, u⟩}

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (singleton u).uncurry ↔ ⟨Z, v⟩ ∈ {⟨Y, u⟩}
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
v : Z ⟶ X
Y : C
⊢ ⟨Z, v⟩ ∈ {⟨⟨Z, v⟩.fst, ⟨Z, v⟩.snd⟩}

Tactic:
;

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
v : Z ⟶ X
Y : C
⊢ ⟨Z, v⟩ ∈ {⟨⟨Z, v⟩.fst, ⟨Z, v⟩.snd⟩}
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
v : Z ⟶ X
u : ⟨Z, v⟩.fst ⟶ X
h : ⟨Z, v⟩.snd ≍ ⟨⟨Z, v⟩.fst, u⟩.snd
⊢ ⟨Z, v⟩ ∈ (singleton u).uncurry

Tactic:
;

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
v : Z ⟶ X
u : ⟨Z, v⟩.fst ⟶ X
h : ⟨Z, v⟩.snd ≍ ⟨⟨Z, v⟩.fst, u⟩.snd
⊢ ⟨Z, v⟩ ∈ (singleton u).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (singleton ⟨Z, v⟩.snd).uncurry

Tactic:
;

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (singleton ⟨Z, v⟩.snd).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: 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⟩ ∈ (pullbackArrows b s).uncurry ↔
    ⟨Z, v⟩ ∈ (fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) '' s.uncurry

Tactic:
;

Goal state after:
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⟩ ∈ (pullbackArrows b s).uncurry ↔
    ⟨Z, v⟩ ∈ (fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) '' s.uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
Y✝ Y : C
u : Y ⟶ X
hu : s u
⊢ ⟨(limit.cone (cospan u b)).1, (limit.cone (cospan u b)).π.1 WalkingCospan.right⟩ ∈
    (fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) '' s.uncurry

Tactic:
;

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
Y✝ Y : C
u : Y ⟶ X
hu : s u
⊢ ⟨(limit.cone (cospan u b)).1, (limit.cone (cospan u b)).π.1 WalkingCospan.right⟩ ∈
    (fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) '' s.uncurry
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
Y : C
u : Y ⟶ X
hu : ⟨Y, u⟩ ∈ s.uncurry
v : ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst ⟶ B
h :
  ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).snd =
    ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst, v⟩.snd
⊢ ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst, v⟩ ∈ (pullbackArrows b s).uncurry

Tactic:
;

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
Y : C
u : Y ⟶ X
hu : ⟨Y, u⟩ ∈ s.uncurry
v : ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst ⟶ B
h :
  ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).snd =
    ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst, v⟩.snd
⊢ ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst, v⟩ ∈ (pullbackArrows b s).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (s.bind t).uncurry ↔
    ⟨Z, v⟩ ∈ ⋃ i, ⋃ (h : i ∈ s.uncurry), (Sigma.map id fun Z g ↦ g ≫ i.snd) '' (t i.snd h).uncurry

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (s.bind t).uncurry ↔
    ⟨Z, v⟩ ∈ ⋃ i, ⋃ (h : i ∈ s.uncurry), (Sigma.map id fun Z g ↦ g ≫ i.snd) '' (t i.snd h).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (s.bind t).uncurry ↔
    ∃ i, ∃ (h : i ∈ s.uncurry), ∃ x ∈ (t i.snd ⋯).uncurry, Sigma.map id (fun Z g ↦ g ≫ i.snd) x = ⟨Z, v⟩

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (s.bind t).uncurry ↔
    ∃ i, ∃ (h : i ∈ s.uncurry), ∃ x ∈ (t i.snd ⋯).uncurry, Sigma.map id (fun Z g ↦ g ≫ i.snd) x = ⟨Z, v⟩
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
fst✝ : C
f : fst✝ ⟶ X
hf : ⟨fst✝, f⟩ ∈ s.uncurry
Y : C
g : Y ⟶ ⟨fst✝, f⟩.fst
hg : ⟨Y, g⟩ ∈ (t ⟨fst✝, f⟩.snd ⋯).uncurry
v : (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst ⟶ X
h :
  (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).snd =
    ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, v⟩.snd
⊢ ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, v⟩ ∈ (s.bind t).uncurry

Tactic:
;

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
fst✝ : C
f : fst✝ ⟶ X
hf : ⟨fst✝, f⟩ ∈ s.uncurry
Y : C
g : Y ⟶ ⟨fst✝, f⟩.fst
hg : ⟨Y, g⟩ ∈ (t ⟨fst✝, f⟩.snd ⋯).uncurry
v : (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst ⟶ X
h :
  (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).snd =
    ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, v⟩.snd
⊢ ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, v⟩ ∈ (s.bind t).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:
;

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 ↔ ⟨Z, v⟩ ∈ Set.range fun i ↦ ⟨Y i, f i⟩
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 ↔ ∃ y, Y y = Z ∧ f y ≍ v

Tactic:
;

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: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y✝ : ι → C
f : (i : ι) → Y✝ i ⟶ X
Y : C
i : ι
⊢ ∃ y, Y✝ y = Y✝ i ∧ f y ≍ f i

Tactic:
;

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y✝ : ι → C
f : (i : ι) → Y✝ i ⟶ X
Y : C
i : ι
⊢ ∃ y, Y✝ y = Y✝ i ∧ f y ≍ f i
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
v : Y i ⟶ X
h : f i ≍ v
⊢ ⟨Y i, v⟩ ∈ (ofArrows Y f).uncurry

Tactic:
;

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
v : Y i ⟶ X
h : f i ≍ v
⊢ ⟨Y i, v⟩ ∈ (ofArrows Y f).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
v : Y i ⟶ X
h : f i ≍ v
⊢ ⟨Y i, f i⟩ ∈ (ofArrows Y f).uncurry

Tactic:
;

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
v : Y i ⟶ X
h : f i ≍ v
⊢ ⟨Y i, f i⟩ ∈ (ofArrows Y f).uncurry
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S : Sieve X✝
R : Presieve X✝
X Y : C
f : X ⟶ Y
x : P.obj (op X)
⊢ X = X

Tactic:
;

Goal state after:
case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S : Sieve X✝
R : Presieve X✝
X Y : C
f : X ⟶ Y
x : P.obj (op X)
⊢ X = X
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝¹ : C
S : Sieve X✝
R : Presieve X✝
X Y✝ : C
f : X ⟶ Y✝
x : FamilyOfElements P (singleton f)
Y : C
⊢ (fun x Z g hg ↦ (ConcreteCategory.hom (P.map (eqToHom ⋯).op)) x) ((fun x ↦ x f ⋯) x) X f ⋯ = x f ⋯

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝¹ : C
S : Sieve X✝
R : Presieve X✝
X Y✝ : C
f : X ⟶ Y✝
x : FamilyOfElements P (singleton f)
Y : C
⊢ (fun x Z g hg ↦ (ConcreteCategory.hom (P.map (eqToHom ⋯).op)) x) ((fun x ↦ x f ⋯) x) X f ⋯ = x f ⋯
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
s : Presieve X
Z Y : D
Y✝ : C
u✝ : Y✝ ⟶ X
hu : s u✝
w✝ : Z ⟶ F.obj Y✝
⊢ Presieve.functorPushforward F s (w✝ ≫ F.map u✝)

Tactic:
;

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
s : Presieve X
Z Y : D
Y✝ : C
u✝ : Y✝ ⟶ X
hu : s u✝
w✝ : Z ⟶ F.obj Y✝
⊢ Presieve.functorPushforward F s (w✝ ≫ F.map u✝)
Module: Mathlib.CategoryTheory.Sites.Sieves

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
X : C
s : Presieve X
Z : D
w✝² : C
w✝¹ : w✝² ⟶ X
w✝ : Z ⟶ F.obj w✝²
hu : s w✝¹
⊢ (generate (Presieve.map F s)).arrows (w✝ ≫ F.map w✝¹)

Tactic:
;

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
s : Presieve X
Z : D
w✝² : C
w✝¹ : w✝² ⟶ X
w✝ : Z ⟶ F.obj w✝²
hu : s w✝¹
⊢ (generate (Presieve.map F s)).arrows (w✝ ≫ F.map w✝¹)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
R : Sieve Z
W : C
h : W ⟶ X
x✝ : (pushforward f (pushforward g R)).arrows h
y : W ⟶ Y
hy : y ≫ f = h
z : W ⟶ Z
hR : z ≫ g = y
hz : R.arrows z
⊢ y ≫ f = h ∧ R.arrows z

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
R : Sieve Z
W : C
h : W ⟶ X
x✝ : (pushforward f (pushforward g R)).arrows h
y : W ⟶ Y
hy : y ≫ f = h
z : W ⟶ Z
hR : z ≫ g = y
hz : R.arrows z
⊢ y ≫ f = h ∧ R.arrows z
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
a : Presieve.FamilyOfElements P S.arrows
| (firstObjEqFamily P S.arrows).toEquiv.symm a

Tactic:
;

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

Tactic:
apply existsUnique_congr

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

Tactic:
;

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
a : Presieve.FamilyOfElements P R
| (ConcreteCategory.hom (firstObjEqFamily P R).hom) ((firstObjEqFamily P R).toEquiv.symm a)