mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
⊢ Nonempty (IsLimit (P.mapCone c)) ↔ (MorphismProperty.single (coconePtToShrinkYoneda c hc')).isLocal P

Tactic:
by
  rw [Types.isLimit_iff_bijective_sectionOfCone,
    MorphismProperty.isLocal_single_iff_bijective,
    ← Function.Bijective.of_comp_iff' (coconeCompShrinkYonedaHomEquiv hc').symm.bijective,
    ← Function.Bijective.of_comp_iff _ shrinkYonedaEquiv.bijective]
  convert Iff.rfl using 2
  ext : 1
  simp [← coconePtToShrinkYoneda_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Kleisli

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : Kleisli T
f : X.Hom Y
⊢ (𝟭 C).map f.of ≫ 𝟙 ((𝟭 C).obj (T.obj Y.of)) = f.of

Tactic:
apply Category.comp_id

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

Goal state before:
pp: case e'_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h :
  lift (fst R (R ⊗ R)) (lift (snd R (R ⊗ R) ≫ fst R R) (snd R (R ⊗ R) ≫ snd R R) ≫ σ) ≫ μ =
    lift (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ fst R R) ≫ μ) (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ snd R R) ≫ μ) ≫ σ
⊢ lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ) =
    lift (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ fst R R) ≫ μ) (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ snd R R) ≫ μ)

Tactic:
· ext
      · simp only [lift_fst]
        congr 1
        cat_disch
      · simp only [lift_snd]
        congr 1
        cat_disch

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

Goal state before:
pp: case e'_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h :
  lift (lift (fst (R ⊗ R) R ≫ fst R R) (fst (R ⊗ R) R ≫ snd R R) ≫ σ) (snd (R ⊗ R) R) ≫ μ =
    lift (lift (fst (R ⊗ R) R ≫ fst R R) (snd (R ⊗ R) R) ≫ μ) (lift (fst (R ⊗ R) R ≫ snd R R) (snd (R ⊗ R) R) ≫ μ) ≫ σ
⊢ lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) =
    lift (lift (fst (R ⊗ R) R ≫ fst R R) (snd (R ⊗ R) R) ≫ μ) (lift (fst (R ⊗ R) R ≫ snd R R) (snd (R ⊗ R) R) ≫ μ)

Tactic:
· ext
      · simp only [lift_fst]
        congr 1
        cat_disch
      · simp only [lift_snd]
        congr 1
        cat_disch

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

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
inst✝¹ : MonoidalClosed V
F G H : C ⥤ V
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C × C
f : x ⟶ y
this :
  F.obj x.1 ◁ ℌ.π x.2 x.1 ≫ F.obj x.1 ◁ (ihom (F.obj x.1)).map (G.map (f.1 ▷ x.2)) =
    F.obj x.1 ◁ ℌ.π x.2 y.1 ≫ F.obj x.1 ◁ (MonoidalClosed.pre (F.map f.1)).app (G.obj (y.1 ⊗ x.2))
⊢ (F.map f.1 ▷ H.obj x.2 ≫ F.obj y.1 ◁ H.map f.2) ≫ MonoidalClosed.uncurry (ℌ.π y.2 y.1) =
    MonoidalClosed.uncurry (ℌ.π x.2 x.1) ≫ G.map (f.1 ⊗ₘ f.2)

Tactic:
simp only [Category.assoc, MonoidalClosed.uncurry_eq, Functor.id_obj,
          ← whiskerLeft_comp_assoc, map_comp_π]

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalClosed V
F G H : C ⥤ V
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C × C
f : x ⟶ y
this :
  F.obj x.1 ◁ ℌ.π x.2 x.1 ≫ F.obj x.1 ◁ (ihom (F.obj x.1)).map (G.map (f.1 ▷ x.2)) =
    F.obj x.1 ◁ ℌ.π x.2 y.1 ≫ F.obj x.1 ◁ (MonoidalClosed.pre (F.map f.1)).app (G.obj (y.1 ⊗ x.2))
⊢ F.map f.1 ▷ H.obj x.2 ≫
      F.obj y.1 ◁ (ℌ.π x.2 y.1 ≫ (ihom (F.obj y.1)).map (G.map (y.1 ◁ f.2))) ≫
        (ihom.ev (F.obj y.1)).app (G.obj (y.1 ⊗ y.2)) =
    F.obj x.1 ◁ ℌ.π x.2 x.1 ≫ (ihom.ev (F.obj x.1)).app (G.obj (x.1 ⊗ x.2)) ≫ G.map (f.1 ⊗ₘ f.2)
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X✝ Y✝ : C ⥤ Comon D
α : X✝ ⟶ Y✝
x : C
⊢ (α.app x).hom ≫ ε = ε

Tactic:
rw [IsComonHom.hom_counit (α.app x).hom]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : C ⥤ CommMon D
⊢ (β_ ((monFunctorCategoryEquivalence C D).inverse.obj (F ⋙ CommMon.forget₂Mon D)).X
          ((monFunctorCategoryEquivalence C D).inverse.obj (F ⋙ CommMon.forget₂Mon D)).X).hom ≫
      μ =
    μ

Tactic:
ext X; exact IsCommMonObj.mul_comm (F.obj X).X

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✝
⊢ map (𝟙 ((ι C V D).obj (𝟙_ D))) ((ι C V D).map f) ≫ (ι C V D).map (λ_ Y✝).hom =
    (ι C V D).map (λ_ X✝).hom ≫ (ι C V D).map f

Tactic:
ι_map_leftUnitor_hom_eq_leftUnitor_hom,

Goal state after:
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✝
⊢ map (𝟙 ((ι C V D).obj (𝟙_ D))) ((ι C V D).map f) ≫
      (DayConvolutionUnit.leftUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj Y✝)).hom =
    (ι C V D).map (λ_ X✝).hom ≫ (ι C V D).map f
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case neg
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)
j : β
k : α
h : ¬f k = g j
⊢ biproduct.ι (fun a ↦ s (f a)) k ≫ z ≫ biproduct.π (fun b ↦ s (g b)) j = 0

Tactic:
apply o.eq_zero h

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
I : IsIso f
⊢ f ≠ 0

Tactic:
intro h
    apply id_nonzero X
    simp only [← IsIso.hom_inv_id f, h, zero_comp]

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

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

pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ (∑ j_1,
      (if h : i = i then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
    𝟙 { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd } ⟨i, j⟩ ⟨i', j'⟩

Tactic:
· intro hi
              simp at hi

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ (∑ j_1,
      (if h : i = i then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
    𝟙 { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd } ⟨i, j⟩ ⟨i', j'⟩
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inr
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
h : D₂.W f✝
⊢ (D₁.P ⊔ D₂.P) i✝

Tactic:
exact Or.inr (D₂.src h)

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

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
this✝ : IsCardinalFiltered J Cardinal.aleph0
α : Type w
w✝¹ : PartialOrder α
w✝ : IsCardinalFiltered α Cardinal.aleph0
F : α ⥤ J
h✝ : F.Final
this : IsFiltered α
⊢ ∃ α x, ∃ (_ : IsDirected α fun x1 x2 ↦ x1 ≤ x2) (_ : Nonempty α), ∃ F, F.Final

Tactic:
exact ⟨α, _, IsFiltered.isDirectedOrder _, nonempty, F, inferInstance⟩

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (regularCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (regularCoverage C).Saturate Y_1 (Sieve.pullback f S)
b : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → ∃ Y_2 π, EffectiveEpi π ∧ (Sieve.pullback f S).arrows π
Y₁ : C
π : Y₁ ⟶ Y
h₁ : EffectiveEpi π
h₂ : R.arrows π
Y' : C
π' : Y' ⟶ Y₁
h✝ : EffectiveEpi π'
H : (Sieve.pullback π S).arrows π'
⊢ S.arrows (π' ≫ π)

Tactic:
by simpa using H

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

Goal state before:
pp: case refine_2.of.a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i ↦ X i
⊢ Sieve.pullback (ψ ≫ Sigma.desc f) (generate (Presieve.ofArrows X f)) ∈
    (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck R

Tactic:
rw [Sieve.pullback_comp]

Goal state after:
case refine_2.of.a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i ↦ X i
⊢ Sieve.pullback ψ (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))) ∈
    (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck R
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mp.of
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ (extensiveCoverage C).coverings X
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Sieve.generate S).arrows (π a)

Tactic:
| of X S hS =>

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

Goal state before:
pp: case e'_2
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a ↦ Exists.choose ⋯
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a ↦ F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a ↦ op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this✝ : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
this : (ConcreteCategory.hom (f.app (op (Z a)))) (x a) = (ConcreteCategory.hom (G.map (π a).op)) y
⊢ (ConcreteCategory.hom (F.map (Sigma.ι Z a).op))
      ((ConcreteCategory.hom (F.map (opCoproductIsoProduct Z).inv))
        ((ConcreteCategory.hom (PreservesProduct.iso F fun a ↦ op (Z a)).inv)
          ((ConcreteCategory.hom (Types.productIso fun a ↦ F.obj (op (Z a))).inv) x))) =
    x a

Tactic:
rw [← Functor.map_comp_apply, opCoproductIsoProduct_inv_comp_ι, ← piComparison_comp_π]
      change ((PreservesProduct.iso F _).hom ≫ _) _ = _
      have := Types.productIso_hom_comp_eval (fun a ↦ F.obj (op (Z a))) a
      rw [← Iso.eq_inv_comp] at this
      simp only [types_comp_apply, Iso.inv_hom_id_apply]
      simp [← comp_apply]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
⊢ (sq i₁ i₂).p₁.op.toLoc ≫ p.op.toLoc = f₁.op.toLoc

Tactic:
← Quiver.Hom.comp_toLoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
⊢ ((sq i₁ i₂).p₁.op ≫ p.op).toLoc = f₁.op.toLoc
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
⊢ (sq i₁ i₂).p₂.op.toLoc ≫ p.op.toLoc = f₂.op.toLoc

Tactic:
← Quiver.Hom.comp_toLoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
⊢ ((sq i₁ i₂).p₂.op ≫ p.op).toLoc = f₂.op.toLoc
Module: Mathlib.CategoryTheory.Subfunctor.Finite

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
U : Cᵒᵖ
u : (yoneda.obj X).obj U
⊢ u ∈ (⨆ i, Subfunctor.ofSection (𝟙 X)).obj U ↔ u ∈ ⊤.obj U

Tactic:
simp only [Subfunctor.iSup_obj, Set.mem_iUnion,
    exists_const, Subfunctor.top_obj, Set.top_eq_univ, Set.mem_univ, iff_true]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
U : Cᵒᵖ
u : (yoneda.obj X).obj U
⊢ u ∈ (Subfunctor.ofSection (𝟙 X)).obj U
Module: Mathlib.CategoryTheory.Subfunctor.Subobject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : MonoOver F
f : X ⟶ Y
⊢ range X.arrow ≤ range Y.arrow

Tactic:
by
        rw [← MonoOver.w f]
        apply range_comp_le

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
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
e : F.DescentData f ≌ F.DescentData f'
iso : F.toDescentData f ⋙ e.functor ≅ F.toDescentData f'
⊢ (F.toDescentData f).IsEquivalence ↔ (F.toDescentData f').IsEquivalence

Tactic:
rw [← Functor.isEquivalence_iff_of_iso iso]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
e : F.DescentData f ≌ F.DescentData f'
iso : F.toDescentData f ⋙ e.functor ≅ F.toDescentData f'
⊢ (F.toDescentData f).IsEquivalence ↔ (F.toDescentData f ⋙ e.functor).IsEquivalence
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ J S
M N : ↑(F.obj { as := op S })
⊢ Sieve.generate ((Sieve.overEquiv (Over.mk (𝟙 S))).symm (Sieve.generate (Presieve.ofArrows X f))).arrows ∈
    (J.over S) (Over.mk (𝟙 S))

Tactic:
rwa [GrothendieckTopology.mem_over_iff, Sieve.generate_sieve, OrderIso.apply_symm_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
x✝ : ↑((S.sequence F n₀ n₁ h).obj ⟨0, ⋯⟩)
⊢ (AddCommGrpCat.Hom.hom
        ((S.sequence F n₀ n₁ h).map' 0 1 homMk₁._proof_4 _proof_450✝ ≫
          ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom))
      x✝ =
    (AddCommGrpCat.Hom.hom
        ((Iso.refl ((S.sequence F n₀ n₁ h).obj' 0 _proof_449✝)).hom ≫
          (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 0 1 homMk₁._proof_4 _proof_450✝))
      x✝

Tactic:
apply biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
x✝ : ↑((S.sequence F n₀ n₁ h).obj ⟨3, ⋯⟩)
⊢ (AddCommGrpCat.Hom.hom
        ((S.sequence F n₀ n₁ h).map' 3 4 _proof_364✝ _proof_453✝ ≫
          ((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom))
      x✝ =
    (AddCommGrpCat.Hom.hom
        ((Iso.refl ((S.sequence F n₀ n₁ h).obj' 3 _proof_452✝)).hom ≫
          (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 3 4 _proof_364✝ _proof_453✝))
      x✝

Tactic:
apply biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply

Goal state after:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
⊢ χ' = χ m

Tactic:
ext : 1
  rw [← cancel_mono (closedSieves J).ι, χ_hom, Subfunctor.lift_ι]
  apply Presheaf.χ_unique _
  have pb : IsPullback (𝟙 G.obj) χ'.hom (χ'.hom ≫ (closedSieves J).ι)
    (closedSieves J).ι := IsPullback.of_horiz_isIso_mono (by simp)
  have : IsPullback m.hom ?_ χ'.hom <| (truth J).hom := by
    simpa using hχ'.map (sheafToPresheaf J _)
  simpa using this.paste_horiz pb

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
a : α
h : a ∈ s
⊢ (bipartiteAbove r t a).Nonempty

Tactic:
← coe_nonempty,

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
a : α
h : a ∈ s
⊢ (↑(bipartiteAbove r t a)).Nonempty
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ log (2 ^ 3) * (69 / 50)

Tactic:
gcongr
      · field_simp
        simp (disch := positivity) [exp_one_gt_two]
      · norm_num1
        exact two_div_one_sub_two_div_e_le_eight

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

Goal state before:
pp: N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N ≤ rexp 16

Tactic:
apply le_trans _ four_zero_nine_six_lt_exp_sixteen.le

Goal state after:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N ≤ 4096
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 4 * A)) ≤ K ^ 3 * ↑(#A)
hA₀ : A.Nonempty
F : Finset G
hF : ↑(#F) ≤ K ^ 3
hAF : A ^ 4 ⊆ F * (A / A)
⊢ (↑A ^ 2) ^ 2 ⊆ ↑F • ↑A ^ 2

Tactic:
by norm_cast; simpa [div_eq_mul_inv, pow_succ, mul_assoc, hAsymm] using hAF

Goal state after:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: case insert
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
⊢ #(insert x C * A * B) * #A ≤ #(A * B) * #(insert x C * A)

Tactic:
| insert x C _ ih =>

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph W
e : V ≃ W
⊢ SimpleGraph.map (⇑e.symm.toEmbedding) G = SimpleGraph.comap (⇑e.toEmbedding) G

Tactic:
← comap_symm,

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph W
e : V ≃ W
⊢ SimpleGraph.comap (⇑e.symm.symm.toEmbedding) G = SimpleGraph.comap (⇑e.toEmbedding) G