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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : Reflective i
inst✝² : MonoidalClosed C
inst✝¹ : CartesianMonoidalCategory D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : C ⥤ D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  curry
    ((ir.homEquiv (A ⊗ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))) ≫
        (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B))))
⊢ (reflector i).map (A ◁ η.app (A ⟹ i.obj B)) ≫
      prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
        L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫
          inv (prodComparison (reflector i) A (A ⟹ i.obj B)) ≫
            (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B)) =
    (ir.homEquiv (A ⊗ (A ⟹ i.obj B)) B).symm ((ihom.ev A).app (i.obj B))

Tactic:
prodComparison_natural_whiskerLeft_assoc,

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : Reflective i
inst✝² : MonoidalClosed C
inst✝¹ : CartesianMonoidalCategory D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : C ⥤ D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  curry
    ((ir.homEquiv (A ⊗ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))) ≫
        (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B))))
⊢ prodComparison (reflector i) A (A ⟹ i.obj B) ≫
      (reflector i).obj A ◁ (reflector i).map (η.app (A ⟹ i.obj B)) ≫
        L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫
          inv (prodComparison (reflector i) A (A ⟹ i.obj B)) ≫
            (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B)) =
    (ir.homEquiv (A ⊗ (A ⟹ i.obj B)) B).symm ((ihom.ev A).app (i.obj B))
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
U : C ⥤ V
inst✝ : DayConvolutionUnit U
c : C
v : V
g h : U.obj c ⟶ v
e : ∀ (f : 𝟙_ C ⟶ c), can ≫ U.map f ≫ g = can ≫ U.map f ≫ h
⊢ g = h

Tactic:
apply (isPointwiseLeftKanExtensionCan c).hom_ext
  intro j
  simpa using e j.hom

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C✝ : Type u₁
inst✝¹⁶ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹⁵ : Category.{v₂, u₂} V✝
inst✝¹⁴ : MonoidalCategory C✝
inst✝¹³ : MonoidalCategory V✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ (𝟙 (𝟙_ D) ⊗ₘ f) ≫ (λ_ Y✝).hom = (λ_ X✝).hom ≫ f

Tactic:
by
      apply Functor.Faithful.map_injective (F := ι C V D)
      simp only [Functor.map_comp, ι_map_tensorHom_hom_eq_tensorHom, Functor.map_id]
      rw [ι_map_leftUnitor_hom_eq_leftUnitor_hom,
        ι_map_leftUnitor_hom_eq_leftUnitor_hom]
      exact DayConvolutionUnit.leftUnitor_naturality
        (ι C V D |>.obj <| 𝟙_ D) (ι C V D |>.map f)

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
i : ι
j : ↑(g ⁻¹' {i})
k : ↑(f ⁻¹' {i})
⊢ s i = s (f ↑k)

Tactic:
by
          rcases k with ⟨k, ⟨⟩⟩
          simp

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

Goal state before:
pp: case refine_1
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j x✝ : J
h : __Diagram✝.P x✝
⊢ ∃ lift, __Diagram✝.W lift

Tactic:
simp only [Diagram.single_P, ObjectProperty.singleton_iff] at h

Goal state after:
case refine_1
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j x✝ : J
h : j = x✝
⊢ ∃ lift, __Diagram✝.W lift
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
X : Type w
inst✝ : PartialOrder X
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
hm : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) (C : SetCardinalLT κ₁ ↑B) (hC : C ∈ Y B hB), ∀ b ∈ ↑C, ↑b ≤ m B hB C hC
B : Set X
hB : HasCardinalLT (↑B) κ₂
T : Type w
f : T → ↑B
hT : HasCardinalLT T κ₁
C₀ : SetCardinalLT κ₁ ↑B := ⟨Set.range f, ⋯⟩
C : SetCardinalLT κ₁ ↑B
hC : C ∈ Y B hB
hC' : C₀ ≤ C
⊢ ∃ a, ∀ (t : T), ↑(f t) ≤ ↑a

Tactic:
exact ⟨⟨m B hB C hC, Set.subset_iUnion _ ⟨C, hC⟩ (Or.inr (by simp))⟩,
    fun t ↦ hm B hB C hC (f t) (hC' (by simp [C₀]))⟩

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

Goal state before:
pp: case inl.inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
i : ι
hf : (D i).W f✝
⊢ (∃ a, (D a).P i✝) ∨ m = i✝

Tactic:
exact Or.inl ⟨i, (D i).src hf⟩

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
⊢ ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
    ∀ S ∈ {S | ∃ X_1 f, (S = Presieve.ofArrows (fun x ↦ X_1) fun x ↦ f) ∧ EffectiveEpi f},
      ∃ T ∈ {S | ∃ X f, (S = Presieve.ofArrows (fun x ↦ X) fun x ↦ f) ∧ EffectiveEpi f}, T.FactorsThruAlong S f

Tactic:
by
    intro X Y f S ⟨Z, π, hπ, h_epi⟩
    have := Preregular.exists_fac f π
    obtain ⟨W, h, _, i, this⟩ := this
    refine ⟨Presieve.singleton h, ⟨?_, ?_⟩⟩
    · exact ⟨W, h, by {rw [Presieve.ofArrows_pUnit h]}, inferInstance⟩
    · intro W g hg
      cases hg
      refine ⟨Z, i, π, ⟨?_, this⟩⟩
      cases hπ
      rw [Presieve.ofArrows_pUnit]
      exact Presieve.singleton.mk

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).coverings X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
Z : Fin n → C := fun i ↦ unop (K.obj { as := i })
this✝ : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).HasPairwisePullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (∐ Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun i ↦ op (Z i) := Discrete.natIsoFunctor
⊢ PreservesLimit K F

Tactic:
let _ : PreservesLimit (Discrete.functor (fun i ↦ op (Z i))) F :=
        Presieve.preservesProduct_of_isSheafFor F ?_ initialIsInitial _ (coproductIsCoproduct Z)
        (FinitaryExtensive.isPullback_initial_to_sigma_ι Z)
        (hF (Presieve.ofArrows Z (fun i ↦ Sigma.ι Z i)) ?_)

Goal state after:
case refine_1.refine_3
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).coverings X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
Z : Fin n → C := fun i ↦ unop (K.obj { as := i })
this✝ : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).HasPairwisePullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (∐ Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun i ↦ op (Z i) := Discrete.natIsoFunctor
x✝ : PreservesLimit (Discrete.functor fun i ↦ op (Z i)) F :=
  preservesProduct_of_isSheafFor F ?refine_1.refine_1 initialIsInitial (Cofan.mk (∐ Z) (Sigma.ι Z))
    (coproductIsCoproduct Z) (FinitaryExtensive.isPullback_initial_to_sigma_ι Z)
    (hF (ofArrows Z fun i ↦ Sigma.ι Z i) ?refine_1.refine_2)
⊢ PreservesLimit K F

case refine_1.refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).coverings X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
Z : Fin n → C := fun i ↦ unop (K.obj { as := i })
this✝ : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).HasPairwisePullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (∐ Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun i ↦ op (Z i) := Discrete.natIsoFunctor
⊢ IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)

case refine_1.refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).coverings X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
Z : Fin n → C := fun i ↦ unop (K.obj { as := i })
this✝ : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).HasPairwisePullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (∐ Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun i ↦ op (Z i) := Discrete.natIsoFunctor
⊢ (ofArrows Z fun i ↦ Sigma.ι Z i) ∈ (extensiveCoverage C).coverings (∐ Z)
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits

Goal state before:
pp: A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
⊢ Presheaf.IsSheaf (extensiveTopology C) (pointwiseCocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)).pt

Tactic:
Presheaf.isSheaf_iff_preservesFiniteProducts

Goal state after:
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
⊢ PreservesFiniteProducts (pointwiseCocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)).pt
Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : ↑(F.obj { as := op S })
S' : C
q : S' ⟶ S
T : (Over S')ᵒᵖ
⊢ ((Over.map q).op ⋙ F.presheafHom M N).obj T ≃
    (F.presheafHom ((F.map q.op.toLoc).toFunctor.obj M) ((F.map q.op.toLoc).toFunctor.obj N)).obj T

Tactic:
letI e := Cat.Hom.toNatIso (F.mapComp' (.toLoc q.op) (.toLoc T.unop.hom.op)
      (.toLoc ((Over.map q).obj T.unop).hom.op))
    exact (Iso.homFromEquiv (e.app M)).trans (Iso.homToEquiv (e.app N))

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

Goal state before:
pp: case refine_2
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)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = (g.comp f).h₀ i
h2 :
  t.ι (F.multicospanShape.fst ⟨((g.comp f).toHom.1 i, (Hom.id F).toHom.1 i), hgf.H i⟩) ≫
      (F.multicospanIndex G).fst ⟨((g.comp f).toHom.1 i, (Hom.id F).toHom.1 i), hgf.H i⟩ =
    t.ι (F.multicospanShape.snd ⟨((g.comp f).toHom.1 i, (Hom.id F).toHom.1 i), hgf.H i⟩) ≫
      (F.multicospanIndex G).snd ⟨((g.comp f).toHom.1 i, (Hom.id F).toHom.1 i), hgf.H i⟩
⊢ Multifork.IsLimit.lift hE (fun a ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫ G.map (F.f i).op = t.ι i

Tactic:
dsimp at h1 h2

Goal state after:
case refine_2
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)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = g.h₀ i ≫ f.h₀ (g.s₀ i)
h2 : t.ι (f.s₀ (g.s₀ i)) ≫ G.map (F.p₁ (hgf.H i)).op = t.ι i ≫ G.map (F.p₂ (hgf.H i)).op
⊢ Multifork.IsLimit.lift hE (fun a ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫ G.map (F.f i).op = t.ι i
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
⊢ (F.map f₁.op.toLoc).toFunctor.map (hom w hf' φ i₁) =
    D₁.hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (hom w hf' φ i₂) ≫ D₂.hom q f₂ f₁ ⋯ ⋯

Tactic:
refine ((isSheaf_iff_isSheaf_of_type _ _).1
    (IsPrestack.isSheaf J (D₁.obj i₁) (D₂.obj i₁)) _ H).isSeparatedFor.ext ?_

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
⊢ ∀ ⦃Y : Over (X i₁)⦄ ⦃f_1 : Y ⟶ Over.mk f₁⦄,
    ((Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f'))).arrows f_1 →
      (ConcreteCategory.hom ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).map f_1.op))
          ((F.map f₁.op.toLoc).toFunctor.map (hom w hf' φ i₁)) =
        (ConcreteCategory.hom ((F.presheafHom (D₁.obj i₁) (D₂.obj i₁)).map f_1.op))
          (D₁.hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (hom w hf' φ i₂) ≫ D₂.hom q f₂ f₁ ⋯ ⋯)
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F✝ G✝ : Cᵒᵖ ⥤ A
F G : Sheaf J A
X : Cᵒᵖ
⊢ ↾(J.overMapPullback A (𝟙 X).unop).map = 𝟙 ((J.overPullback A (unop X)).obj F ⟶ (J.overPullback A (unop X)).obj G)

Tactic:
ext φ : 4
    exact ConcreteCategory.congr_hom ((presheafHom F.1 G.1).map_id X) φ.1

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
inst✝ : ∀ (Z : C), _root_.Small.{max u v, w} (F.obj (Opposite.op Z))
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor F S.arrows

Tactic:
let F' : Cᵒᵖ ⥤ Type max u v := FunctorToTypes.shrink F

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
inst✝ : ∀ (Z : C), _root_.Small.{max u v, w} (F.obj (Opposite.op Z))
X : C
S : Sieve X
hS : S ∈ J X
F' : Cᵒᵖ ⥤ Type (max u v) := FunctorToTypes.shrink.{max u v, w, v, u} F
⊢ Presieve.IsSheafFor F S.arrows
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
this : (ConcreteCategory.hom f₁) (Classical.choose hf₁) = (ConcreteCategory.hom f₂) (Classical.choose hf₂)
⊢ (ConcreteCategory.hom (S.map (((↾fun x ↦ PUnit.unit).op ≫ g₁.op) ≫ g.op)))
      (f ((ConcreteCategory.hom f₁) (Classical.choose hf₁))) =
    (ConcreteCategory.hom (S.map (((↾fun x ↦ PUnit.unit).op ≫ g₂.op) ≫ g.op)))
      (f ((ConcreteCategory.hom f₂) (Classical.choose hf₂)))

Tactic:
this,

Goal state after:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
this : (ConcreteCategory.hom f₁) (Classical.choose hf₁) = (ConcreteCategory.hom f₂) (Classical.choose hf₂)
⊢ (ConcreteCategory.hom (S.map (((↾fun x ↦ PUnit.unit).op ≫ g₁.op) ≫ g.op)))
      (f ((ConcreteCategory.hom f₂) (Classical.choose hf₂))) =
    (ConcreteCategory.hom (S.map (((↾fun x ↦ PUnit.unit).op ≫ g₂.op) ≫ g.op)))
      (f ((ConcreteCategory.hom f₂) (Classical.choose hf₂)))
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
h :
  ∀ (M N : ↑(F.obj { as := op S })),
    Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows
S₀ : C
M N : ↑(F.obj { as := op S₀ })
a : S ⟶ S₀
⊢ Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk a)).symm R).arrows

Tactic:
replace h := h ((F.map a.op.toLoc).toFunctor.obj M) ((F.map a.op.toLoc).toFunctor.obj N)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
S₀ : C
M N : ↑(F.obj { as := op S₀ })
a : S ⟶ S₀
h :
  Presieve.IsSheafFor (F.presheafHom ((F.map a.op.toLoc).toFunctor.obj M) ((F.map a.op.toLoc).toFunctor.obj N))
    ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows
⊢ Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk a)).symm R).arrows
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
J : GrothendieckTopology C
hF : ∀ (S : C), ∀ R ∈ J S, F.IsPrestackFor R.arrows
S✝ : C
M N : ↑(F.obj { as := op S✝ })
⊢ Presheaf.IsSheaf (J.over S✝) (F.presheafHom M N)

Tactic:
by
    rw [isSheaf_iff_isSheaf_of_type]
    intro U S hS
    obtain ⟨U, u, rfl⟩ := Over.mk_surjective U
    apply (hF _ _ hS).isSheafFor'

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
⊢ Over.Hom.left (h.iso m).inv.hom ≫ Over.Hom.left (h.iso m).hom.hom ≫ pullbackπ (h.χ m) h.Ω₀ = pullbackπ (h.χ m) h.Ω₀

Tactic:
rw [← Over.comp_left_assoc]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
⊢ Over.Hom.left ((h.iso m).inv.hom ≫ (h.iso m).hom.hom) ≫ pullbackπ (h.χ m) h.Ω₀ = pullbackπ (h.χ m) h.Ω₀
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
n : ℕ
⊢ P.triangEnvelopeIter (n + 1) =
    ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProduct (P.triangEnvelopeIter n)).retractClosure

Tactic:
by
  rw [triangEnvelopeIter, extensionProductIter_succ,
    ← retractClosure_extensionProduct_retractClosure_retractClosure]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X Y : A
n : ℤ
f : (shiftFunctor C n).obj (ι.obj X) ⟶ ι.obj Y
hn : 0 < n
⊢ (shiftEquiv C n).unitIso.hom.app (ι.obj X) ≫ (shiftFunctor C (-n)).map f = 0

Tactic:
exact hι _ (by lia)

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
⊢ (ι ⋙ shiftFunctor C 1).map (ιK f₃ α ≫ f₁) = (ι ⋙ shiftFunctor C 1).map 0

Tactic:
by
    have := comp_distTriang_mor_zero₃₁ _ hT
    dsimp at this
    simp [this]

Goal state after:
Module: Mathlib.Combinatorics.Pigeonhole

Goal state before:
pp: α : Type u
β : Type v
M : Type w
inst✝³ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝² : CommSemiring M
inst✝¹ : LinearOrder M
inst✝ : IsStrictOrderedRing M
hf : ∀ a ∈ s, f a ∈ t
ht : #t • b < ↑(#s)
⊢ ∃ y ∈ t, b < ↑(#({x ∈ s | f x = y}))

Tactic:
simp_rw [cast_card] at ht ⊢
  exact exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum hf ht

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d✝ k N : ℕ
x : Fin n → ℕ
d : ℕ
⊢ ∑ i, 0 i * d ^ ↑i = 0

Tactic:
simp_rw [Pi.zero_apply, zero_mul, sum_const_zero]

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : x₁ 0 + (∑ x, x₁ x.succ * d ^ ↑x) * d = x₂ 0 + (∑ x, x₂ x.succ * d ^ ↑x) * d
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)

Tactic:
this,

Goal state after:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : x₂ 0 + (∑ x, x₁ x.succ * d ^ ↑x) * d = x₂ 0 + (∑ x, x₂ x.succ * d ^ ↑x) * d
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)