mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Tactic:
by_cases hfa : (f ^ a) x ∈ f.support

Goal state after:
case pos
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∈ f.support
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∉ f.support
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
x y : α
hab : x ≠ y
⊢ (swap x y ^ 1) x = y

Tactic:
by rw [zpow_one, swap_apply_left]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ _root_.Set.univ = {x | (f.subtypePerm ⋯) x ≠ x}

Tactic:
rw [eq_comm, Set.eq_univ_iff_forall]

Goal state after:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ ∀ (x : { x // x ∈ s }), x ∈ {x | (f.subtypePerm ⋯) x ≠ x}
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
g : Perm α
s : Set α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
h : g.IsCycleOn s
⊢ ∀ ⦃x : β⦄, x ∈ Subtype.val ∘ ⇑f '' s → ∀ ⦃y : β⦄, y ∈ Subtype.val ∘ ⇑f '' s → (g.extendDomain f).SameCycle x y

Tactic:
by
    rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩
    exact (h.2 ha hb).extendDomain

Goal state after:
Module: Mathlib.GroupTheory.Perm.Option

Goal state before:
pp: case some.some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : σ (some x) = some val✝
hn : σ (some x) ≠ none
hσn : σ (some x) ≠ σ none
⊢ Option.map (⇑(removeNone σ)) (some x) = (swap none (σ none)) (some val✝)

Tactic:
simp [removeNone_some _ ⟨_, h⟩, ← h, swap_apply_of_ne_of_ne hn hσn]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
⊢ (finRotate (n + 2)).cycleType = {n + 2}

Tactic:
rw [isCycle_finRotate.cycleType, support_finRotate, ← Fintype.card, Fintype.card_fin]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case inr
n : ℕ
inst✝ : NeZero n
j : Fin n
hj : 0 < j
⊢ ↑((cycleRange 0) j) = ↑(1 j)

Tactic:
rw [cycleRange_of_gt hj, one_apply]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case pos
n : ℕ
i j k : Fin n
h : k < i
hij : i ≤ j
⊢ (i.cycleIcc j) k = k

Tactic:
simpa [hij] using Perm.extendDomain_apply_not_subtype _ _ (by
      simp [range_natAdd_castLEEmb]; lia)

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ ∀ (σ τ : Perm α),
    σ.Disjoint τ →
      σ.IsCycle →
        (∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}) →
          (∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}) →
            ∀ {f : Perm α},
              f ∈ (σ * τ).cycleFactorsFinset → (σ * τ * f⁻¹).cycleFactorsFinset = (σ * τ).cycleFactorsFinset \ {f}

Tactic:
· intro σ τ hd _ hσ hτ f
    simp_rw [hd.cycleFactorsFinset_mul_eq_union, mem_union]
    -- if only `wlog` could work here...
    rintro (hf | hf)
    · rw [hd.commute.eq, union_comm, union_sdiff_distrib, sdiff_singleton_eq_erase,
        erase_eq_of_notMem, mul_assoc, Disjoint.cycleFactorsFinset_mul_eq_union, hσ hf]
      · rw [mem_cycleFactorsFinset_iff] at hf
        intro x
        rcases hd.symm x with hx | hx
        · exact Or.inl hx
        · refine Or.inr ?_
          by_cases hfx : f x = x
          · rw [← hfx]
            simpa [hx] using hfx.symm
          · rw [mul_apply]
            rw [← hf.right _ (mem_support.mpr hfx)] at hx
            contradiction
      · exact fun H =>
        notMem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem hf H))
    · rw [union_sdiff_distrib, sdiff_singleton_eq_erase, erase_eq_of_notMem, mul_assoc,
        Disjoint.cycleFactorsFinset_mul_eq_union, hτ hf]
      · rw [mem_cycleFactorsFinset_iff] at hf
        intro x
        rcases hd x with hx | hx
        · exact Or.inl hx
        · refine Or.inr ?_
          by_cases hfx : f x = x
          · rw [← hfx]
            simpa [hx] using hfx.symm
          · rw [mul_apply]
            rw [← hf.right _ (mem_support.mpr hfx)] at hx
            contradiction
      · exact fun H =>
        notMem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem H hf))

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
A : Matrix n n R
inst✝ : IsEmpty n
⊢ ∑ σ ∈ ofSign 1, ∏ k, A k (σ k) = 1

Tactic:
sum_unique_nonempty _ _ ⟨1, _⟩

Goal state after:
n : Type u_1
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
A : Matrix n n R
inst✝ : IsEmpty n
⊢ ∏ k, A k (default k) = 1

n : Type u_1
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
A : Matrix n n R
inst✝ : IsEmpty n
⊢ 1 ∈ ofSign 1
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
⊢ f ((insert i t).piecewise (m + m') m') = ∑ s ∈ (insert i t).powerset, f (s.piecewise m m')

Tactic:
have A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i) :=
    t.piecewise_insert _ _ _

Goal state after:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
⊢ f ((insert i t).piecewise (m + m') m') = ∑ s ∈ (insert i t).powerset, f (s.piecewise m m')
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: m : Type u_1
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M N : Matrix m m R
⊢ (M * N).det = (N * M).det

Tactic:
by
  rw [det_mul, det_mul, mul_comm]

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
w : (hom (colimit.ι F j)) x = (hom (colimit.ι F j')) x'
⊢ Quot.mk F.ColimitTypeRel ⟨j, x⟩ = Quot.mk F.ColimitTypeRel ⟨j', x'⟩

Tactic:
simpa using! congr_arg (colimitEquivColimitType F) w

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

Goal state before:
pp: case refine_3.refine_1
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
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ.symm x).2 = x.2
mk_apply_eq : ∀ (k : o) (x : n), ((σ (x, k)).1, k) = σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((σ.symm (x, k)).1, k) = σ.symm (x, k)
k : o
x✝ : k ∈ univ
⊢ LeftInverse (fun x ↦ (σ.symm (x, k)).1) fun x ↦ (σ (x, k)).1

Tactic:
intro x
        simp [mk_apply_eq]

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
⊢ MultilinearMap.mkPiRing R ι 0 = 0

Tactic:
ext; rw [mkPiRing_apply, smul_zero, zero_apply]

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

Goal state before:
pp: 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✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ f (update m i (x + -y)) = f (update m i x) + -f (update m i y)

Tactic:
MultilinearMap.map_update_add,

Goal state after:
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✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ f (update m i x) + f (update m i (-y)) = f (update m i x) + -f (update m i y)
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case insert
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 : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ f a - f ((insert k s).piecewise b a) =
    ∑ i ∈ insert k s, f fun j ↦ if j ∈ insert k s → j < i then a j else if i = j then a j - b j else b j

Tactic:
rw [Finset.piecewise_insert, map_update, ← sub_add, ih,
      add_comm, sum_insert (lt_irrefl _ <| hk k ·)]

Goal state after:
case insert
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 : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ (f (update (s.piecewise b a) k (s.piecewise b a k - b k)) +
      ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j) =
    (f fun j ↦ if j ∈ insert k s → j < k then a j else if k = j then a j - b j else b j) +
      ∑ x ∈ s, f fun j ↦ if j ∈ insert k s → j < x then a j else if x = j then a j - b j else b j
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ A.det = ∑ j, (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det

Tactic:
by
  rw [← det_transpose A, det_succ_column_zero]
  refine Finset.sum_congr rfl fun i _ => ?_
  rw [← det_transpose]
  simp only [transpose_apply, transpose_submatrix, transpose_transpose]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝¹ : Category.{w', w} J
F : J ⥤ C
inst✝ : PreservesLimit F G
c₁ c₂ : Cone F
t : IsLimit c₁
⊢ ∀ (j : J), G.map (t.lift c₂) ≫ (G.mapCone c₁).π.app j = (G.mapCone c₂).π.app j

Tactic:
simp [← G.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝¹ : Category.{w', w} J
F : J ⥤ C
inst✝ : PreservesLimit F G
c₁ c₂ : Cone F
t : IsLimit c₁
⊢ ∀ (j : J), G.map (t.lift c₂) ≫ (G.mapCone c₁).π.app j = (G.mapCone c₂).π.app j

Tactic:
by simp [← G.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝² : Category.{w', w} J
F : J ⥤ C
inst✝¹ : PreservesLimit F G
inst✝ : HasLimit F
t : Cone F
j✝ : J
⊢ (G.map (limit.lift F t) ≫ (preservesLimitIso G F).hom) ≫ limit.π (F ⋙ G) j✝ =
    limit.lift (F ⋙ G) (G.mapCone t) ≫ limit.π (F ⋙ G) j✝

Tactic:
simp [← G.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝¹ : Category.{w', w} J
F : J ⥤ C
inst✝ : PreservesColimit F G
c₁ c₂ : Cocone F
t : IsColimit c₁
⊢ ∀ (j : J), (G.mapCocone c₁).ι.app j ≫ G.map (t.desc c₂) = (G.mapCocone c₂).ι.app j

Tactic:
simp [← G.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝¹ : Category.{w', w} J
F : J ⥤ C
inst✝ : PreservesColimit F G
c₁ c₂ : Cocone F
t : IsColimit c₁
⊢ ∀ (j : J), (G.mapCocone c₁).ι.app j ≫ G.map (t.desc c₂) = (G.mapCocone c₂).ι.app j

Tactic:
by simp [← G.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝² : Category.{w', w} J
F : J ⥤ C
inst✝¹ : PreservesColimit F G
inst✝ : HasColimit F
t : Cocone F
j✝ : J
⊢ colimit.ι (F ⋙ G) j✝ ≫ (preservesColimitIso G F).inv ≫ G.map (colimit.desc F t) =
    colimit.ι (F ⋙ G) j✝ ≫ colimit.desc (F ⋙ G) (G.mapCocone t)

Tactic:
simp [← G.map_comp]

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

Goal state before:
pp: B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F₁ F₂ : B ⥤ C ⥤ D
h : uncurry.obj F₁ = uncurry.obj F₂
⊢ F₁ = F₂

Tactic:
rw [← curry_obj_uncurry_obj F₁, ← curry_obj_uncurry_obj F₂, h]

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
Y Y' : Cᵒᵖ
g : Y ⟶ Y'
f : (shrinkYoneda.{w, v, u}.obj X).obj Y
⊢ shrinkYonedaObjObjEquiv ((ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj X).map g)) f) =
    g.unop ≫ shrinkYonedaObjObjEquiv f

Tactic:
simp [shrinkYonedaObjObjEquiv, shrinkYoneda]

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

Goal state before:
pp: case refine_5
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
r : R
j : J
⊢ ↑⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) ((algebraMap R ↑s.1) r), ⋯⟩ j =
    ↑((algebraMap R ↥(sectionsSubalgebra F)) r) j

Tactic:
exact (s.π.app j).hom.commutes r

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
X₁ : C₁
X₂ Y₂ : C₂
φ✝ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
φ : X₃ ⟶ Y₃
⊢ { obj := fun X₃ ↦ (F.obj X₁).obj ((G₂₃.obj X₂).obj X₃), map := fun {X Y} φ ↦ (F.obj X₁).map ((G₂₃.obj X₂).map φ),
            map_id := ⋯, map_comp := ⋯ }.map
        φ ≫
      (F.obj X₁).map ((G₂₃.map φ✝).app Y₃) =
    (F.obj X₁).map ((G₂₃.map φ✝).app X₃) ≫
      { obj := fun X₃ ↦ (F.obj X₁).obj ((G₂₃.obj Y₂).obj X₃), map := fun {X Y} φ ↦ (F.obj X₁).map ((G₂₃.obj Y₂).map φ),
            map_id := ⋯, map_comp := ⋯ }.map
        φ

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

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
ε : 𝟙_ D ⟶ F.obj (𝟙_ C)
μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (Y ⊗ Z)
left_unitality : ∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom
right_unitality : ∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom
X : C
⊢ (λ_ (F.obj X)).hom = ε ▷ F.obj X ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom

Tactic:
by
    simp_rw [← tensorHom_id, left_unitality]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X₁ : SemimoduleCat R
X₂ : SemimoduleCat R
X₃ : SemimoduleCat R
Y₁ : SemimoduleCat R
Y₂ : SemimoduleCat R
Y₃ : SemimoduleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ Hom.hom (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom) =
    Hom.hom ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃))

Tactic:
apply TensorProduct.ext_threefold

Goal state after:
R : Type u
inst✝ : CommSemiring R
X₁ : SemimoduleCat R
X₂ : SemimoduleCat R
X₃ : SemimoduleCat R
Y₁ : SemimoduleCat R
Y₂ : SemimoduleCat R
Y₃ : SemimoduleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ∀ (x : ↑X₁) (y : ↑X₂) (z : ↑X₃),
    (Hom.hom (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃))) (x ⊗ₜ[R] y ⊗ₜ[R] z)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
⊢ Hom.hom ((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom) =
    Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))

Tactic:
apply TensorProduct.ext_threefold

Goal state after:
R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
⊢ ∀ (x : ↑M) (y : ↑(of R R)) (z : ↑N),
    (Hom.hom ((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))) (x ⊗ₜ[R] y ⊗ₜ[R] 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:
← εIso_hom,

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
⊢ CategoryTheory.inv (η F) = (εIso F).hom
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
⊢ Hom.hom ((α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) =
    Hom.hom ((X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom)

Tactic:
apply TensorProduct.ext_threefold

Goal state after:
R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
⊢ ∀ (x : ↑X) (y : ↑Y) (z : ↑Z),
    (Hom.hom ((α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom ((X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
⊢ Hom.hom ((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv) =
    Hom.hom ((α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y)

Tactic:
apply TensorProduct.ext_threefold

Goal state after:
R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
⊢ ∀ (x : ↑X) (y : ↑Y) (z : ↑Z),
    (Hom.hom ((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom ((α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y)) (x ⊗ₜ[R] y ⊗ₜ[R] 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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
x✝ : C
⊢ 𝟙 (F.obj x✝ ⊗ 𝟙_ D) = F.obj x✝ ◁ h.εIso.hom ≫ F.obj x✝ ◁ h.εIso.inv

Tactic:
whiskerLeft_hom_inv

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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
x✝ : C
⊢ 𝟙 (F.obj x✝ ⊗ 𝟙_ D) = 𝟙 (F.obj x✝ ⊗ 𝟙_ D)
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
h : F.CoreMonoidal
inst✝² : F.OplaxMonoidal
inst✝¹ : IsIso (η F)
inst✝ : ∀ (X Y : C), IsIso (δ F X Y)
X : C
⊢ (λ_ (F.obj X)).hom = (asIso (η F)).symm.hom ▷ F.obj X ≫ (asIso (δ F (𝟙_ C) X)).symm.hom ≫ F.map (λ_ X).hom

Tactic:
by simp [← cancel_epi (λ_ (F.obj X)).inv]

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
x✝ : HasColimitsOfShape J C
this : HasColimitsOfShape Jᵒᵖᵒᵖ C
⊢ HasLimitsOfShape Jᵒᵖ Cᵒᵖ

Tactic:
exact hasLimitsOfShape_op_of_hasColimitsOfShape

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
g : Y✝ ⟶ Z✝
x✝ : C
f : X✝ ⟶ x✝
hf : W.multiplicativeClosure f
⊢ W.multiplicativeClosure (f ≫ 𝟙 x✝)

Tactic:
| id _ =>

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
x✝ : C
g : x✝ ⟶ Z✝
hg : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' (𝟙 x✝ ≫ g)

Tactic:
| id _ =>

Goal state after:
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
⊢ epimorphisms C ≤ MorphismProperty.surjective C

Tactic:
rw [surjective_eq_epimorphisms]

Goal state after: