mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
g : N →ₗ[R] M
hg : g ∘ₗ f = LinearMap.id
x✝ : ↥(⋀[R]^n M)
⊢ (map n LinearMap.id) x✝ = x✝

Tactic:
map_id,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
g : N →ₗ[R] M
hg : g ∘ₗ f = LinearMap.id
x✝ : ↥(⋀[R]^n M)
⊢ LinearMap.id x✝ = x✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
X : Cᵒᵖ
⊢ limMap (F.whiskerLeft (restriction R (𝟙 X))) ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)).inv ≫
        (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)).hom =
    (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (limit (F ⋙ evaluation R X))).inv ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)).hom

Tactic:
Iso.inv_hom_id,

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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
X : Cᵒᵖ
⊢ limMap (F.whiskerLeft (restriction R (𝟙 X))) ≫
      𝟙 (limit (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X))))) =
    (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (limit (F ⋙ evaluation R X))).inv ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)).hom
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ limMap (F.whiskerLeft (restriction R (f ≫ g))) ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (F ⋙ evaluation R Z)).inv ≫
        (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (F ⋙ evaluation R Z)).hom =
    limMap (F.whiskerLeft (restriction R f)) ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            (limMap (F.whiskerLeft (restriction R g)) ≫
              (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv) ≫
          (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (limit (F ⋙ evaluation R Z))).inv ≫
            (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (F ⋙ evaluation R Z)).hom

Tactic:
Iso.inv_hom_id,

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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ limMap (F.whiskerLeft (restriction R (f ≫ g))) ≫
      𝟙 (limit (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g))))) =
    limMap (F.whiskerLeft (restriction R f)) ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            (limMap (F.whiskerLeft (restriction R g)) ≫
              (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv) ≫
          (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (limit (F ⋙ evaluation R Z))).inv ≫
            (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (F ⋙ evaluation R Z)).hom
Module: Mathlib.CategoryTheory.Limits.Final.Connected

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
T : Type w
inst✝¹ : Unique T
F : C ⥤ Discrete T
inst✝ : IsConnected C
⊢ F.Final

Tactic:
rwa [← isConnected_iff_final_of_unique F]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F : J ⥤ C
j : J
⊢ (λ_ F).inv.app j ≫ (λ_ (F.obj j)).hom = (λ_ (F.obj j)).inv ≫ (λ_ (F.obj j)).hom

Tactic:
Iso.inv_hom_id,

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F : J ⥤ C
j : J
⊢ (λ_ F).inv.app j ≫ (λ_ (F.obj j)).hom = 𝟙 (F.obj j)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ F).inv.app j = (ρ_ (F.obj j)).inv

Tactic:
← cancel_mono ((ρ_ (F.obj j)).hom),

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ F).inv.app j ≫ (ρ_ (F.obj j)).hom = (ρ_ (F.obj j)).inv ≫ (ρ_ (F.obj j)).hom
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ F).inv.app j ≫ (ρ_ (F.obj j)).hom = (ρ_ (F.obj j)).inv ≫ (ρ_ (F.obj j)).hom

Tactic:
Iso.inv_hom_id,

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ F).inv.app j ≫ (ρ_ (F.obj j)).hom = 𝟙 (F.obj j)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (α_ F₁ F₂ F₃).inv.app j ≫ (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom =
    (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).inv ≫ (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom

Tactic:
Iso.inv_hom_id,

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (α_ F₁ F₂ F₃).inv.app j ≫ (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom = 𝟙 ((F₁ ⊗ F₂ ⊗ F₃).obj j)
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
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
j j' : J
f : j ⟶ j'
k : K
this : (F.map f).app k ≫ c.ι.app (j', k) = c.ι.app (j, k)
⊢ (F.map f).app k ≫ c.ι.app (j', k) = c.ι.app (j, k)

Tactic:
exact this

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
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit (coneOfConeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ uncurry.obj F ≅ F.obj j :=
  fun j ↦ NatIso.ofComponents (fun x ↦ Iso.refl ((Prod.sectR j K ⋙ uncurry.obj F).obj x)) ⋯
s : Cone (uncurry.obj F)
j' j : J
f : j' ⟶ j
k : K
⊢ (((const J).obj s.pt).map f ≫ (Q j).lift ((Cone.postcompose (E j).hom).obj (Cone.whisker (Prod.sectR j K) s))) ≫
      (D.obj j).π.app k =
    ((Q j').lift ((Cone.postcompose (E j').hom).obj (Cone.whisker (Prod.sectR j' K) s)) ≫ D.conePoints.map f) ≫
      (D.obj j).π.app k

Tactic:
by simpa [E] using s.π.naturality ((Prod.sectL J k).map f)

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
r : ↑cR.pt
⊢ r • 0 = 0

Tactic:
obtain ⟨U, r, rfl⟩ := ιR_jointly_surjective hcR r

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
U : Cᵒᵖ
r : ↑(R.obj U)
⊢ (ιR cR) r • 0 = 0
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : F.PartialRightAdjointSource
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.partialRightAdjointMap (f ≫ g) = F.partialRightAdjointMap f ≫ F.partialRightAdjointMap g

Tactic:
apply F.partialRightAdjointHomEquiv.injective
    simp [partialRightAdjointHomEquiv_comp, ← assoc, ← F.partialRightAdjointHomEquiv_comp]

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

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₁₃ : C₁ ⥤ C₃
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₃₁ : C₃ ⥤ C₁
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
τ₁₂₃ : G₃₁ ⟶ G₃₂ ⋙ G₂₁
τ₀₁₃ : G₃₀ ⟶ G₃₁ ⋙ G₁₀
⊢ F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ τ₁₂₃) ≫ adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃ =
    (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm (τ₀₁₃ ≫ whiskerRight τ₁₂₃ G₁₀)

Tactic:
obtain ⟨τ₁₂₃, rfl⟩ := (conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃)).surjective τ₁₂₃
  obtain ⟨τ₀₁₃, rfl⟩ := (conjugateEquiv adj₀₃ (adj₀₁.comp adj₁₃)).surjective τ₀₁₃
  apply (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).injective
  simp [leftAdjointCompNatTrans, ← conjugateEquiv_whiskerLeft _ _ adj₀₁]

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

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₁₂ : F₀₁ ⋙ F₁₂ ⟶ F₀₂
τ₀₂₃ : F₀₂ ⋙ F₂₃ ⟶ F₀₃
⊢ (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))) ((F₀₁.associator F₁₂ F₂₃).inv ≫ whiskerRight τ₀₁₂ F₂₃ ≫ τ₀₂₃) ≫
      (G₃₂.associator G₂₁ G₁₀).hom =
    (conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃)) τ₀₂₃ ≫
      G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)) τ₀₁₂) ≫
        (G₃₂.associator G₂₁ G₁₀).inv ≫ (G₃₂.associator G₂₁ G₁₀).hom

Tactic:
Iso.inv_hom_id,

Goal state after:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₁₂ : F₀₁ ⋙ F₁₂ ⟶ F₀₂
τ₀₂₃ : F₀₂ ⋙ F₂₃ ⟶ F₀₃
⊢ (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))) ((F₀₁.associator F₁₂ F₂₃).inv ≫ whiskerRight τ₀₁₂ F₂₃ ≫ τ₀₂₃) ≫
      (G₃₂.associator G₂₁ G₁₀).hom =
    (conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃)) τ₀₂₃ ≫
      G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)) τ₀₁₂) ≫ 𝟙 (G₃₂ ⋙ G₂₁ ⋙ G₁₀)
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✝¹ ▷ x✝ = 𝟙 (x✝¹ ⊗ x✝)

Tactic:
ext1 X
    apply MonoidalCategory.id_whiskerRight (C := ModuleCat (R.obj X))

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve Y
T : Presieve X
⊢ pushforward f R ≤ T ↔ R ≤ pullback f T

Tactic:
by
  refine ⟨fun hle Z g hg ↦ hle _ _ (pushforward_apply_comp hg), ?_⟩
  rintro hle Z - ⟨g, rfl, hg⟩
  exact hle _ _ hg

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
inst✝ : Mono f
x : FamilyOfElements P R
hx : (x.map f).Compatible
⊢ x.Compatible

Tactic:
by
  intro Y Z W g₁ g₂ f₁ f₂ hf₁ hf₂ heq
  refine injective_of_mono (f.app _) ?_
  simpa using hx _ _ hf₁ hf₂ heq

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
Z : D
T : Presieve (F.obj Z)
x : FamilyOfElements P T
h : x.Compatible
⊢ (FamilyOfElements.functorPullback F x).Compatible

Tactic:
intro Z₁ Z₂ W g₁ g₂ f₁ f₂ h₁ h₂ eq

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
Z : D
T : Presieve (F.obj Z)
x : FamilyOfElements P T
h : x.Compatible
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ Z
f₂ : Z₂ ⟶ Z
h₁ : Presieve.functorPullback F T f₁
h₂ : Presieve.functorPullback F T f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom ((F.op ⋙ P).map g₁.op)) (FamilyOfElements.functorPullback F x f₁ h₁) =
    (ConcreteCategory.hom ((F.op ⋙ P).map g₂.op)) (FamilyOfElements.functorPullback F x f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
⊢ (x.map f).Compatible

Tactic:
intro Z₁ Z₂ W g₁ g₂ f₁ f₂ h₁ h₂ eq

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
Z₁ Z₂ W : C
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ X
f₂ : Z₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (Q.map g₁.op)) (x.map f f₁ h₁) = (ConcreteCategory.hom (Q.map g₂.op)) (x.map f 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 : C
s : Presieve X
⊢ generate (Presieve.map F s) = functorPushforward F (generate s)

Tactic:
by
  ext
  rw [arrows_generate_map_eq_functorPushforward]
  simp [functorPushforward_extend_eq]

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
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t

Tactic:
simp_rw [compatible_iff_sieveCompatible]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.SieveCompatible → ∃! t, x.IsAmalgamation t
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
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
⊢ ∃ g, F.map g = f ∧ R.arrows g

pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : ∃ g, F.map g = f ∧ R.arrows g
g : Y ⟶ X
hcomp : F.map g = f
hg : R.arrows g
⊢ Presieve.functorPushforward F R.arrows f

Tactic:
· obtain ⟨h', hh'⟩ := F.map_surjective h
    use h' ≫ g
    simp only [Functor.map_comp, hh', hcomp, true_and]
    apply R.downward_closed hg

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
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : ∃ g, F.map g = f ∧ R.arrows g
g : Y ⟶ X
hcomp : F.map g = f
hg : R.arrows g
⊢ Presieve.functorPushforward F R.arrows f
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)
⊢ (Sieve.bind (Sieve.ofArrows Z f).arrows fun x x_1 hg ↦
      Sieve.pullback (Sieve.ofArrows.h hg) (Sieve.generate (R (Sieve.ofArrows.i hg)))) ≤
    Sieve.generate (bindOfArrows Z f R)

Tactic:
by
  rintro T g ⟨W, v, v', hv', ⟨S, u, u', h, hu⟩, rfl⟩
  rw [← Sieve.ofArrows.fac hv', ← reassoc_of% hu]
  exact ⟨S, u, u' ≫ f _, ⟨_, _, h⟩, rfl⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h : g₁ ≫ (fun i ↦ (Over.map p).map (f i)) i₁ = g₂ ≫ (fun i ↦ (Over.map p).map (f i)) i₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) ((fun i ↦ ↑s i) i₁) = (ConcreteCategory.hom (P.map g₂.op)) ((fun i ↦ ↑s i) i₂)

Tactic:
replace h := (Over.forget _).congr_map h

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h :
  (Over.forget B').map (g₁ ≫ (fun i ↦ (Over.map p).map (f i)) i₁) =
    (Over.forget B').map (g₂ ≫ (fun i ↦ (Over.map p).map (f i)) i₂)
⊢ (ConcreteCategory.hom (P.map g₁.op)) ((fun i ↦ ↑s i) i₁) = (ConcreteCategory.hom (P.map g₂.op)) ((fun i ↦ ↑s i) i₂)
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
hG : Presieve.IsSheaf J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection s).arrows i
⊢ (ConcreteCategory.hom (F.map i.op)) ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) =
    (ConcreteCategory.hom (F.map i.op)) s

Tactic:
exact (congr_arg Subtype.val ((hG _ hs).valid_glue (G.family_of_elements_compatible s) _ hi) :)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered

Goal state before:
pp: C : Type u_3
ι : Type u_5
inst✝ : Category.{v_2, u_3} C
F G : Discrete ι ⥤ C
α : F ⟶ G
⊢ Equifibered α

Tactic:
rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩
  simp only [Discrete.functor_map_id]
  exact IsPullback.of_horiz_isIso ⟨by rw [Category.id_comp, Category.comp_id]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered

Goal state before:
pp: C : Type u_3
inst✝ : Category.{v_2, u_3} C
ι : Type u_6
F G : Discrete ι ⥤ C
α : F ⟶ G
⊢ Equifibered α

Tactic:
rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩
  simp only [Discrete.functor_map_id]
  exact IsPullback.of_horiz_isIso ⟨by rw [Category.id_comp, Category.comp_id]⟩

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case h.left
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ (ConcreteCategory.hom
        ((pullbackIsoProdSubtype f g).inv ≫
          prod.lift (pullback.fst f g) (pullback.snd f g) ≫ limit.π (pair X Y) { as := WalkingPair.left }))
      ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩ =
    (ConcreteCategory.hom (limit.π (pair X Y) { as := WalkingPair.left })) x

Tactic:
limit.lift_π

Goal state after:
case h.left
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ (ConcreteCategory.hom
        ((pullbackIsoProdSubtype f g).inv ≫
          (BinaryFan.mk (pullback.fst f g) (pullback.snd f g)).π.app { as := WalkingPair.left }))
      ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩ =
    (ConcreteCategory.hom (limit.π (pair X Y) { as := WalkingPair.left })) x
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case h.right
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ (ConcreteCategory.hom
        ((pullbackIsoProdSubtype f g).inv ≫
          prod.lift (pullback.fst f g) (pullback.snd f g) ≫ limit.π (pair X Y) { as := WalkingPair.right }))
      ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩ =
    (ConcreteCategory.hom (limit.π (pair X Y) { as := WalkingPair.right })) x

Tactic:
limit.lift_π

Goal state after:
case h.right
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ (ConcreteCategory.hom
        ((pullbackIsoProdSubtype f g).inv ≫
          (BinaryFan.mk (pullback.fst f g) (pullback.snd f g)).π.app { as := WalkingPair.right }))
      ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩ =
    (ConcreteCategory.hom (limit.π (pair X Y) { as := WalkingPair.right })) x
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullback f g).str = induced (⇑(ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g)))) (X ⨯ Y).str

Tactic:
simp [prod_topology, pullback_topology, induced_compose, ← coe_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst✝ : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
⊢ (pullback.fst αX f ≫ h') ≫ αZ = (pullback.snd αX f ≫ g) ≫ i

Tactic:
by simp only [Category.assoc, hh.toCommSq.w, pullback.condition_assoc, ← H.w]

Goal state after: