mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT S.X₂ n
h₃ : HasInjectiveDimensionLT S.X₁ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
⊢ ∀ ⦃Y : C⦄ (e : Ext Y S.X₃ i), e = 0

Tactic:
Y

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT S.X₂ n
h₃ : HasInjectiveDimensionLT S.X₁ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
⊢ ∀ (e : Ext Y S.X₃ i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
d : ℕ
⊢ ∀ ⦃Y : C⦄ (e : Ext Y X d) (k : ℕ), d = n + k → e = 0

Tactic:
Y

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
d : ℕ
Y : C
⊢ ∀ (e : Ext Y X d) (k : ℕ), d = n + k → e = 0
Module: Mathlib.Algebra.Category.ModuleCat.LeftResolution

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M N : ModuleCat R
f : (free R).obj X ⟶ N
p : M ⟶ N
hp : Function.Surjective ⇑(ConcreteCategory.hom p)
⊢ ∃ f', f' ≫ p = f

Tactic:
obtain ⟨s, hs⟩ := hp.hasRightInverse

Goal state after:
R : Type u
inst✝ : Ring R
X : Type u
M N : ModuleCat R
f : (free R).obj X ⟶ N
p : M ⟶ N
hp : Function.Surjective ⇑(ConcreteCategory.hom p)
s : ↑N → ↑M
hs : Function.RightInverse s ⇑(ConcreteCategory.hom p)
⊢ ∃ f', f' ≫ p = f
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)) = ⋀[R]^n M

Tactic:
apply le_antisymm
  · rw [Submodule.span_le, Set.range_subset_iff]
    intro
    rw [SetLike.mem_coe, ιMulti_family_eq_coe_comp, comp_apply]
    exact Submodule.coe_mem _
  · rw [← ιMulti_span_fixedDegree_of_span_eq_top R n M hv, Submodule.span_le]
    rintro - ⟨f, ⟨f_range, rfl⟩⟩
    rw [Set.mem_ofPred] at f_range
    obtain ⟨α, rfl⟩ := Set.range_subset_range_iff_exists_comp.mp f_range
    exact ιMulti_family_span_fixedDegree_aux R v α

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
this : Algebra R S := f.toAlgebra
⊢ (ConcreteCategory.hom (↟↑(AlgebraTensorModule.rid R S S))) (1 ⊗ₜ[R] r) = f r

Tactic:
erw [AlgebraTensorModule.rid_tmul]

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
this : Algebra R S := f.toAlgebra
⊢ r • 1 = f r
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ ((F.obj j).map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((F.obj j).map g) ≫
          (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                  (RingCat.Hom.hom (R.map (f ≫ g))) ⋯).inv.app
            ((F.obj j).obj Z)) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))).map (colimit.ι (F ⋙ evaluation R Z) j) =
    (F.whiskerLeft (restriction R f)).app j ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
          ((F.whiskerLeft (restriction R g)).app j ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (colimit.ι (F ⋙ evaluation R Z) j)) ≫
        (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
            (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))).inv

Tactic:
ModuleCat.restrictScalarsComp'_inv_app,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ ((F.obj j).map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((F.obj j).map g) ≫
          (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
              (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ ((F.obj j).obj Z)).inv) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))).map (colimit.ι (F ⋙ evaluation R Z) j) =
    (F.whiskerLeft (restriction R f)).app j ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
          ((F.whiskerLeft (restriction R g)).app j ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (colimit.ι (F ⋙ evaluation R Z) j)) ≫
        (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
            (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))).inv
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G F'✝ G' : C ⥤ D
α : F ⟶ G
β : F'✝ ⟶ G'
F' : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ α.app Y ▷ F'.obj Y = α.app X ▷ F'.obj X ≫ (tensorObj G F').map f

Tactic:
by
    simp only [← tensorHom_id]
    apply (tensorHom α (𝟙 F')).naturality

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsConnected C
s : Cocone (constPUnitFunctor C)
j X : C
⊢ ∀ (j₂ : C) (x : X ⟶ j₂),
    (ConcreteCategory.hom (s.ι.app X)) PUnit.unit = (ConcreteCategory.hom (s.ι.app j₂)) PUnit.unit

Tactic:
Y

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsConnected C
s : Cocone (constPUnitFunctor C)
j X Y : C
⊢ ∀ (x : X ⟶ Y), (ConcreteCategory.hom (s.ι.app X)) PUnit.unit = (ConcreteCategory.hom (s.ι.app Y)) PUnit.unit
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: case h.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
X : StructuredArrow (c₁, c₂) (Functor.diag C)
⊢ [c₁, X.right, c₂].getLast ⋯ = c₂

Tactic:
· rfl

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

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
⊢ limit G ≅ limit (curry.obj G ⋙ lim)

Tactic:
by
  have i : G ≅ uncurry.obj ((@curry J _ K _ C _).obj G) := currying.symm.unitIso.app G
  haveI : Limits.HasLimit (uncurry.obj ((@curry J _ K _ C _).obj G)) := hasLimit_of_iso i
  trans limit (uncurry.obj ((@curry J _ K _ C _).obj G))
  · apply HasLimit.isoOfNatIso i
  · exact limitUncurryIsoLimitCompLim ((@curry J _ K _ C _).obj G)

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
inst✝¹ : Category.{v_1, u_1} C₀
inst✝ : Category.{v_2, u_2} C₁
F₀₁ : C₀ ⥤ C₁
F₁₁' : C₁ ⥤ C₁
G₁₀ : C₁ ⥤ C₀
G₁'₁ : C₁ ⥤ C₁
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₁' : F₁₁' ⊣ G₁'₁
e₀₁₁' : G₁'₁ ⋙ G₁₀ ≅ G₁₀
e₁'₁ : G₁'₁ ≅ 𝟭 C₁
h : e₀₁₁' = isoWhiskerRight e₁'₁ G₁₀ ≪≫ G₁₀.leftUnitor
⊢ adj₀₁.leftAdjointCompIso adj₁₁' adj₀₁ e₀₁₁' = F₀₁.isoWhiskerLeft (adj₁₁'.leftAdjointIdIso e₁'₁) ≪≫ F₀₁.rightUnitor

Tactic:
subst h

Goal state after:
C₀ : Type u_1
C₁ : Type u_2
inst✝¹ : Category.{v_1, u_1} C₀
inst✝ : Category.{v_2, u_2} C₁
F₀₁ : C₀ ⥤ C₁
F₁₁' : C₁ ⥤ C₁
G₁₀ : C₁ ⥤ C₀
G₁'₁ : C₁ ⥤ C₁
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₁' : F₁₁' ⊣ G₁'₁
e₁'₁ : G₁'₁ ≅ 𝟭 C₁
⊢ adj₀₁.leftAdjointCompIso adj₁₁' adj₀₁ (isoWhiskerRight e₁'₁ G₁₀ ≪≫ G₁₀.leftUnitor) =
    F₀₁.isoWhiskerLeft (adj₁₁'.leftAdjointIdIso e₁'₁) ≪≫ F₀₁.rightUnitor
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
inst✝¹ : Category.{v_1, u_1} C₀
inst✝ : Category.{v_2, u_2} C₁
F₀₀' : C₀ ⥤ C₀
F₀'₁ : C₀ ⥤ C₁
G₀'₀ : C₀ ⥤ C₀
G₁₀' : C₁ ⥤ C₀
adj₀₀' : F₀₀' ⊣ G₀'₀
adj₀'₁ : F₀'₁ ⊣ G₁₀'
e₀₀'₁ : G₁₀' ⋙ G₀'₀ ≅ G₁₀'
e₀'₀ : G₀'₀ ≅ 𝟭 C₀
h : e₀₀'₁ = G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor
⊢ adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ e₀₀'₁ = isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor

Tactic:
subst h

Goal state after:
C₀ : Type u_1
C₁ : Type u_2
inst✝¹ : Category.{v_1, u_1} C₀
inst✝ : Category.{v_2, u_2} C₁
F₀₀' : C₀ ⥤ C₀
F₀'₁ : C₀ ⥤ C₁
G₀'₀ : C₀ ⥤ C₀
G₁₀' : C₁ ⥤ C₀
adj₀₀' : F₀₀' ⊣ G₀'₀
adj₀'₁ : F₀'₁ ⊣ G₁₀'
e₀'₀ : G₀'₀ ≅ 𝟭 C₀
⊢ adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor) =
    isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor
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✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ (α_ x✝² x✝¹ x✝).inv ≫ (isoMk (fun X ↦ β_ ((x✝² ⊗ x✝¹).obj X) (x✝.obj X)) ⋯).hom ≫ (α_ x✝ x✝² x✝¹).inv =
    x✝² ◁ (isoMk (fun X ↦ β_ (x✝¹.obj X) (x✝.obj X)) ⋯).hom ≫
      (α_ x✝² x✝ x✝¹).inv ≫ (isoMk (fun X ↦ β_ (x✝².obj X) (x✝.obj X)) ⋯).hom ▷ x✝¹

Tactic:
ext : 1
    apply hexagon_reverse (C := ModuleCat (R.obj _))

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
⊢ ∀ {x y : GrothendieckTopology C}, x.sieves ≤ y.sieves ↔ x ≤ y

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
⊢ IsGLB (sieves '' s) (sInf s).sieves

Tactic:
· rfl

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
⊢ IsGLB (sieves '' s) (sInf s).sieves
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsEmpty C
J : GrothendieckTopology C
⊢ J = ⊤

Tactic:
rw [eq_top_iff]
  intro X
  exact IsEmpty.elim ‹IsEmpty C› X

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S R : Sieve X✝
J : GrothendieckTopology C
X : C
⊢ ∀ ⦃Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X),
    S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)} →
      Sieve.pullback f S ∈ {S | ∀ {Y_1 : C} (f : Y_1 ⟶ Y), ∃ Z g, S.arrows (g ≫ f)}

Tactic:
Y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S R : Sieve X✝
J : GrothendieckTopology C
X Y : C
⊢ ∀ ⦃S : Sieve X⦄ (f : Y ⟶ X),
    S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)} →
      Sieve.pullback f S ∈ {S | ∀ {Y_1 : C} (f : Y_1 ⟶ Y), ∃ Z g, S.arrows (g ≫ f)}
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
H₁ : S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
R : Sieve X
H₂ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | ∀ {Y_1 : C} (f : Y_1 ⟶ Y), ∃ Z g, S.arrows (g ≫ f)}
⊢ R ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}

Tactic:
Y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
H₁ : S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
R : Sieve X
H₂ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | ∀ {Y_1 : C} (f : Y_1 ⟶ Y), ∃ Z g, S.arrows (g ≫ f)}
Y : C
⊢ ∀ (f : Y ⟶ X), ∃ Z g, R.arrows (g ≫ f)
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Precoverage C
inst✝¹ : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
R : Presieve Y
hR : R ∈ J.coverings Y
inst✝ : R.HasPullbacks f
⊢ Presieve.pullbackArrows f R ∈ J.coverings X

Tactic:
obtain ⟨ι, Z, g, rfl⟩ := R.exists_eq_ofArrows
  have (i : ι) : Limits.HasPullback (g i) f := Presieve.hasPullback f (Presieve.ofArrows.mk i)
  rw [← Presieve.ofArrows_pullback]
  exact mem_coverings_of_isPullback _ hR _ _ _ fun i ↦ (IsPullback.of_hasPullback _ _).flip

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
F : C ⥤ D
G : D ⥤ E
J : Precoverage E
⊢ comap (F ⋙ G) J = comap F (comap G J)

Tactic:
ext X R

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
F : C ⥤ D
G : D ⥤ E
J : Precoverage E
X : C
R : Presieve X
⊢ R ∈ (comap (F ⋙ G) J).coverings X ↔ R ∈ (comap F (comap G J)).coverings X
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
F : C ⥤ D
J K : Precoverage D
inst✝ : J.IsStableUnderComposition
ι : Type (max u v)
S : C
Y : ι → C
f : (i : ι) → Y i ⟶ S
hf : Presieve.ofArrows Y f ∈ (comap F J).coverings S
σ : ι → Type (max u v)
Z : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Z i j ⟶ Y i
hg : ∀ (i : ι), Presieve.ofArrows (Z i) (g i) ∈ (comap F J).coverings (Y i)
⊢ (Presieve.ofArrows (fun p ↦ Z p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ (comap F J).coverings S

Tactic:
simp only [mem_comap_iff, Presieve.map_ofArrows, Functor.map_comp] at hf hg ⊢

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
F : C ⥤ D
J K : Precoverage D
inst✝ : J.IsStableUnderComposition
ι : Type (max u v)
S : C
Y : ι → C
f : (i : ι) → Y i ⟶ S
σ : ι → Type (max u v)
Z : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Z i j ⟶ Y i
hf : (Presieve.ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)) ∈ J.coverings (F.obj S)
hg : ∀ (i : ι), (Presieve.ofArrows (fun i_1 ↦ F.obj (Z i i_1)) fun i_1 ↦ F.map (g i i_1)) ∈ J.coverings (F.obj (Y i))
⊢ (Presieve.ofArrows (fun i ↦ F.obj (Z i.fst i.snd)) fun i ↦ F.map (g i.fst i.snd) ≫ F.map (f i.fst)) ∈
    J.coverings (F.obj S)
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
g : Z ⟶ X
i : ι
h : Z = Y i
hg : g = eqToHom h ≫ f i
⊢ ofArrows Y f g

Tactic:
subst h

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
g : Y i ⟶ X
hg : g = eqToHom ⋯ ≫ f i
⊢ ofArrows Y f g
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 : C
R : Presieve X
Y : D
f : Y ⟶ F.obj X
x✝ : ∃ Z, ∃ (h : F.obj Z = Y), ∃ g, R g ∧ F.map g = eqToHom h ≫ f
Z : C
h : F.obj Z = Y
g : Z ⟶ X
hg : R g
heq : F.map g = eqToHom h ≫ f
⊢ map F R f

Tactic:
subst h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve X
Z : C
g : Z ⟶ X
hg : R g
f : F.obj Z ⟶ F.obj X
x✝ : ∃ Z_1, ∃ (h : F.obj Z_1 = F.obj Z), ∃ g, R g ∧ F.map g = eqToHom h ≫ f
heq : F.map g = eqToHom ⋯ ≫ f
⊢ map F R f
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 : C
R : Presieve X
Z : C
g : Z ⟶ X
hg : R g
f : F.obj Z ⟶ F.obj X
x✝ : ∃ Z_1, ∃ (h : F.obj Z_1 = F.obj Z), ∃ g, R g ∧ F.map g = eqToHom h ≫ f
heq : F.map g = eqToHom ⋯ ≫ f
⊢ map F R f

Tactic:
rw [eqToHom_refl, Category.id_comp] at heq

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve X
Z : C
g : Z ⟶ X
hg : R g
f : F.obj Z ⟶ F.obj X
x✝ : ∃ Z_1, ∃ (h : F.obj Z_1 = F.obj Z), ∃ g, R g ∧ F.map g = eqToHom h ≫ f
heq : F.map g = f
⊢ map F R f
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:
subst h

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: 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:
subst 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
Y : C
u : Y ⟶ X
hu : ⟨Y, u⟩ ∈ s.uncurry
⊢ ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst,
      ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).snd⟩ ∈
    (pullbackArrows 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
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:
subst h

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
⊢ ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).snd⟩ ∈
    (s.bind t).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, v⟩ ∈ (ofArrows Y f).uncurry

Tactic:
rw [← eq_of_heq h]

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 mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.Compatible
⊢ x.SieveCompatible

Tactic:
Y

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.Compatible
Y : C
⊢ ∀ ⦃Z : C⦄ (f : Y ⟶ X) (g : Z ⟶ Y) (hf : S.arrows f), x (g ≫ f) ⋯ = (ConcreteCategory.hom (P.map g.op)) (x f hf)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x
⊢ Presieve.FamilyOfElements.SieveCompatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x)

Tactic:
Y

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x
Y : C
⊢ ∀ ⦃Z : C⦄ (f : Y ⟶ X) (g : Z ⟶ Y) (hf : S.arrows f),
    (ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x (g ≫ f) ⋯ =
      (ConcreteCategory.hom (P.map g.op)) ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x f hf)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mpr
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 : P.obj (op X)
q : (firstObjEqFamily P S.arrows).toEquiv ((ConcreteCategory.hom (forkMap P S.arrows)) t) = x
⊢ x.IsAmalgamation t

Tactic:
Y

Goal state after:
case mpr
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 : P.obj (op X)
q : (firstObjEqFamily P S.arrows).toEquiv ((ConcreteCategory.hom (forkMap P S.arrows)) t) = x
Y : C
⊢ ∀ (f : Y ⟶ X) (h : S.arrows f), (ConcreteCategory.hom (P.map f.op)) t = x f h
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 R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : (generate R).arrows f
⊢ (ConcreteCategory.hom (P.map f.op)) t = (ConcreteCategory.hom (P.map ⋯.choose.op)) (x ⋯.choose ⋯)

Tactic:
rw [← ht _, ← comp_apply, ← Functor.map_comp, ← op_comp, hf.choose_spec.choose_spec.choose_spec.2]

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

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
t : (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x
⊢ Presieve.FamilyOfElements.PullbackCompatible ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x)

Tactic:
Y

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
t : (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x
Y : C
⊢ ∀ ⦃Y₂ : C⦄ ⦃f₁ : Y ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : R f₁) (h₂ : R f₂),
    (ConcreteCategory.hom (P.map (pullback.fst f₁ f₂).op)) ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x f₁ h₁) =
      (ConcreteCategory.hom (P.map (pullback.snd f₁ f₂).op)) ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x f₂ h₂)
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✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : F.EssSurj
inst✝ : F.Full
X : C
S : Sieve (F.obj X)
⊢ S ≤ functorPushforward F (functorPullback F S)

Tactic:
Y

Goal state after:
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✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : F.EssSurj
inst✝ : F.Full
X : C
S : Sieve (F.obj X)
Y : D
⊢ ∀ (f : Y ⟶ F.obj X), S.arrows f → (functorPushforward F (functorPullback F S)).arrows f
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) = x
⊢ x.IsAmalgamation t

Tactic:
Y

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) = x
Y : C
⊢ ∀ (f : Y ⟶ X) (h : R f), (ConcreteCategory.hom (P.map f.op)) t = x f h