mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
M : ℕ
hM : 0 < M
⊢ ∫ (x : ℝ) in ↑N..↑M + ↑N, f x ≤ ∑ n ∈ Finset.range M, f ↑(n + N)

Tactic:
convert! AntitoneOn.integral_le_sum (anti.mono _) using 2 <;> grind

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ 1 / j ^ 2 ∈ Set.Ioi 0

Tactic:
rw [Set.mem_Ioi]; positivity

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : ∀ (a : A), IsFiltered (StructuredArrow (L.obj a) R)
⊢ IsFiltered (Comma L R)

Tactic:
have (a : Aᵒᵖ) : IsCofiltered (CostructuredArrow R.op (L.op.obj a)) :=
    IsCofiltered.of_equivalence (structuredArrowOpEquivalence R (L.obj a.unop))

Goal state after:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : ∀ (a : A), IsFiltered (StructuredArrow (L.obj a) R)
this : ∀ (a : Aᵒᵖ), IsCofiltered (CostructuredArrow R.op (L.op.obj a))
⊢ IsFiltered (Comma L R)
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : ∀ (a : A), IsFiltered (StructuredArrow (L.obj a) R)
⊢ (snd L R).Final

Tactic:
have (a : Aᵒᵖ) : IsCofiltered (CostructuredArrow R.op (L.op.obj a)) :=
    IsCofiltered.of_equivalence (structuredArrowOpEquivalence R (L.obj a.unop))

Goal state after:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : ∀ (a : A), IsFiltered (StructuredArrow (L.obj a) R)
this : ∀ (a : Aᵒᵖ), IsCofiltered (CostructuredArrow R.op (L.op.obj a))
⊢ (snd L R).Final
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
inst✝ : Injective B
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
l₁ : image (d g) ⟶ B := epiDesc (factorThruImage (d g)) (d f) ⋯
l₂ : A ⟶ B := Injective.factorThru l₁ (Limits.image.ι (d g))
| d g

pp: case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
inst✝ : Injective B
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
l₁ : image (d g) ⟶ B := epiDesc (factorThruImage (d g)) (d f) ⋯
l₂ : A ⟶ B := Injective.factorThru l₁ (Limits.image.ι (d g))
| Injective.factorThru (epiDesc (factorThruImage (d g)) (d f) ⋯) (Limits.image.ι (d g))

Tactic:
rw [← Limits.image.fac (d g)]

Goal state after:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
inst✝ : Injective B
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
l₁ : image (d g) ⟶ B := epiDesc (factorThruImage (d g)) (d f) ⋯
l₂ : A ⟶ B := Injective.factorThru l₁ (Limits.image.ι (d g))
| factorThruImage (d g) ≫ Limits.image.ι (d g)

case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
inst✝ : Injective B
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
l₁ : image (d g) ⟶ B := epiDesc (factorThruImage (d g)) (d f) ⋯
l₂ : A ⟶ B := Injective.factorThru l₁ (Limits.image.ι (d g))
| Injective.factorThru (epiDesc (factorThruImage (d g)) (d f) ⋯) (Limits.image.ι (d g))
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
⊢ { X₁ := I.cocomplex.X (n + 1), X₂ := I.cocomplex.X (n + 1 + 1), X₃ := I.cocomplex.X (n + 1 + 2),
          f := I.cocomplex.d (n + 1) (n + 1 + 1), g := I.cocomplex.d (n + 1 + 1) (n + 1 + 2), zero := ⋯ }.f ≫
      (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0

Tactic:
dsimp
      rw [Preadditive.comp_sub, ← HomologicalComplex.Hom.comm, w, Preadditive.add_comp,
        Category.assoc, Category.assoc, HomologicalComplex.d_comp_d, comp_zero,
        add_zero, sub_self]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian D
C : Type u_2
inst✝² : Category.{v_2, u_2} C
inst✝¹ : Abelian C
X : C
P : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ P.toRightDerivedZero' F ≫ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).iCycles 0 = F.map (P.ι.f 0)

Tactic:
simp [toRightDerivedZero']

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ IsIso (P.toRightDerivedZero' F)

Tactic:
dsimp [InjectiveResolution.toRightDerivedZero']
  rw [CochainComplex.isIso_liftCycles_iff, ShortComplex.exact_and_mono_f_iff_f_is_kernel]
  exact ⟨KernelFork.mapIsLimit _ (P.isLimitKernelFork) F⟩

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
⊢ ∀ (x y : N), ⟨x * y, 1⟩ = ⟨x, 1⟩ * ⟨y, 1⟩

Tactic:
intros; ext <;>
    simp only [mul_left, map_one, MulAut.one_apply, mul_right, mul_one]

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ →* N₂
fg : G₁ →* G₂
h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn
⊢ (map fn fg h).comp inr = inr.comp fg

Tactic:
by ext <;> simp [map]

Goal state after:
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : HasFiniteColimits V
⊢ PreservesFiniteColimits (forget V G)

Tactic:
change PreservesFiniteColimits ((Action.functorCategoryEquivalence V G).functor ⋙
    (evaluation (SingleObj G) V).obj (SingleObj.star G))

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : HasFiniteColimits V
⊢ PreservesFiniteColimits
    ((functorCategoryEquivalence V G).functor ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (adj₁.unit.app (U.obj X)) ≫
      F'.map (U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
        adj₂.counit.app (F'.obj (U.1 X)) =
    𝟙 (F'.obj (U.obj X))

Tactic:
← F'.map_comp_assoc,

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (adj₁.unit.app (U.obj X) ≫ U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
      adj₂.counit.app (F'.obj (U.1 X)) =
    𝟙 (F'.obj (U.obj X))
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h✝ : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ (adj₁.homEquiv (U.obj X) (R.obj Y')).symm
      ((adj₂.homEquiv (U.obj X) Y')
        ↑((Cofork.IsColimit.homIso
              (colimit.isColimit (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X))) Y')
            (h ≫ g))) =
    ↑((Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y'))
        ((Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y)).symm
            ⟨(adj₁.homEquiv (U.obj X) (R.obj Y)).symm
                ((adj₂.homEquiv (U.obj X) Y)
                  ↑((Cofork.IsColimit.homIso
                        (colimit.isColimit
                          (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)))
                        Y)
                      h)),
              ⋯⟩ ≫
          R.map g))

Tactic:
Cofork.IsColimit.homIso_natural,

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h✝ : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ (adj₁.homEquiv (U.obj X) (R.obj Y')).symm
      ((adj₂.homEquiv (U.obj X) Y')
        (↑((Cofork.IsColimit.homIso
                (colimit.isColimit (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X))) Y)
              h) ≫
          g)) =
    ↑((Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y'))
        ((Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y)).symm
            ⟨(adj₁.homEquiv (U.obj X) (R.obj Y)).symm
                ((adj₂.homEquiv (U.obj X) Y)
                  ↑((Cofork.IsColimit.homIso
                        (colimit.isColimit
                          (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)))
                        Y)
                      h)),
              ⋯⟩ ≫
          R.map g))
Module: Mathlib.CategoryTheory.Bicategory.Extension

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : RightLift f g
i : s ⟶ t
x : B
h : x ⟶ c
⊢ (postcomp x f).map (h ◁ i.left) ≫ CostructuredArrow.hom (t.whisker h) = CostructuredArrow.hom (s.whisker h)

Tactic:
← cancel_epi (α_ h _ _).inv

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : RightLift f g
i : s ⟶ t
x : B
h : x ⟶ c
⊢ (α_ h s.lift f).inv ≫ (postcomp x f).map (h ◁ i.left) ≫ CostructuredArrow.hom (t.whisker h) =
    (α_ h s.lift f).inv ≫ CostructuredArrow.hom (s.whisker h)
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
⊢ ∀ (s : LeftExtension f (g ≫ h)) (τ : t.whisker h ⟶ s),
    τ =
      let k := s.extension;
      let θ := s.unit;
      let sτ := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u));
      let τ := H.desc sτ;
      let sσ := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ);
      let σ := H'.desc sσ;
      homMk σ ⋯

Tactic:
intro s' τ₀'

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
⊢ τ₀' =
    let k := s'.extension;
    let θ := s'.unit;
    let sτ := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u));
    let τ := H.desc sτ;
    let sσ := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ);
    let σ := H'.desc sσ;
    homMk σ ⋯
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
x✝ : (p : α → Prop) × (Subtype p → β)
p : α → Prop
f : Subtype p → β
⊢ (fun f ↦ ⟨fun a ↦ (f a).Dom, f.asSubtype⟩) ((fun f x ↦ { Dom := f.fst x, get := fun h ↦ f.snd ⟨x, h⟩ }) ⟨p, f⟩) =
    ⟨p, f⟩

Tactic:
dsimp; congr

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
⊢ C a

Tactic:
have h₂ := (Part.mem_assert_iff.1 h).snd

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a ⋯
⊢ C a
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: case e_f
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (ρ_ X).hom ≫ e₁.inv = (e₁.inv ⊗ₘ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom

Tactic:
← rightUnitor_naturality,

Goal state after:
case e_f
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ e₁.inv ▷ 𝟙_ (LocalizedMonoidal L W ε) ≫ (ρ_ (L'.obj X')).hom =
    (e₁.inv ⊗ₘ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
⊢ g.unop ≫ f.unop = f.unop ≫ g.unop

Tactic:
rw [this, ForgetEnrichment.homTo_comp, Category.assoc, unitors_inv_equal,
      ← leftUnitor_inv_braiding_assoc]

Goal state after:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
⊢ (λ_ (𝟙_ V)).inv ≫
      (β_ (𝟙_ V) (𝟙_ V)).hom ≫
        (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
          eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    f.unop ≫ g.unop
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
hab : a = b
S : 𝒮
hS : p.obj b = S
⊢ p.IsHomLift (𝟙 S) (eqToHom hab)

Tactic:
subst hS hab; simp

Goal state after:
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
g : G
X : C
x✝ : IsGalois X
x : (F.obj X).obj
hg : ∀ (i : PointedGaloisObject F), g ∈ cl i
⊢ g ∈ gi { obj := X, pt := x, isGalois := ⋯ } • ↑(MulAction.stabilizer G x)

Tactic:
exact hg _

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
hp : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
⊢ Groupoid.inv p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj c✝)}

Tactic:
rw [mem_ofPred, inv_eq_inv, φ.map_inv, ← inv_eq_inv]

Goal state after:
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
hp : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
⊢ Groupoid.inv (φ.map p✝) ∈ S.arrows (φ.obj d✝) (φ.obj c✝)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
a b : C
g : a ⟶ b
hg : g ∈ S.arrows a b
⊢ Arrows φ hφ S (φ.obj a) (φ.obj b) (eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯)

Tactic:
← eq_conj_eqToHom

Goal state after:
case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
a b : C
g : a ⟶ b
hg : g ∈ S.arrows a b
⊢ Arrows φ hφ S (φ.obj a) (φ.obj b) (φ.map g)
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.inr ≫ biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p =
    biprod.inr ≫ 𝟙 (P ⊞ P.complement)

Tactic:
rw [biprod.inr_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc,
        add_eq_right, ← assoc]
      refine (?_ =≫ _).trans zero_comp
      ext
      simp only [complement_X, comp_f, decompId_i_f, complement_p,
        decompId_p_f, sub_comp, id_comp, idem, sub_self, zero_def]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
⊢ Map.Arrows φ hφ S (φ.obj c) (φ.obj c) (𝟙 (φ.obj c))

Tactic:
← Functor.map_id

Goal state after:
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
⊢ Map.Arrows φ hφ S (φ.obj c) (φ.obj c) (φ.map (𝟙 c))
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasProducts A
J : Type w
f : J → FormalCoproduct C
F : Cᵒᵖ ⥤ A
s : Cone ((Discrete.functor fun x ↦ op (f x)) ⋙ (evalOp C A).obj F)
i✝ : Discrete J
i : (unop ((Discrete.functor fun x ↦ op (f x)).obj i✝)).I
⊢ ((Pi.lift fun i ↦
          s.π.app { as := i.fst } ≫
            Pi.π (fun i_1 ↦ F.obj (op ((unop ((Discrete.functor fun x ↦ op (f x)).obj { as := i.fst })).obj i_1)))
              i.snd) ≫
        (((evalOp C A).obj F).mapCone (cofan J f).op).π.app i✝) ≫
      Pi.π (fun i ↦ F.obj (op ((unop ((Discrete.functor fun x ↦ op (f x)).obj i✝)).obj i))) i =
    s.π.app i✝ ≫ Pi.π (fun i ↦ F.obj (op ((unop ((Discrete.functor fun x ↦ op (f x)).obj i✝)).obj i))) i

Tactic:
by simp [cofan]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun x ↦ Y
f : md → (X ⟶ Y)
k : md
⊢ (fun f k ↦ f ≫ Pi.π (fun x ↦ Y) k) (Pi.lift f) k = f k

Tactic:
simp [yp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun x ↦ Y
f : X ⟶ yp
j : C
snd✝ : (W : C) × (j ⟶ W)
⊢ Pi.lift ((fun f k ↦ f ≫ Pi.π (fun x ↦ Y) k) f) ≫ Pi.π (fun a ↦ Y) ⟨j, snd✝⟩ = f ≫ Pi.π (fun a ↦ Y) ⟨j, snd✝⟩

Tactic:
simp [yp]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g : X ⟶ Z
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ hf.F.op ⋙ yoneda.obj Z).sections
⊢ ∃ y, ∀ (i : J) (hi : i < j), (ConcreteCategory.hom ((hf.F.op ⋙ yoneda.obj Z).map (homOfLE ⋯).op)) y = ↑s (op ⟨i, hi⟩)

Tactic:
by
          let c : Cocone ((Set.principalSegIio j).monotone.functor ⋙ hf.F) :=
            { pt := Z
              ι.app k := s.1 (op k)
              ι.naturality _ _ g := by
                dsimp
                simpa only [Category.comp_id] using! s.2 g.op }
          exact ⟨(hf.F.isColimitOfIsWellOrderContinuous j hj).desc c, fun k hk ↦
            by simpa using! (hf.F.isColimitOfIsWellOrderContinuous j hj).fac c ⟨k, hk⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case l_naturality
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 𝟙_ D ◁ projectMapAux f✝¹ f✝ ≫ (λ_ (projectObj f✝¹ Y✝)).hom = (λ_ (projectObj f✝¹ X✝)).hom ≫ projectMapAux f✝¹ f✝

Tactic:
rw [MonoidalCategory.leftUnitor_naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: case refine_3
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ LaxMonoidal.ofBifunctor.leftMapᵣ F =
    LaxMonoidal.ofBifunctor.topMapᵣ (εIso G ≪≫ e.symm.app (𝟙_ C) ≪≫ F.mapIso (εIso L).symm).hom ≫
      ((flipFunctor D D E).map (curriedTensorPreIsoPost L W F G).hom).app (𝟙_ D) ≫ LaxMonoidal.ofBifunctor.bottomMapᵣ F

Tactic:
refine natTrans_ext L W (fun X₁ ↦ ?_)
    have := ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).naturality (εIso L).inv
    dsimp [e] at this ⊢
    monoidal_simps
    simp [reassoc_of% this, curriedTensorPreIsoPost_hom_app_app, tensorHom_def,
      whisker_exchange_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc, ← map_comp]

Goal state after: