mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ⊗ₘ Δ) ≫
      (α_ A A (A ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫
              (α_ A A A).inv ▷ A ≫
                (α_ (A ⊗ A) A A).hom ≫
                  (A ⊗ A) ◁ (β_ A A).hom ≫ (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮) ≫ (((α_ (A ⊗ A) A A).inv ≫ μ ▷ A ▷ A) ≫ μ ▷ A) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
slice_lhs 11 12 =>
    simp only [← comp_whiskerRight]
    rw [MonObj.mul_assoc]
    simp only [comp_whiskerRight]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ⊗ₘ Δ) ≫
      (α_ A A (A ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫
              (α_ A A A).inv ▷ A ≫
                (α_ (A ⊗ A) A A).hom ≫
                  (A ⊗ A) ◁ (β_ A A).hom ≫
                    (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮) ≫ (α_ (A ⊗ A) A A).inv ≫ ((α_ A A A).hom ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ▷ A ≫
      (α_ A A A).hom ≫
        ((((((A ◁ (β_ A A).hom ≫ A ◁ Δ ▷ A) ≫ A ◁ (α_ A A A).hom) ≫ A ◁ A ◁ (𝒮 ⊗ₘ 𝒮)) ≫ A ◁ (α_ A A A).inv) ≫
              A ◁ μ ▷ A) ≫
            A ◁ μ) ≫
          μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
tensorHom_def'

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ▷ A ≫
      (α_ A A A).hom ≫
        ((((((A ◁ (β_ A A).hom ≫ A ◁ Δ ▷ A) ≫ A ◁ (α_ A A A).hom) ≫ A ◁ A ◁ (A ◁ 𝒮 ≫ 𝒮 ▷ A)) ≫ A ◁ (α_ A A A).inv) ≫
              A ◁ μ ▷ A) ≫
            A ◁ μ) ≫
          μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| ε ▷ A ≫ 𝟙_ C ◁ ε

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| η ▷ 𝟙_ C

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (ρ_ A).hom

Tactic:
rw [← tensorHom_def]

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| ε ⊗ₘ ε

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| η ▷ 𝟙_ C

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (ρ_ A).hom
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ (α_ P.X Q.X L.X).inv ≫
      (α_ P.X Q.X L.X).hom ≫
        P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
          coequalizer.π (P.actRight ▷ TensorBimod.X Q L)
            ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L) =
    P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
      coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X)
          ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫
        𝟙 (TensorBimod.X P (Q.tensorBimod L))

Tactic:
slice_lhs 1 3 => rw [Iso.inv_hom_id_assoc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
      coequalizer.π (P.actRight ▷ TensorBimod.X Q L)
        ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L) =
    P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
      coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X)
          ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫
        𝟙 (TensorBimod.X P (Q.tensorBimod L))
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case of_presieve
C : Type u
inst✝³ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
X✝¹ Y✝¹ : C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderBaseChange
inst✝ : HasPullbacks C
Y X Z✝ : C
f✝ : X ⟶ Z✝
X✝ Y✝ : C
f : X✝ ⟶ Y✝
R : Presieve X✝
hR : R ∈ K.coverings X✝
h✝ : ∀ (U : C) (g : U ⟶ X✝), R g → sourceLocalClosure K P (g ≫ f)
ih :
  ∀ (U : C) (g : U ⟶ X✝),
    R g →
      ∀ (W : C) (g_1 : Y ⟶ Y✝) (fst : W ⟶ U) (snd : W ⟶ Y), IsPullback fst snd (g ≫ f) g_1 → sourceLocalClosure K P snd
W : C
g : Y ⟶ Y✝
fst : W ⟶ X✝
snd : W ⟶ Y
h : IsPullback fst snd f g
U : C
v : U ⟶ W
Z : C
u : Z ⟶ X✝
hu : R u
⊢ sourceLocalClosure K P (pullback.snd u fst ≫ snd)

Tactic:
exact ih _ _ hu _ g (pullback.fst _ _) _ (.paste_vert (.of_hasPullback _ _) h)

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
hp : P ≤ isFinitelyPresentable C
inst✝ : LocallySmall.{w, v, u} C
⊢ P.ind.ind = P.ind

Tactic:
refine le_antisymm (fun X Y f hf ↦ ?_) P.ind.le_ind

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
hp : P ≤ isFinitelyPresentable C
inst✝ : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
hf : P.ind.ind f
⊢ P.ind f
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f : X ⟶ Y
⊢ (∃ R ∈ K.coverings X, ∀ (U : C) (g : U ⟶ X), R g → P (g ≫ f)) → sourceLocalClosure K P f

Tactic:
intro ⟨R, hR, h⟩

Goal state after:
case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f : X ⟶ Y
R : Presieve X
hR : R ∈ K.coverings X
h : ∀ (U : C) (g : U ⟶ X), R g → P (g ≫ f)
⊢ sourceLocalClosure K P f
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u✝ v✝ : Arrow V
f✝ g : u✝ ⟶ v✝
inst✝ : HasBinaryBiproducts V
u v : Arrow V
f : u ⟶ v
⊢ IsIso (Hom.right (π f))

Tactic:
by simp only [π, homMk_right]; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
a✝ : Projective P
X Y : C
p : X ⟶ Y
x✝ : Epi p
⊢ HasLiftingProperty 0 p

Tactic:
exact Projective.hasLiftingProperty_of_isZero 0 p hZ

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{u, u, u + 1} Q), hasCardinalLTWithTerminal κ ≤ Q.isoClosure

Tactic:
obtain ⟨X, hX⟩ : ∃ (X : Type u), Cardinal.mk X = κ := ⟨κ.ord.ToType, by simp⟩

Goal state after:
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X : Type u
hX : Cardinal.mk X = κ
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{u, u, u + 1} Q), hasCardinalLTWithTerminal κ ≤ Q.isoClosure
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
⊢ (if h' : j' = j then eqToHom ⋯ else 0) = if h : j = j' then eqToHom ⋯ else 0

Tactic:
by_cases h : j' = j

Goal state after:
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
h : j' = j
⊢ (if h' : j' = j then eqToHom ⋯ else 0) = if h : j = j' then eqToHom ⋯ else 0

case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
h : ¬j' = j
⊢ (if h' : j' = j then eqToHom ⋯ else 0) = if h : j = j' then eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ (∑ j, (fun j_1 x ↦ if h : j_1 = j then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : j = k then eqToHom ⋯ else 0) i j =
    if h : i = j then eqToHom ⋯ else 0

Tactic:
rw [Finset.sum_apply, Finset.sum_apply, Finset.sum_eq_single i]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ ((fun j x ↦ if h : j = i then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : i = k then eqToHom ⋯ else 0) i j =
    if h : i = j then eqToHom ⋯ else 0

case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ ∀ b ∈ Finset.univ,
    b ≠ i → ((fun j x ↦ if h : j = b then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : b = k then eqToHom ⋯ else 0) i j = 0

case h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
⊢ i ∉ Finset.univ →
    ((fun j x ↦ if h : j = i then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : i = k then eqToHom ⋯ else 0) i j = 0
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
a : ↑J.withTop.obj
⊢ ∃ S, J.PropSetWithTop κ' S ∧ a ∈ S

Tactic:
by
    induction a with
    | some a => exact ⟨_, propSetWithTop_pair _ a, by aesop⟩
    | none => exact ⟨_, propSetWithTop_pair _ (Classical.arbitrary _), by aesop⟩

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
j : ↑J.obj
⊢ HasTerminal ↑{j}

Tactic:
by
    let : OrderTop ({j} : Set J.obj) := { top := ⟨j, rfl⟩, le_top := by simp }
    exact isTerminalTop.hasTerminal

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP :
  ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] (c : PullbackCone π π) (x : IsLimit c),
    Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯))
⊢ EqualizerCondition P

Tactic:
by
  intro X B π _ c hc
  specialize hP X B π c hc
  rw [Types.type_equalizer_iff_unique]
  rw [Function.bijective_iff_existsUnique] at hP
  intro b hb
  obtain ⟨a, ha₁, ha₂⟩ := hP ⟨b, hb⟩
  refine ⟨a, ?_, ?_⟩
  · simpa [mapToEqualizer] using Subtype.ext_iff.1 ha₁
  · intro y h
    apply ha₂ y
    ext
    simpa [mapToEqualizer] using h

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ regularTopology C ≤ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck

Tactic:
exact (Coverage.gi _).gc.monotone_l le_sup_right

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
⊢ ∀ (m : t.pt ⟶ (F.multifork G).pt),
    (∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i) →
      m = Multifork.IsLimit.lift hE (fun a ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯

Tactic:
m

Goal state after:
case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
m : t.pt ⟶ (F.multifork G).pt
⊢ (∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i) →
    m = Multifork.IsLimit.lift hE (fun a ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (pullback.snd f (𝒰.f i))
⊢ f ≫ 𝒰.glueMorphisms (fun i ↦ inv (pullback.snd f (𝒰.f i)) ≫ pullback.fst f (𝒰.f i)) ⋯ = 𝟙 X

Tactic:
exact (𝒰.pullback₁ f).hom_ext fun i ↦ by simp [pullback.condition_assoc]

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

Goal state before:
pp: case right.left
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.left
fac : a ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.left s.fst s.snd ≫ F.obj.map b.op

Tactic:
obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' h₁.isLimit _ _ fac.symm
            simpa using s.condition.symm =≫ F.obj.map φ.op

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst✝³ : HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R
⊢ F.IsStack J.toGrothendieck

Tactic:
have := IsPrestack.of_precoverage (fun S R hR ↦ (hF _ _ hR).isPrestackFor)

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
inst✝³ : HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
hF : ∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R
this : F.IsPrestack J.toGrothendieck
⊢ F.IsStack J.toGrothendieck
Module: Mathlib.CategoryTheory.Sites.Point.Monoidal

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ P₃ : Cᵒᵖ ⥤ A
X : C
x : Φ.fiber.obj X
| (α_ P₁ P₂ P₃).hom.app (Opposite.op X) ≫
    Φ.toPresheafFiber X x P₁ ▷ (P₂.obj (Opposite.op X) ⊗ P₃.obj (Opposite.op X)) ≫
      Φ.presheafFiber.obj P₁ ◁ (Φ.toPresheafFiber X x P₂ ⊗ₘ Φ.toPresheafFiber X x P₃)

Tactic:
rw [← tensorHom_def]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ P₃ : Cᵒᵖ ⥤ A
X : C
x : Φ.fiber.obj X
| (α_ P₁ P₂ P₃).hom.app (Opposite.op X) ≫
    (Φ.toPresheafFiber X x P₁ ⊗ₘ Φ.toPresheafFiber X x P₂ ⊗ₘ Φ.toPresheafFiber X x P₃)
Module: Mathlib.CategoryTheory.Sites.Point.Map

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
J : GrothendieckTopology C
Φ : J.Point
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : F.IsCocontinuous J K
X : D
R : Sieve X
hR : R ∈ K X
u : Φ.fiber.Elements
f : (CategoryOfElements.π Φ.fiber ⋙ F).obj u ⟶ X
⊢ ∃ Y g, ∃ (_ : R.arrows g), ∃ v q a, a ≫ g = F.map ↑q ≫ f

Tactic:
obtain ⟨U, u⟩ := u

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
J : GrothendieckTopology C
Φ : J.Point
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : F.IsCocontinuous J K
X : D
R : Sieve X
hR : R ∈ K X
U : C
u : Φ.fiber.obj U
f : (CategoryOfElements.π Φ.fiber ⋙ F).obj ⟨U, u⟩ ⟶ X
⊢ ∃ Y g, ∃ (_ : R.arrows g), ∃ v q a, a ≫ g = F.map ↑q ≫ f
Module: Mathlib.CategoryTheory.Sites.Point.Map

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
J : GrothendieckTopology C
Φ : J.Point
F : C ⥤ D
K : GrothendieckTopology D
inst✝³ : F.IsCocontinuous J K
inst✝² : LocallySmall.{w, v', u'} D
A : Type u''
inst✝¹ : Category.{v'', u''} A
inst✝ : HasColimitsOfSize.{w, w, v'', u''} A
P : Dᵒᵖ ⥤ A
X : C
x : Φ.fiber.obj X
⊢ Φ.toPresheafFiber X x (F.op ⋙ P) ≫ (Φ.presheafFiberMapObjIso F K P).inv = Φ.toPresheafFiberMap F K P X x

Tactic:
simpa [-toPresheafFiberMap_presheafFiberMapObjIso_hom] using
    (Φ.toPresheafFiberMap_presheafFiberMapObjIso_hom F K ..).symm =≫
      (Φ.presheafFiberMapObjIso F K P).inv

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

Goal state before:
pp: case restrict
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
t : (X : C) → ι X → F.obj (Opposite.op X) := fun X i ↦ ↑((equivShrink ↑(𝒮 X)).symm i)
x : F.obj (Opposite.op X)
Z✝ W✝ : C
f : Z✝ ⟶ W✝
a✝ : F.obj (Opposite.op W✝)
ha : K.SubsheafClosure 𝒮 W✝ a✝
ih : ∃ i, Witness.eval hF ι t i = some a✝
⊢ ∃ i, Witness.eval hF ι t i = some ((ConcreteCategory.hom (F.map f.op)) a✝)

Tactic:
| restrict f ha ih =>

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
t : (X : C) → ι X → F.obj (Opposite.op X) := fun X i ↦ ↑((equivShrink ↑(𝒮 X)).symm i)
x : F.obj (Opposite.op X)
hx : K.SubsheafClosure 𝒮 X x
⊢ ∃ i, Witness.eval hF ι t i = some x

Tactic:
induction hx with

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
⊢ Nonempty (F.toDescentData fun f ↦ f.obj.hom).FullyFaithful ↔
    ∀ (M N : ↑(F.obj { as := op S })),
      Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows

Tactic:
Functor.FullyFaithful.nonempty_iff_map_bijective

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
⊢ (∀ (X Y : ↑(F.obj { as := op S })), Function.Bijective (F.toDescentData fun f ↦ f.obj.hom).map) ↔
    ∀ (M N : ↑(F.obj { as := op S })),
      Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ pullback.snd 𝒞.truth (𝒞.χ i) ≫ 𝟙 X =
    (underlyingIso (pullback.snd 𝒞.truth (𝒞.χ i))).inv ≫ ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow

Tactic:
rw [Iso.eq_inv_comp, comp_id, underlyingIso_hom_comp_eq_mk]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ (Subobject.mk (pullback.snd 𝒞.truth (𝒞.χ i))).arrow = ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
⊢ P.triangEnvelopeIter 0 = (P.shiftClosure ℤ).binaryProductsClosure.retractClosure

Tactic:
rw [triangEnvelopeIter, extensionProductIter_zero, retractClosure_eq_self]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map (𝟙 ((𝟭 Cᵒᵖ).obj X)).unop =
    (((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj (unop X)))).unop ≫
        (shiftFunctor D n).map ((commShiftIso F.op n).hom.app X).unop ≫
          (commShiftIso F n).inv.app (unop ((shiftFunctor Cᵒᵖ n).obj X))) ≫
      F.map ((opShiftFunctorEquivalence C n).unitIso.hom.app X).unop

Tactic:
map_opShiftFunctorEquivalence_unitIso_hom_app_unop,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map (𝟙 ((𝟭 Cᵒᵖ).obj X)).unop =
    (((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj (unop X)))).unop ≫
        (shiftFunctor D n).map ((commShiftIso F.op n).hom.app X).unop ≫
          (commShiftIso F n).inv.app (unop ((shiftFunctor Cᵒᵖ n).obj X))) ≫
      (commShiftIso F n).hom.app (unop ((shiftFunctor Cᵒᵖ n).obj X)) ≫
        (shiftFunctor D n).map ((commShiftIso F.op n).inv.app X).unop ≫
          ((opShiftFunctorEquivalence D n).unitIso.hom.app (op (F.obj (unop X)))).unop
Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
p q : ℤ
⊢ iso C (p + q) = Functor.CommShift.isoAdd (iso C p) (iso C q)

Tactic:
ext X
    simp only [Functor.CommShift.isoAdd_hom_app, op_comp,
      ← shiftFunctorAdd'_eq_shiftFunctorAdd, Functor.map_comp,
      fun X n ↦ iso_hom_app X n (-n) (add_neg_cancel n),
      shiftFunctorAdd'_op_hom_app _ p q (p + q) rfl (-p) (-q) (-(p + q))
        (add_neg_cancel p) (add_neg_cancel q) (add_neg_cancel (p + q)),
      shiftFunctorAdd'_op_inv_app _ (-p) (-q) (-(p + q)) (by lia) p q (p + q)
        (neg_add_cancel p) (neg_add_cancel q) (neg_add_cancel (p + q)),
      shiftFunctor_op_map _ (-q) q, shiftFunctor_op_map _ q (-q)]
    simp [← Functor.map_comp_assoc, ← unop_comp, ← unop_comp_assoc]

Goal state after: