mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
⊢ ∀ a₁ ∈ univ, ∀ a₂ ∈ univ, ((prodCongrLeft fun k ↦ a₁ k ⋯) = prodCongrLeft fun k ↦ a₂ k ⋯) → a₁ = a₂

pp: case refine_3
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
⊢ ∀ b ∈ preserving_snd, ∃ a, ∃ (_ : a ∈ univ), (prodCongrLeft fun k ↦ a k ⋯) = b

pp: case refine_4
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
⊢ ∀ a ∈ univ,
    ∏ x, ↑↑(sign (a x ⋯)) * ∏ x_1, M x ((a x ⋯) x_1) x_1 =
      ↑↑(sign (prodCongrLeft fun k ↦ a k ⋯)) * ∏ i, blockDiagonal M ((prodCongrLeft fun k ↦ a k ⋯) i) i

Tactic:
· intro σ _ σ' _ eq
      ext x hx k
      have :
        ∀ k x,
          prodCongrLeft (fun k => σ k (Finset.mem_univ _)) (k, x) =
            prodCongrLeft (fun k => σ' k (Finset.mem_univ _)) (k, x) :=
        fun k x => by rw [eq]
      simp only [prodCongrLeft_apply, Prod.mk_inj] at this
      exact (this k x).1

Goal state after:
case refine_3
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
⊢ ∀ b ∈ preserving_snd, ∃ a, ∃ (_ : a ∈ univ), (prodCongrLeft fun k ↦ a k ⋯) = b

case refine_4
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
⊢ ∀ a ∈ univ,
    ∏ x, ↑↑(sign (a x ⋯)) * ∏ x_1, M x ((a x ⋯) x_1) x_1 =
      ↑↑(sign (prodCongrLeft fun k ↦ a k ⋯)) * ∏ i, blockDiagonal M ((prodCongrLeft fun k ↦ a k ⋯) i) i
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ 0 * Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j, x⟩ = 0

Tactic:
erw [colimit_zero_eq _ j, colimit_mul_mk_eq _ ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j)]

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
      ⟨j,
        (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map (𝟙 j))) ⟨j, 0⟩.snd *
          (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map (𝟙 j))) ⟨j, x⟩.snd⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x y : M F
⊢ M F

Tactic:
refine Quot.lift₂ (colimitMulAux F) ?_ ?_ x y
    · intro x y y' h
      apply colimitMulAux_eq_of_rel_right
      apply Types.FilteredColimit.rel_of_colimitTypeRel
      exact h
    · intro x x' y h
      apply colimitMulAux_eq_of_rel_left
      apply Types.FilteredColimit.rel_of_colimitTypeRel
      exact h

Goal state after:
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j, x⟩ * 0 = 0

Tactic:
erw [colimit_zero_eq _ j, colimit_mul_mk_eq _ ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j)]

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
      ⟨j,
        (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map (𝟙 j))) ⟨j, x⟩.snd *
          (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map (𝟙 j))) ⟨j, 0⟩.snd⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
x : ↑(F.obj j)
⊢ M.mk F ⟨j, x * 1⟩ = M.mk F ⟨j, x⟩

Tactic:
mul_one

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
x : ↑(F.obj j)
⊢ M.mk F ⟨j, x⟩ = M.mk F ⟨j, x⟩
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹⁰ : CommSemiring R
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
f f' : MultilinearMap R M₁ M₂
A : Type u_1
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → A
i : ι
x y : A
⊢ ∏ i_1, update m i (x + y) i_1 = ∏ i_1, update m i x i_1 + ∏ i_1, update m i y i_1

Tactic:
simp [Finset.prod_update_of_mem, add_mul]

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

Goal state before:
pp: case refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
x✝ : Nonempty (IsLimit c)
s : (j : J) → F.obj j
hs : s ∈ F.sections
t : IsLimit c
⊢ ∃! x, ∀ (j : J), (hom (c.π.app j)) x = s j

Tactic:
let cs := coneOfSection hs
    exact ⟨t.lift cs ⟨⟩, fun j ↦ congr_hom (t.fac cs j) ⟨⟩,
      fun x hx ↦ congr_hom (CC := fun X ↦ X)
        (t.uniq cs (↾fun _ ↦ x) fun j ↦ by ext; exact hx j) ⟨⟩⟩

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

Goal state before:
pp: case neg.inr
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
hji : ¬j < i
hij : i ≠ j
⊢ (if i = j then s.piecewise a v j - b j else b j) = if j = i then a j - b j else b j

Tactic:
rw [if_neg hij, if_neg hij.symm]

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
inst✝ : HasLimitsOfShape J C
F G : J ⥤ K ⥤ C
η : F ⟶ G
k : K
j : J
⊢ ((flipFunctor J K C ⋙ (whiskeringRight K (J ⥤ C) C).obj lim).map η ≫ (limitIsoFlipCompLim G).symm.hom).app k ≫
      (limit.π G j).app k =
    ((limitIsoFlipCompLim F).symm.hom ≫ lim.map η).app k ≫ (limit.π G j).app k

Tactic:
simp [comp_evaluation, ← NatTrans.comp_app (limMap η)]

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
J : Type u_1
inst✝² : Category.{v_1, u_1} J
F : J ⥤ AlgCat R
inst✝¹ : PreservesColimitsOfShape J (forget RingCat)
c : Cocone (F ⋙ forget₂ (AlgCat R) RingCat)
inst✝ : IsFilteredOrEmpty J
hc : IsColimit c
j : J
s : Cocone F
m : (coconeOfIsFiltered hc j).pt ⟶ s.pt
hm : ∀ (j_1 : J), (coconeOfIsFiltered hc j).ι.app j_1 ≫ m = s.ι.app j_1
⊢ m =
    ofHom
      (let __spread.0 := RingCat.Hom.hom (hc.desc ((forget₂ (AlgCat R) RingCat).mapCocone s));
      { toRingHom := __spread.0, commutes' := ⋯ })

Tactic:
by
    ext
    refine congr($(hc.uniq (Functor.mapCocone _ s) ((forget₂ _ _).map m) fun j ↦ ?_) _)
    ext
    exact congr($(hm _) _)

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

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
X✝ Y✝ Z✝ : ι
hij : X✝ ⟶ Y✝
hjk : Y✝ ⟶ Z✝
x✝ : ↑(of R (G X✝))
⊢ (Hom.hom (↟(f X✝ Y✝ ⋯) ≫ ↟(f Y✝ Z✝ ⋯))) x✝ = (Hom.hom (↟(f X✝ Z✝ ⋯))) x✝

Tactic:
apply Module.DirectedSystem.map_map f

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

Goal state before:
pp: case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ L.map ((h.homEquiv X (L.obj Y)) f ≫ section_ (h.unit.app Y)) = f

Tactic:
suffices L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y) by simp [this]

Goal state after:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y)
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₁ X₂ Y₂ : D
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ (fData.μIso X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (fData.μIso Y₁ Y₂).hom =
    ((fData.μIso X₁ X₂).inv ≫ F.map f ▷ F.obj X₂ ≫ (fData.μIso Y₁ X₂).hom) ≫
      (fData.μIso Y₁ X₂).inv ≫ F.obj Y₁ ◁ F.map g ≫ (fData.μIso Y₁ Y₂).hom

Tactic:
simp only [tensorHom_def, assoc, Iso.hom_inv_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
h : ∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)
X Y : C
f : X ⟶ Y
r : R
⊢ F.map (r • f) = r • F.map f

Tactic:
have : r • f = (r • 𝟙 X) ≫ f := by simp

Goal state after:
case mpr
R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
h : ∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)
X Y : C
f : X ⟶ Y
r : R
this : r • f = (r • 𝟙 X) ≫ f
⊢ F.map (r • f) = r • F.map f
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
f✝ g✝ : Y✝ ⟶ Z✝
⊢ F.map ((f✝ + g✝) ▷ X✝) = F.map (f✝ ▷ X✝ + g✝ ▷ X✝)

Tactic:
simp only [Functor.Monoidal.map_whiskerRight, Functor.map_add, Preadditive.comp_add,
        Preadditive.add_comp, MonoidalPreadditive.add_whiskerRight]

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

Goal state before:
pp: M : Type u
inst✝² : Monoid M
N : Type u'
inst✝¹ : Monoid N
K : Type u
inst✝ : Monoid K
F : M →* N
G : N →* K
x✝¹ x✝ : Discrete M
⊢ μ (monoidalFunctor F ⋙ monoidalFunctor G) x✝¹ x✝ ≫ (monoidalFunctorComp F G).hom.app (x✝¹ ⊗ x✝) =
    ((monoidalFunctorComp F G).hom.app x✝¹ ⊗ₘ (monoidalFunctorComp F G).hom.app x✝) ≫
      μ (monoidalFunctor (G.comp F)) x✝¹ x✝

Tactic:
dsimp only [comp_μ, monoidalFunctorComp, Iso.refl, Discrete.monoidalFunctor_μ]

Goal state after:
M : Type u
inst✝² : Monoid M
N : Type u'
inst✝¹ : Monoid N
K : Type u
inst✝ : Monoid K
F : M →* N
G : N →* K
x✝¹ x✝ : Discrete M
⊢ (Discrete.eqToHom ⋯ ≫ (monoidalFunctor G).map (Discrete.eqToHom ⋯)) ≫
      (𝟙 (monoidalFunctor F ⋙ monoidalFunctor G)).app (x✝¹ ⊗ x✝) =
    ((𝟙 (monoidalFunctor F ⋙ monoidalFunctor G)).app x✝¹ ⊗ₘ (𝟙 (monoidalFunctor F ⋙ monoidalFunctor G)).app x✝) ≫
      Discrete.eqToHom ⋯
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ⟶ g
η' θ' : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
η_hom : η'.hom = η
Θ_hom : θ'.hom = θ
Hη : 𝟙_ C ◁ η' ≪≫ η_g = η_f
Hθ : 𝟙_ C ◁ θ' ≪≫ η_g = η_f
⊢ η'.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom

Tactic:
by
      simp [← reassoc_of% (congrArg Iso.hom Hη)]

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 : C
η : f ⟶ g
η₁ : f ⟶ 𝟙_ C ⊗ g
η₂ : 𝟙_ C ⊗ f ⟶ 𝟙_ C ⊗ g
e_η₁ : η ≫ (λ_ g).inv = η₁
e_η₂ : (λ_ f).hom ≫ η₁ = η₂
⊢ 𝟙_ C ◁ η = η₂

Tactic:
by
  simp [e_η₁, e_η₂]

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 : C
η : f ⟶ g
η₁ : f ⟶ g ⊗ 𝟙_ C
η₂ : f ⊗ 𝟙_ C ⟶ g ⊗ 𝟙_ C
e_η₁ : η ≫ (ρ_ g).inv = η₁
e_η₂ : (ρ_ f).hom ≫ η₁ = η₂
⊢ η ▷ 𝟙_ C = η₂

Tactic:
by
  simp [e_η₁, e_η₂]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
⊢ HasColimitsOfShape J Cᵒᵖ ↔ HasLimitsOfShape Jᵒᵖ C

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
  have : HasColimitsOfShape Jᵒᵖᵒᵖ Cᵒᵖ := hasColimitsOfShape_of_equivalence (opOpEquivalence J).symm
  exact hasLimitsOfShape_of_hasColimitsOfShape_op

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.obj X✝) (F.obj Y✝) (F.obj Z✝)).hom ≫
      F.obj X✝ ◁ μ F Y✝ Z✝ ≫ μ F X✝ (Y✝ ⊗ Z✝) ≫ F.map (β X✝ (Y✝ ⊗ Z✝)).hom ≫ F.map (α_ Y✝ Z✝ X✝).hom =
    (β_ (F.obj X✝) (F.obj Y✝)).hom ▷ F.obj Z✝ ≫
      (α_ (F.obj Y✝) (F.obj X✝) (F.obj Z✝)).hom ≫
        F.obj Y✝ ◁ ((β_ (F.obj X✝) (F.obj Z✝)).hom ≫ μ F Z✝ X✝) ≫ μ F Y✝ (Z✝ ⊗ X✝)

Tactic:
whiskerLeft_comp_assoc,

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.obj X✝) (F.obj Y✝) (F.obj Z✝)).hom ≫
      F.obj X✝ ◁ μ F Y✝ Z✝ ≫ μ F X✝ (Y✝ ⊗ Z✝) ≫ F.map (β X✝ (Y✝ ⊗ Z✝)).hom ≫ F.map (α_ Y✝ Z✝ X✝).hom =
    (β_ (F.obj X✝) (F.obj Y✝)).hom ▷ F.obj Z✝ ≫
      (α_ (F.obj Y✝) (F.obj X✝) (F.obj Z✝)).hom ≫
        F.obj Y✝ ◁ (β_ (F.obj X✝) (F.obj Z✝)).hom ≫ F.obj Y✝ ◁ μ F Z✝ X✝ ≫ μ F Y✝ (Z✝ ⊗ X✝)
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.obj X✝ ◁ μ F Y✝ Z✝ ≫
      μ F X✝ (Y✝ ⊗ Z✝) ≫ F.map (α_ X✝ Y✝ Z✝).inv ≫ F.map (β (X✝ ⊗ Y✝) Z✝).hom ≫ F.map (α_ Z✝ X✝ Y✝).inv =
    F.obj X✝ ◁ ((β_ (F.obj Y✝) (F.obj Z✝)).hom ≫ μ F Z✝ Y✝) ≫
      μ F X✝ (Z✝ ⊗ Y✝) ≫ F.map (α_ X✝ Z✝ Y✝).inv ≫ F.map ((β X✝ Z✝).hom ▷ Y✝)

Tactic:
whiskerLeft_comp_assoc,

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.obj X✝ ◁ μ F Y✝ Z✝ ≫
      μ F X✝ (Y✝ ⊗ Z✝) ≫ F.map (α_ X✝ Y✝ Z✝).inv ≫ F.map (β (X✝ ⊗ Y✝) Z✝).hom ≫ F.map (α_ Z✝ X✝ Y✝).inv =
    F.obj X✝ ◁ (β_ (F.obj Y✝) (F.obj Z✝)).hom ≫
      F.obj X✝ ◁ μ F Z✝ Y✝ ≫ μ F X✝ (Z✝ ⊗ Y✝) ≫ F.map (α_ X✝ Z✝ Y✝).inv ≫ F.map ((β X✝ Z✝).hom ▷ Y✝)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
| (β_ X (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).hom ▷ X

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
| (β_ X (𝟙_ C)).inv

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
| (α_ X (𝟙_ C) (𝟙_ C)).hom

Tactic:
← braiding_naturality_right

Goal state after:
case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
| X ◁ (λ_ (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).hom

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
| (β_ X (𝟙_ C)).inv

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
| (α_ X (𝟙_ C) (𝟙_ C)).hom
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

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

Tactic:
μ_natural_right,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : F.LaxBraided
W X Y Z : C
⊢ (α_ (F.obj W) (F.obj X) (F.obj Y ⊗ F.obj Z)).hom ≫
      F.obj W ◁ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫
        (α_ (F.obj W) (F.obj X ⊗ F.obj Y) (F.obj Z)).inv ≫
          (F.obj W ◁ μ F X Y ≫ μ F W (X ⊗ Y) ≫ F.map (W ◁ (β_ X Y).hom)) ▷ F.obj Z ≫
            μ F (W ⊗ Y ⊗ X) Z ≫ F.map ((α_ W Y X).inv ▷ Z) ≫ F.map (α_ (W ⊗ Y) X Z).hom =
    (μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (W ⊗ X) (Y ⊗ Z) ≫
        F.map
          ((α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ W ◁ (β_ X Y).hom ▷ Z ≫ W ◁ (α_ Y X Z).hom ≫ (α_ W Y (X ⊗ Z)).inv)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : RingCon N
e : M ≃+* N
h : c = d.comap e
⊢ ∀ (x y : c.Quotient),
    (Quotient.congr ↑e ⋯).toFun (x * y) = (Quotient.congr ↑e ⋯).toFun x * (Quotient.congr ↑e ⋯).toFun y

Tactic:
by rintro ⟨x⟩ ⟨y⟩; exact congrArg toQuotient (e.map_mul x y)

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 * 1 = x

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⁻¹.fst ≠ 0

Tactic:
mul_one

Goal state after:
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

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⁻¹.fst ≠ 0
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
M₁ M₂ M₃ : ModuleCat R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x : ↑(obj' f M₁)
⊢ (Hom.hom (map' f (l₁₂ ≫ l₂₃))) x = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) x

Tactic:
induction x using TensorProduct.induction_on with

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
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
s : S
m : ↑M
⊢ s ⊗ₜ[R] m = (s * 1) ⊗ₜ[R] m

Tactic:
mul_one

Goal state after:
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
s : S
m : ↑M
⊢ s ⊗ₜ[R] m = s ⊗ₜ[R] m
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
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this✝ : Algebra R S := f.toAlgebra
s : S
m : ↑M
this : s ⊗ₜ[R] m = s • 1 ⊗ₜ[R] m
⊢ (ConcreteCategory.hom α) (s ⊗ₜ[R] m) = (ConcreteCategory.hom β) (s ⊗ₜ[R] m)

Tactic:
simp only [this, map_smul, h]

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
x : ↑((extendScalars f).obj X)
⊢ (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) x =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) x

Tactic:
induction x using TensorProduct.induction_on with

Goal state after: