mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x : ↑(R F)
⊢ x * 0 = 0

Tactic:
refine Quot.inductionOn x ?_; clear x; intro x
      obtain ⟨j, x⟩ := x
      erw [colimit_zero_eq _ j, colimit_mul_mk_eq _ ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j)]
      rw [CategoryTheory.Functor.map_id]
      dsimp
      rw [mul_zero x]
      rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case h
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
σ₁₂ : Perm m × Perm n
hσ₁₂ : (sumCongrHom m n) σ₁₂ = σ
⊢ σ₁₂ ∈ ↑univ ∧ (fun σ ↦ σ.1.sumCongr σ.2) σ₁₂ = σ

Tactic:
← hσ₁₂

Goal state after:
case h
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
σ₁₂ : Perm m × Perm n
hσ₁₂ : (sumCongrHom m n) σ₁₂ = σ
⊢ σ₁₂ ∈ ↑univ ∧ (fun σ ↦ σ.1.sumCongr σ.2) σ₁₂ = (sumCongrHom m n) σ₁₂
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3.refine_3
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ Set.SurjOn (fun σ ↦ σ.1.sumCongr σ.2) ↑univ ↑(↑(sumCongrHom m n).range).toFinset

Tactic:
intro σ hσ
        rw [mem_coe, Set.mem_toFinset] at hσ
        obtain ⟨σ₁₂, hσ₁₂⟩ := hσ
        use σ₁₂
        rw [← hσ₁₂]
        simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3.refine_4
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m
σ₂ : Perm n
⊢ (↑↑(sign σ₁) * ∏ x, A (σ₁ x) x) * (↑↑(sign σ₂) * ∏ x, D (σ₂ x) x) =
    ↑↑(sign (σ₁.sumCongr σ₂)) *
      ((∏ x, fromBlocks A B 0 D (Sum.map (⇑σ₁) (⇑σ₂) (Sum.inl x)) (Sum.inl x)) *
        ∏ x, fromBlocks A B 0 D (Sum.inr (σ₂ x)) (Sum.inr x))

Tactic:
Sum.map_inl,

Goal state after:
case e'_3.refine_4
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m
σ₂ : Perm n
⊢ (↑↑(sign σ₁) * ∏ x, A (σ₁ x) x) * (↑↑(sign σ₂) * ∏ x, D (σ₂ x) x) =
    ↑↑(sign (σ₁.sumCongr σ₂)) *
      ((∏ x, fromBlocks A B 0 D (Sum.inl (σ₁ x)) (Sum.inl x)) * ∏ x, fromBlocks A B 0 D (Sum.inr (σ₂ x)) (Sum.inr x))
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
⊢ (∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c.π.app j)) x = s j) ↔
    ∀ (a : (j : J) → F.obj j) (b : a ∈ F.sections), ∃! a_1, sectionOfCone c a_1 = ⟨a, b⟩

Tactic:
F.sections_ext_iff,

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
⊢ (∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c.π.app j)) x = s j) ↔
    ∀ a ∈ F.sections, ∃! a_1, ∀ (j : J), ↑(sectionOfCone c a_1) j = a j
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
⊢ (ConcreteCategory.hom (lift F' ≫ F'.m)).toFun x = (ConcreteCategory.hom (ι f)).toFun x

Tactic:
change (F'.e ≫ F'.m) _ = _

Goal state after:
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
⊢ (ConcreteCategory.hom (F'.e ≫ F'.m))
      ↑(Classical.indefiniteDescription (fun x_1 ↦ (ConcreteCategory.hom f) x_1 = ↑x) ⋯) =
    (ConcreteCategory.hom (ι f)).toFun x
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommRingCat
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ F.map f ≫
      ofHom (RingCat.Hom.hom ((RingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ CommRingCat RingCat)).ι.app x✝)) =
    ofHom (RingCat.Hom.hom ((RingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ CommRingCat RingCat)).ι.app x✝¹)) ≫
      ((Functor.const J).obj (colimit F)).map f

Tactic:
by
        ext
        simpa using! (Types.TypeMax.colimitCocone (F ⋙ forget CommRingCat)).ι.naturality_apply f _

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w'
inst✝ : F.IsRepresentable
⊢ PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
    (uliftYoneda.{w', v, u}.obj (F ⋙ uliftFunctor.{v, w'}).reprX)

Tactic:
exact inferInstanceAs <| PreservesLimitsOfSize (yoneda.obj _ ⋙ uliftFunctor)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cone F
t : (k : K) → IsLimit (((evaluation K C).obj k).mapCone c)
s : Cone F
j : J
⊢ { app := fun k ↦ (t k).lift { pt := s.pt.obj k, π := whiskerRight s.π ((evaluation K C).obj k) }, naturality := ⋯ } ≫
      c.π.app j =
    s.π.app j

Tactic:
ext k; exact (t k).fac _ j

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cocone F
t : (k : K) → IsColimit (((evaluation K C).obj k).mapCocone c)
s : Cocone F
X Y : K
f : X ⟶ Y
j : J
⊢ (F.obj j).map f ≫
      (c.ι.app j).app Y ≫ (t Y).desc { pt := s.pt.obj Y, ι := whiskerRight s.ι ((evaluation K C).obj Y) } =
    { pt := s.pt.obj X, ι := whiskerRight s.ι ((evaluation K C).obj X) }.ι.app j ≫ s.pt.map f

Tactic:
(t Y).fac ⟨s.pt.obj _, whiskerRight s.ι _⟩ j

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cocone F
t : (k : K) → IsColimit (((evaluation K C).obj k).mapCocone c)
s : Cocone F
X Y : K
f : X ⟶ Y
j : J
⊢ (F.obj j).map f ≫ { pt := s.pt.obj Y, ι := whiskerRight s.ι ((evaluation K C).obj Y) }.ι.app j =
    { pt := s.pt.obj X, ι := whiskerRight s.ι ((evaluation K C).obj X) }.ι.app j ≫ s.pt.map f
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cocone F
t : (k : K) → IsColimit (((evaluation K C).obj k).mapCocone c)
s : Cocone F
j : J
⊢ c.ι.app j ≫
      { app := fun k ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι ((evaluation K C).obj k) },
        naturality := ⋯ } =
    s.ι.app j

Tactic:
ext k; exact (t k).fac _ j

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X✝ Y✝ Z X Y : C
f g : X ⟶ Y
h : (tensoringLeft C).map f = (tensoringLeft C).map g
⊢ f = g

Tactic:
injections h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X✝ Y✝ Z X Y : C
f g : X ⟶ Y
h : (fun Y_1 ↦ f ▷ Y_1) = fun Y_1 ↦ g ▷ Y_1
⊢ f = g
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X✝ Y✝ Z X Y : C
f g : X ⟶ Y
h : (tensoringRight C).map f = (tensoringRight C).map g
⊢ f = g

Tactic:
injections h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X✝ Y✝ Z X Y : C
f g : X ⟶ Y
h : (fun j ↦ ((curriedTensor C).obj j).map f) = fun j ↦ ((curriedTensor C).obj j).map g
⊢ f = g
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
X Y : D
f : X ⟶ Y
⊢ F.map (𝟙_ D ◁ f ≫ (λ_ Y).hom) = F.map ((λ_ X).hom ≫ f)

Tactic:
simp [fData.leftUnitor_eq, fData.whiskerLeft_eq, whisker_exchange_assoc]

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ μ G (F.obj X✝) (F.obj x✝) ≫ G.map (F.map x✝¹ ▷ F.obj x✝ ≫ μ F Y✝ x✝) =
    μ G (F.obj X✝) (F.obj x✝) ≫ G.map (μ F X✝ x✝ ≫ F.map (x✝¹ ▷ x✝))

Tactic:
μ_natural_left

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv =
    F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv ≫ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z

Tactic:
rw [← cancel_epi (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom, map_associator']

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ (μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z) ≫
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv =
    (μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z) ≫
      F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv ≫ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
⊢ CategoryTheory.inv (η F) = ε F

Tactic:
by
  rw [← εIso_hom, ← Iso.comp_inv_eq_id, εIso_inv, IsIso.inv_hom_id]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i j : C
η : g ⟶ h
ηs : i ⟶ j
ηs' : i ⊗ f ⟶ j ⊗ f
η₁ : g ⊗ i ⊗ f ⟶ h ⊗ j ⊗ f
η₂ : g ⊗ i ⊗ f ⟶ (h ⊗ j) ⊗ f
η₃ : (g ⊗ i) ⊗ f ⟶ (h ⊗ j) ⊗ f
e_ηs' : ηs ▷ f = ηs'
e_η₁ : (Iso.refl g).hom ≫ η ≫ (Iso.refl h).hom ⊗ₘ ηs' = η₁
e_η₂ : η₁ ≫ (α_ h j f).inv = η₂
e_η₃ : (α_ g i f).hom ≫ η₂ = η₃
⊢ (η ⊗ₘ ηs) ▷ f = η₃

Tactic:
simp [← e_ηs', ← e_η₁, ← e_η₂, ← e_η₃, MonoidalCategory.tensorHom_def]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h h' i i' : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
β : f' ≅ g'
θ : g' ⟶ h'
θs : h' ⟶ i'
ηθ : g ⊗ g' ⟶ h ⊗ h'
ηθs : h ⊗ h' ⟶ i ⊗ i'
ηθ₁ : g ⊗ g' ⟶ i ⊗ i'
ηθ₂ : f ⊗ f' ⟶ i ⊗ i'
e_ηθ : η ⊗ₘ θ = ηθ
e_ηθs : ηs ⊗ₘ θs = ηθs
e_ηθ₁ : ηθ ≫ ηθs = ηθ₁
e_ηθ₂ : (α ⊗ᵢ β).hom ≫ ηθ₁ = ηθ₂
⊢ α.hom ≫ η ≫ ηs ⊗ₘ β.hom ≫ θ ≫ θs = ηθ₂

Tactic:
simp [← e_ηθ, ← e_ηθs, ← e_ηθ₁, ← e_ηθ₂]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : C ⥤ D
⊢ (Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c) ≅ c.map G

Tactic:
by
      refine PullbackCone.ext (Iso.refl _) ?_ ?_
      · dsimp only [fst]
        simp
      · dsimp only [snd]
        simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).hom ≫ pullback.fst (G.map f) (G.map g) = G.map (pullback.fst f g)

Tactic:
by
  simp [PreservesPullback.iso]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).hom ≫ pullback.snd (G.map f) (G.map g) = G.map (pullback.snd f g)

Tactic:
by
  simp [PreservesPullback.iso]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ ∀ (j : WalkingSpan),
    ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι.app
          j ≫
        (Iso.refl
            ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
                (G.mapCocone (PushoutCocone.mk h k comm))).pt).hom =
      (PushoutCocone.mk (G.map h) (G.map k) ⋯).ι.app j

Tactic:
rintro (_ | _ | _) <;> dsimp

Goal state after:
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj W) ≫ G.map (f ≫ h)) ≫ 𝟙 (G.obj Z) = G.map f ≫ G.map h

case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj X) ≫ G.map h) ≫ 𝟙 (G.obj Z) = G.map h

case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj Y) ≫ G.map k) ≫ 𝟙 (G.obj Z) = G.map k
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : naturalityProperty app e.hom
⊢ naturalityProperty app e.inv

Tactic:
simp only [naturalityProperty] at he ⊢
  rw [← cancel_epi (F₁.map e.hom)]
  slice_rhs 1 2 => rw [he]
  simp only [Category.assoc, ← F₁.map_comp_assoc, ← F₂.map_comp, e.hom_inv_id, Functor.map_id,
    Category.id_comp, Category.comp_id]

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

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✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
f✝ : Y✝ ⟶ Z✝
⊢ (β_ (F.obj X✝) (F.obj Y✝)).hom ≫ F.map f✝ ▷ F.obj X✝ ≫ μ F Z✝ X✝ =
    (β_ (F.obj X✝) (F.obj Y✝)).hom ≫ μ F Y✝ X✝ ≫ F.map (f✝ ▷ X✝)

Tactic:
μ_natural_left

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
f✝ : Y✝ ⟶ Z✝
⊢ (β_ (F.obj X✝) (F.obj Y✝)).hom ≫ μ F Y✝ X✝ ≫ F.map (f✝ ▷ X✝) =
    (β_ (F.obj X✝) (F.obj Y✝)).hom ≫ μ F Y✝ X✝ ≫ F.map (f✝ ▷ X✝)
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasStrongEpiMonoFactorisations C
inst✝¹ : (forget C).PreservesMonomorphisms
inst✝ : (forget C).PreservesEpimorphisms
⊢ monomorphisms C ≤ MorphismProperty.injective C

Tactic:
rw [injective_eq_monomorphisms]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom = (ρ_ X).hom ▷ 𝟙_ C

Tactic:
triangle

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (ρ_ X).hom ▷ 𝟙_ C = (ρ_ X).hom ▷ 𝟙_ C
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ X (𝟙_ C)).hom = (ρ_ X).hom ≫ (λ_ X).inv

Tactic:
by
  simp [← rightUnitor_inv_braiding]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
⊢ (λ_ (X₁ ⊗ X₂)).hom = (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ tensorμ (𝟙_ C) (𝟙_ C) X₁ X₂ ≫ ((λ_ X₁).hom ⊗ₘ (λ_ X₂).hom)

Tactic:
by
  dsimp only [tensorμ]
  have :
    ((λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂)) ≫
        (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ (𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv) =
      𝟙_ C ◁ (λ_ X₁).inv ▷ X₂ := by
    simp
  slice_rhs 1 3 => rw [this]
  clear this
  slice_rhs 1 2 => rw [← whiskerLeft_comp, ← comp_whiskerRight,
    leftUnitor_inv_braiding]
  simp [tensorHom_def]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j : J
x : ↑((F ⋙ uliftFunctor).obj j)
⊢ (quotUliftToQuot F) ((Quot.ι (F ⋙ uliftFunctor) j) x) = (Quot.ι F j) x.down

Tactic:
dsimp [quotUliftToQuot, Quot.ι]
  conv_lhs => erw [AddMonoidHom.comp_apply (QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor)))
    (DFinsupp.singleAddHom _ j), QuotientAddGroup.lift_mk']
  simp only [DFinsupp.singleAddHom_apply,
    DFinsupp.sumAddHom_single, AddMonoidHom.coe_comp, Function.comp_apply]
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ toTensor (ι R m) = (TensorAlgebra.ι R) m

Tactic:
simp [toTensor]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2.inr.inr
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
ha : a.fst ≠ 0
hb : b.fst ≠ 0
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
      -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))

Tactic:
rw [inv_mul_cancel_right₀ ha, mul_inv_cancel_left₀ hb]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
⊢ x * x⁻¹ * x⁻¹⁻¹ = x

Tactic:
by
      rw [mul_assoc, TrivSqZeroExt.mul_inv_cancel, mul_one]
      rw [fst_inv]
      apply inv_ne_zero hx

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x : ↑X
⊢ 1 • (ConcreteCategory.hom g) x = (Hom.hom g) x

Tactic:
rw [one_smul]

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a : α
this : a + a = a + a + (a + a)
⊢ a + a = 0

Tactic:
right_eq_add

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a : α
this : a + a = 0
⊢ a + a = 0
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a + a * b + (b * a + b) = a + b + (a * b + b * a)

Tactic:
by abel

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Bialgebra R B
inst✝ : Algebra R A
x : B
⊢ ((↑(comulAlgHom A (A ⊗[R] B))).comp ↑Algebra.TensorProduct.includeRight) x =
    ((Algebra.TensorProduct.mapRingHom (algebraMap R A) ↑Algebra.TensorProduct.includeRight
            ↑Algebra.TensorProduct.includeRight ⋯ ⋯).comp
        ↑(comulAlgHom R B))
      x

Tactic:
simp [← (ℛ R x).eq, TensorProduct.tmul_sum]

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a \ b) = f a \ f b

Tactic:
sdiff_eq,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a ⊓ bᶜ) = f a \ f b
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a ⊓ bᶜ) = f a \ f b

Tactic:
sdiff_eq,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a ⊓ bᶜ) = f a ⊓ (f b)ᶜ
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
⊢ (algebraMap R S) x * invSelf x = 1

Tactic:
convert! IsLocalization.mk'_mul_mk'_eq_one (M := Submonoid.powers x) (S := S) _ 1
  symm
  apply IsLocalization.mk'_one

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
z : S
⊢ ∃ n a, z * (algebraMap R S) x ^ n = (algebraMap R S) a

Tactic:
by
  obtain ⟨⟨a, ⟨-, n, rfl⟩⟩, h⟩ := IsLocalization.surj (Submonoid.powers x) z
  use n, a
  simpa using h

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℕ
h : n < m
⊢ (algebraMap R B) (↑(Submonoid.pow x m) * 1) = (algebraMap R B) (↑(Submonoid.pow x (m - n)) * x ^ n)

Tactic:
simp [Submonoid.pow_apply, ← pow_add, Nat.sub_add_cancel h.le]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
⊢ ((λ_ (𝟙_ C)).inv ⊗ₘ 𝟙 (𝟙_ C)) ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom ≫ (η ⊗ₘ η ⊗ₘ η) = η ⊗ₘ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
slice_rhs 1 2 => rw [← Category.id_comp η, ← tensorHom_comp_tensorHom]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
⊢ ((λ_ (𝟙_ C)).inv ⊗ₘ 𝟙 (𝟙_ C)) ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom ≫ (η ⊗ₘ η ⊗ₘ η) =
    (𝟙 (𝟙_ C) ⊗ₘ (λ_ (𝟙_ C)).inv) ≫ (η ⊗ₘ η ⊗ₘ η)