mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
ι : Type u_1
inst✝³ : Small.{w, u_1} ι
inst✝² : P.IsClosedUnderLimitsOfShape (Discrete ι)
inst✝¹ : HasProductsOfShape ι C
inst✝ : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
x✝ : P.ind.strictLimitsOfShape (Discrete ι) X
Y : Discrete ι ⥤ C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
⊢ P.ind (limit Y)

Tactic:
let e := equivShrink ι

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
ι : Type u_1
inst✝³ : Small.{w, u_1} ι
inst✝² : P.IsClosedUnderLimitsOfShape (Discrete ι)
inst✝¹ : HasProductsOfShape ι C
inst✝ : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
x✝ : P.ind.strictLimitsOfShape (Discrete ι) X
Y : Discrete ι ⥤ C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
e : ι ≃ Shrink.{w, u_1} ι := equivShrink ι
⊢ P.ind (limit Y)
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)
a b : D
⊢ (ι C V D).map ((α_ a (𝟙_ D) b).hom ≫ (𝟙 a ⊗ₘ (λ_ b).hom)) = (ι C V D).map ((ρ_ a).hom ⊗ₘ 𝟙 b)

Tactic:
simp only [Functor.map_comp, Functor.map_id, ι_map_tensorHom_hom_eq_tensorHom,
        ι_map_associator_hom_eq_associator_hom, ι_map_leftUnitor_hom_eq_leftUnitor_hom,
        ι_map_rightUnitor_hom_eq_rightUnitor_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)
a b : D
⊢ (DayConvolution.associator ((ι C V D).obj a) ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj b)).hom ≫
      map (𝟙 ((ι C V D).obj a)) (DayConvolutionUnit.leftUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj b)).hom =
    map (DayConvolutionUnit.rightUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj a)).hom (𝟙 ((ι C V D).obj b))
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : IsAlgClosed 𝕜
inst✝² : Linear 𝕜 C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
I : FiniteDimensional 𝕜 (X ⟶ X)
g : End X
c : 𝕜
⊢ c • 𝟙 X * g = g * c • 𝟙 X

Tactic:
obtain ⟨d, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 g

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : IsAlgClosed 𝕜
inst✝² : Linear 𝕜 C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
I : FiniteDimensional 𝕜 (X ⟶ X)
c d : 𝕜
⊢ c • 𝟙 X * d • 𝟙 X = d • 𝟙 X * c • 𝟙 X
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
⊢ Function.Surjective fun x ↦ ⟨Arrow.mk (𝟙 j), ⋯⟩

Tactic:
rintro ⟨f, hf⟩
      refine ⟨⟨⟩, ?_⟩
      ext
      exact ((MorphismProperty.ofHoms_iff _ _).1
        ((MorphismProperty.arrow_mk_mem_toSet_iff _ _).1 hf)).choose_spec.symm

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
⊢ Presieve.IsSheaf (coherentTopology C) P ↔
    ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
by
  constructor
  · intro hP B α _ X π h
    simp only [coherentTopology, Presieve.isSheaf_coverage] at hP
    apply hP
    exact ⟨α, inferInstance, X, π, rfl, h⟩
  · intro h
    simp only [coherentTopology, Presieve.isSheaf_coverage]
    rintro B S ⟨α, _, X, π, rfl, hS⟩
    exact h _ _ _ _ hS

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.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
⊢ t.ι (f.s₀ (g.s₀ i)) ≫ G.map (F.p₁ (hgf.H i)).op ≫ G.map (hgf.a i).op = t.ι i

Tactic:
reassoc_of% 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
⊢ t.ι i ≫ G.map (F.p₂ (hgf.H i)).op ≫ G.map (hgf.a i).op = t.ι i
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)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D₁ D₂ : F.DescentData' sq sq₃
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    (F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).hom ≫ D₂.hom i₁ i₂ =
      D₁.hom i₁ i₂ ≫ (F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (e i₂).hom
i₁ i₂ : ι
⊢ (F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).inv ≫
      D₁.hom i₁ i₂ ≫ (F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (e i₂).hom =
    D₂.hom i₁ i₂

Tactic:
← cancel_epi ((F.map _).toFunctor.map (e i₁).hom),

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)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D₁ D₂ : F.DescentData' sq sq₃
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    (F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).hom ≫ D₂.hom i₁ i₂ =
      D₁.hom i₁ i₂ ≫ (F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (e i₂).hom
i₁ i₂ : ι
⊢ (F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).hom ≫
      (F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).inv ≫
        D₁.hom i₁ i₂ ≫ (F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (e i₂).hom =
    (F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).hom ≫ D₂.hom i₁ i₂
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})
x : (fun X ↦ X) α
⊢ (ConcreteCategory.hom (S.map (↾fun x ↦ PUnit.unit).op))
      (f ((ConcreteCategory.hom (↾fun x_1 ↦ x)) (Classical.choose ⋯))) =
    f x

Tactic:
convert! ConcreteCategory.congr_hom (S.map_id _) _

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

Goal state before:
pp: ⊢ ⇑(Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) = ⇑typesGrothendieckTopology

Tactic:
funext α

Goal state after:
α : Type u
⊢ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α = typesGrothendieckTopology α
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
X : C
π' : X ⟶ underlying.obj h.Ω₀
⊢ π' = h.π (𝟙 X)

Tactic:
by
    have : IsPullback (𝟙 X) π' (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow :=
      { isLimit' := ⟨PullbackCone.IsLimit.mk _ (fun s ↦ s.fst) (by simp)
          (fun s ↦ by rw [← cancel_mono h.Ω₀.arrow, ← s.condition, Category.assoc])
          (fun s m hm _ ↦ by simpa using hm) ⟩ }
    rw [← cancel_mono h.Ω₀.arrow, h.uniq this,
      ← (h.isPullback (𝟙 X)).w, Category.id_comp]

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 : ℕ
y : ↑(F.H' n S.X₄)
⊢ (ConcreteCategory.hom (S.toBiprod F n)) y =
    (ConcreteCategory.hom
        (((F.cohomologyPresheaf n).obj (op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (op S.X₃))).inv)
      ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
        (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y)

Tactic:
by
  apply (AddCommGrpCat.biprodIsoProd _ _).addCommGroupIsoToAddEquiv.injective
  dsimp [toBiprod]
  ext
  · rw [Iso.addCommGroupIsoToAddEquiv_apply,
      Iso.addCommGroupIsoToAddEquiv_apply,
      ← AddCommGrpCat.biprodIsoProd_inv_comp_fst_apply,
      Iso.hom_inv_id_apply, ← ConcreteCategory.comp_apply,
      biprod.lift_fst, Iso.inv_hom_id_apply]
  · rw [Iso.addCommGroupIsoToAddEquiv_apply,
      Iso.addCommGroupIsoToAddEquiv_apply,
      ← AddCommGrpCat.biprodIsoProd_inv_comp_snd_apply,
      Iso.hom_inv_id_apply, ← ConcreteCategory.comp_apply,
      biprod.lift_snd, Iso.inv_hom_id_apply]

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 ℤ
⊢ ∀ (a b : ℤ), -(a + b) = -a + -b

Tactic:
intros; lia

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 ℤ
G : C ⥤ D
inst✝¹ : G.CommShift ℤ
τ : F ⟶ G
inst✝ : NatTrans.CommShift τ ℤ
⊢ ∀ (a b : ℤ), -(a + b) = -a + -b

Tactic:
intros; lia

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 ℤ
G : D ⥤ C
inst✝¹ : G.CommShift ℤ
adj : F ⊣ G
inst✝ : adj.CommShift ℤ
⊢ ∀ (a b : ℤ), -(a + b) = -a + -b

Tactic:
intros; lia

Goal state after:
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.shiftClosure ℤ).binaryProductsClosure.retractClosure.retractClosure =
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure

Tactic:
retractClosure_eq_self

Goal state after:
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.shiftClosure ℤ).binaryProductsClosure.retractClosure = (P.shiftClosure ℤ).binaryProductsClosure.retractClosure
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 ℤ
G : D ⥤ C
inst✝¹ : G.CommShift ℤ
adj : F ⊣ G
inst✝ : adj.CommShift ℤ
eq : adj.op = PullbackShift.adjunction (AddMonoidHom.mk' (fun n ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj)
⊢ ∀ (a b : ℤ), -(a + b) = -a + -b

Tactic:
intros; lia

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

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✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this : Mono ((adj.homEquiv Z T.obj₃) h)
Y : C
φ : Y ⟶ G.obj T.obj₃
ψ : Y ⟶ Z
hψ : φ ≫ G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁ = ψ ≫ g
α : Y ⟶ G.obj T.obj₃
hα : α = φ - ψ ≫ (adj.homEquiv Z T.obj₃) h
hα₀ : α ≫ G.map T.mor₃ = 0
β : Y ⟶ Z
hβ : β ≫ (adj.homEquiv Z T.obj₃) h = α
⊢ (ψ + β) ≫ (adj.homEquiv Z T.obj₃) h = φ

Tactic:
rw [add_comp, hβ, hα, add_sub_cancel]

Goal state after:
Module: Mathlib.CategoryTheory.UnivLE

Goal state before:
pp: w : uliftFunctor.{u, v}.EssSurj
α : Type (max u v)
⊢ Small.{v, max u v} α

Tactic:
obtain ⟨a', m⟩ := w.mem_essImage α

Goal state after:
w : uliftFunctor.{u, v}.EssSurj
α : Type (max u v)
a' : Type v
m : Nonempty (uliftFunctor.{u, v}.obj a' ≅ α)
⊢ Small.{v, max u v} α
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
ha : a ≠ 0
hs : ThreeGPFree (a • s)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : b * d = c * c
⊢ a • b * a • d = a * c * (a * c)

Tactic:
by
        rw [smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h, mul_mul_mul_comm]

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ mulRothNumber s ≤ mulRothNumber (map (mulLeftEmbedding a) s)

Tactic:
obtain ⟨u, hus, hcard, hu⟩ := mulRothNumber_spec s
    have h : ThreeGPFree (u.map <| mulLeftEmbedding a : Set α) := by rw [coe_map]; exact hu.smul_set
    convert! h.le_mulRothNumber (map_subset_map.2 hus) using 1
    rw [card_map, hcard]

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

Goal state before:
pp: M N : ℕ
⊢ rothNumberNat (M + N) ≤ rothNumberNat M + rothNumberNat N

Tactic:
simp_rw [rothNumberNat_def]

Goal state after:
M N : ℕ
⊢ addRothNumber (range (M + N)) ≤ addRothNumber (range M) + addRothNumber (range N)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑N ^ ((↑n - ↑2) / ↑(nValue N)) / rexp 1 ^ (↑n - ↑2) / ↑n

Tactic:
cast_two,

Goal state after:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑N ^ ((↑n - 2) / ↑(nValue N)) / rexp 1 ^ (↑n - 2) / ↑n
Module: Mathlib.Combinatorics.Additive.ETransform

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ #(x.1 ∪ e • x.2) + #(x.2 ∩ e⁻¹ • x.1) = #x.1 + #x.2

Tactic:
← card_smul_finset e (_ ∩ _),

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ #(x.1 ∪ e • x.2) + #(e • (x.2 ∩ e⁻¹ • x.1)) = #x.1 + #x.2
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: case refine_2
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝¹ : Fact (1 < n)
this✝ : ↑(n / n.minFac) ≠ 0
s : AddSubgroup (ZMod n)
hs : s ≠ ⊥
x✝ : (↑s).Finite
this : Nontrivial ↥s
⊢ ↑n.minFac ≤ ↑(Nat.card ↥s)

Tactic:
exact WithTop.coe_le_coe.2 <| minFac_le_of_dvd Finite.one_lt_card <|
      (card_addSubgroup_dvd_card _).trans n.card_zmod.dvd

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : Mul α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ #s + #t - 1 ≤ #(s * t)

Tactic:
suffices s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht} by
    rw [← card_singleton_mul (s.max' hs) t, ← card_mul_singleton s (t.min' ht),
      ← card_union_add_card_inter, ← card_singleton _, ← this, Nat.add_sub_cancel]
    exact card_mono (union_subset (mul_subset_mul_left <| singleton_subset_iff.2 <| min'_mem _ _) <|
      mul_subset_mul_right <| singleton_subset_iff.2 <| max'_mem _ _)
  refine eq_singleton_iff_unique_mem.2 ⟨mem_inter.2 ⟨mul_mem_mul (max'_mem _ _) <|
    mem_singleton_self _, mul_mem_mul (mem_singleton_self _) <| min'_mem _ _⟩, ?_⟩
  simp only [mem_inter, and_imp, mem_mul, mem_singleton, exists_eq_left,
    forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mul_left_inj]
  exact fun a' ha' b' hb' h ↦ (le_max' _ _ ha').eq_of_not_lt fun ha ↦
    (lt_of_eq_of_lt h (mul_lt_mul_left ha _)).not_ge <| mul_le_mul_right (min'_le _ _ hb') _

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
s : Set V
h : (induce s G).spanningCoe = G
v : V
hv : v ∈ Subtype.val '' (induce s G).support
⊢ v ∈ s

Tactic:
have ⟨u, _, hvu⟩ := hv

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
s : Set V
h : (induce s G).spanningCoe = G
v : V
hv : v ∈ Subtype.val '' (induce s G).support
u : ↑s
left✝ : u ∈ (induce s G).support
hvu : ↑u = v
⊢ v ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype W
inst✝ : DecidableRel G'.Adj
f : G ≃g G'
⊢ G.minDegree = G'.minDegree

Tactic:
classical
  have : (G'.degree ·) ∘ f = (G.degree ·) := funext (f.degree_eq ·)
  rw [minDegree, minDegree, ← this, ← image_image, Finset.image_univ_of_surjective f.surjective]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
i j : EInt
f : i ⟶ j
X : C
⊢ (t.eTruncLT.map f).app X ≫ (t.eTruncLTι j).app X = (t.eTruncLTι i).app X

Tactic:
simp only [← NatTrans.comp_app, ← Functor.map_comp]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
i j : EInt
f : i ⟶ j
X : C
⊢ (t.eTruncLT.map (f ≫ homOfLE ⋯)).app X = (t.eTruncLTι i).app X
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
i j : EInt
f : i ⟶ j
X : C
⊢ (t.eTruncGEπ i).app X ≫ (t.eTruncGE.map f).app X = (t.eTruncGEπ j).app X

Tactic:
simp only [← NatTrans.comp_app, ← Functor.map_comp]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
i j : EInt
f : i ⟶ j
X : C
⊢ (t.eTruncGE.map (homOfLE ⋯ ≫ f)).app X = (t.eTruncGEπ j).app X
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n : ℕ
⊢ ↑(stepBound n) = ↑n * 4 ^ n

Tactic:
by unfold stepBound; norm_cast

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∃ f, ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst

Tactic:
use P.equivSigmaParts.trans ((Equiv.refl _).sigmaCongr (fun t ↦ t.1.equivFin))
  simp [equivSigmaParts, Equiv.sigmaCongr, Equiv.sigmaCongrLeft]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a✝ : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
a : α
⊢ (∃ i ∈ x, a ∈ {b ∈ x | s i b}) ↔ a ∈ x

Tactic:
mem_filter

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a✝ : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
a : α
⊢ (∃ i ∈ x, a ∈ x ∧ s i a) ↔ a ∈ x
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
hz1 : z ∈ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}
R : Finset (Finset α)
hR : R ∈ F.powerset
hz2 : z ∈ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
⊢ Q = R

Tactic:
mem_filter

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ∈ F.powerset
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
⊢ Q = R
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ u : Finset α
P : Finpartition s✝
a✝ : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ F
⊢ t ∈ {u ∈ F | a ∈ u} ↔ a ∈ t

Tactic:
mem_filter

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ u : Finset α
P : Finpartition s✝
a✝ : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ F
⊢ t ∈ F ∧ a ∈ t ↔ a ∈ t