mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap R (fun x ↦ M₂) M₃
inst✝ : DecidableEq ι₂
v : ι₂ → M₂
i : ι₂
a : R
b : M₂
this : DecidableEq ι₁ := ⋯.decidableEq
⊢ (m fun i_1 ↦ update v i (a • b) (σ i_1)) = a • m fun i_1 ↦ update v i b (σ i_1)

Tactic:
Function.update_apply_equiv_apply v

Goal state after:
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✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap R (fun x ↦ M₂) M₃
inst✝ : DecidableEq ι₂
v : ι₂ → M₂
i : ι₂
a : R
b : M₂
this : DecidableEq ι₁ := ⋯.decidableEq
⊢ (m fun i_1 ↦ update (v ∘ ⇑σ) (σ.symm i) (a • b) i_1) = a • m fun i_1 ↦ update (v ∘ ⇑σ) (σ.symm i) b i_1
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case neg
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
hik : ¬i = k
hik2 : ¬k < i
⊢ ↑i < ↑k.succ

Tactic:
Fin.val_succ,

Goal state after:
case neg
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
hik : ¬i = k
hik2 : ¬k < i
⊢ ↑i < ↑k + 1
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0
A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc
⊢ Aᵀ.det = B.det

Tactic:
← det_transpose B

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0
A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc
⊢ Aᵀ.det = Bᵀ.det
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: 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
⊢ ∑ σ, ↑↑(sign σ) * ∏ i, blockDiagonal M (σ i) i = ∑ x, ∏ x_1, ↑↑(sign (x x_1 ⋯)) * ∏ x_2, M x_1 ((x x_1 ⋯) x_2) x_2

Tactic:
let preserving_snd : Finset (Equiv.Perm (n × o)) := {σ | ∀ x, (σ x).snd = x.snd}

Goal state after:
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}
⊢ ∑ σ, ↑↑(sign σ) * ∏ i, blockDiagonal M (σ i) i = ∑ x, ∏ x_1, ↑↑(sign (x x_1 ⋯)) * ∏ x_2, M x_1 ((x x_1 ⋯) x_2) x_2
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: case mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', y⟩ → FilteredColimit.Rel F ⟨j, x⟩ ⟨j', y⟩

Tactic:
rw [← (FilteredColimit.rel_equiv F).eqvGen_iff]

Goal state after:
case mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', y⟩ → Relation.EqvGen (FilteredColimit.Rel F) ⟨j, x⟩ ⟨j', y⟩
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
⊢ (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t)) 1 = 1

Tactic:
simp [colimit_one_eq F IsFiltered.nonempty.some]

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

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
⊢ ∑ y, sign (decomposeFin.symm (i.succ, y)) • ∏ x, A ((decomposeFin.symm (i.succ, y)) x) x =
    (-1) ^ ↑i.succ * A i.succ 0 * (of fun i_1 j ↦ A (i.succ.succAbove i_1) j.succ).det

Tactic:
Fin.val_succ,

Goal state after:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
⊢ ∑ y, sign (decomposeFin.symm (i.succ, y)) • ∏ x, A ((decomposeFin.symm (i.succ, y)) x) x =
    (-1) ^ (↑i + 1) * A i.succ 0 * (of fun i_1 j ↦ A (i.succ.succAbove i_1) j.succ).det
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)
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), (directLimitCocone G f).ι.app j ≫ m = s.ι.app j
i : ι
⊢ s.ι.app i = ↟(DirectLimit.of R ι (fun i ↦ G i) (fun i j H ↦ f i j H) i) ≫ m

Tactic:
← h

Goal state after:
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)
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), (directLimitCocone G f).ι.app j ≫ m = s.ι.app j
i : ι
⊢ (directLimitCocone G f).ι.app i ≫ m = ↟(DirectLimit.of R ι (fun i ↦ G i) (fun i j H ↦ f i j H) i) ≫ m
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: case h₂
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
E' : Type u₄
inst✝¹⁰ : Category.{v₄, u₄} E'
inst✝⁹ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁸ : F₁.LaxMonoidal
inst✝⁷ : F₂.LaxMonoidal
inst✝⁶ : F₃.LaxMonoidal
F G : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
⊢ (ε (F.prod' H) ≫ (prod' α β).app (𝟙_ C)).2 = (ε (G.prod' K)).2

Tactic:
rw [prod_comp_snd, prod'_ε_snd, prod'_ε_snd, prod'_app_snd, IsMonoidal.unit]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.CancelIso

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst✝ : IsIso f
g : y ⟶ x
h : inv f = g
⊢ f ≫ g = 𝟙 x

Tactic:
← h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst✝ : IsIso f
g : y ⟶ x
h : inv f = g
⊢ f ≫ inv f = 𝟙 x
Module: Mathlib.Tactic.CategoryTheory.CancelIso

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst✝ : IsIso f
g : y ⟶ x
h : inv f = g
z : C
k : x ⟶ z
⊢ f ≫ g ≫ k = k

Tactic:
← h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst✝ : IsIso f
g : y ⟶ x
h : inv f = g
z : C
k : x ⟶ z
⊢ f ≫ inv f ≫ k = k
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 ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : Y ⊗ X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ δ F (G.obj X ⊗ G.obj Y) (G.obj Z) ≫
      F.map (adj.unit.app (G.obj X ⊗ G.obj Y)) ▷ F.obj (G.obj Z) ≫
        adj.counit.app (F.obj (G.obj X ⊗ G.obj Y)) ▷ F.obj (G.obj Z) ≫
          F.obj (G.obj X ⊗ G.obj Y) ◁ adj.counit.app Z ≫
            δ F (G.obj X) (G.obj Y) ▷ Z ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y) ▷ Z ≫ (α_ X Y Z).hom =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))

Tactic:
← comp_whiskerRight_assoc,

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
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : Y ⊗ X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
⊢ δ F (G.obj X ⊗ G.obj Y) (G.obj Z) ≫
      (F.map (adj.unit.app (G.obj X ⊗ G.obj Y)) ≫ adj.counit.app (F.obj (G.obj X ⊗ G.obj Y))) ▷ F.obj (G.obj Z) ≫
        F.obj (G.obj X ⊗ G.obj Y) ◁ adj.counit.app Z ≫
          δ F (G.obj X) (G.obj Y) ▷ Z ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y) ▷ Z ≫ (α_ X Y Z).hom =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))
Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsLimit (cospan f f) F
inst✝ : Mono (F.map f)
this : IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) ⋯)
⊢ Mono f

Tactic:
apply PullbackCone.mono_of_isLimitMkIdId _ (isLimitOfIsLimitPullbackConeMap F _ this)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.ContainsIdentities
x : C
⊢ W (CategoryTheory.eqToHom ⋯)

Tactic:
rw [eqToHom_refl]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.ContainsIdentities
x : C
⊢ W (𝟙 x)
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
h : W.multiplicativeClosure = W
⊢ W.IsMultiplicative

Tactic:
← h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
h : W.multiplicativeClosure = W
⊢ W.multiplicativeClosure.IsMultiplicative
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
f g : Arrow (Type u)
φ : f ⟶ g
⊢ (Arrow.leftFunc.map φ ≫ ↾fun x ↦ ⟨(hom g.hom) x, ⋯⟩) =
    (↾fun x ↦ ⟨(hom f.hom) x, ⋯⟩) ≫
      { obj := fun f ↦ ↑(Set.range ⇑(TypeCat.Hom.hom f.hom)),
            map := fun {X Y} φ ↦ ↾fun y ↦ ⟨(hom (Arrow.Hom.right φ)) ↑y, ⋯⟩,
            map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
            map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 }.map
        φ

Tactic:
ext x
        exact congr_hom φ.w x

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 ⥤ C
adj : F ⊣ G
inst✝⁵ : F.OplaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : adj.IsMonoidal
F' : D ⥤ E
G' : E ⥤ D
adj' : F' ⊣ G'
inst✝² : F'.OplaxMonoidal
inst✝¹ : G'.LaxMonoidal
inst✝ : adj'.IsMonoidal
⊢ ε (G' ⋙ G) = (adj.comp adj').unit.app (𝟙_ C) ≫ (G' ⋙ G).map (η (F ⋙ F'))

Tactic:
simp [IsMonoidal.leftAdjoint_ε (adj := adj'), IsMonoidal.leftAdjoint_ε (adj := adj),
      ← map_comp, ← adj'.unit_naturality_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
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
h : MorphismProperty.surjective C = epimorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
⊢ Function.Surjective ⇑(hom ((forget C).map f))

Tactic:
← h

Goal state after:
case mp
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
h : MorphismProperty.surjective C = epimorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : MorphismProperty.surjective C f
⊢ Function.Surjective ⇑(hom ((forget C).map f))
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
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
h : MorphismProperty.injective C = monomorphisms C
⊢ ∀ {X Y : C} (f : X ⟶ Y) [Mono f], Mono ((forget C).map f)

Tactic:
rintro _ _ f (hf : monomorphisms C f)

Goal state after:
case mp
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
h : MorphismProperty.injective C = monomorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
⊢ Mono ((forget C).map f)
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
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
h : MorphismProperty.injective C = monomorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
⊢ Function.Injective ⇑(hom ((forget C).map f))

Tactic:
← h

Goal state after:
case mp
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
h : MorphismProperty.injective C = monomorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : MorphismProperty.injective C f
⊢ Function.Injective ⇑(hom ((forget C).map f))
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 X✝ Y✝ ▷ F.obj Z✝ ≫
      μ F (X✝ ⊗ Y✝) Z✝ ≫ F.map (α_ X✝ Y✝ Z✝).hom ≫ F.map (β X✝ (Y✝ ⊗ Z✝)).hom ≫ F.map (α_ Y✝ Z✝ X✝).hom =
    μ F X✝ Y✝ ▷ F.obj Z✝ ≫
      F.map (β X✝ Y✝).hom ▷ F.obj Z✝ ≫ μ F (Y✝ ⊗ X✝) Z✝ ≫ F.map (α_ Y✝ X✝ Z✝).hom ≫ F.map (Y✝ ◁ (β X✝ Z✝).hom)

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

Tactic:
← comp_whiskerRight_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✝)).inv ≫
      μ F X✝ Y✝ ▷ F.obj Z✝ ≫ μ F (X✝ ⊗ Y✝) Z✝ ≫ 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.obj Z✝) (F.obj Y✝)).inv ≫ (μ F X✝ Z✝ ≫ F.map (β X✝ Z✝).hom) ▷ F.obj Y✝ ≫ μ F (Z✝ ⊗ X✝) Y✝
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 ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| adj.unit.app X ▷ Y ▷ Z ≫
    (G.obj (F.obj X) ◁ adj.unit.app Y) ▷ Z ≫
      (G.obj (F.obj X) ⊗ G.obj (F.obj Y)) ◁ adj.unit.app Z ≫
        μ G (F.obj X) (F.obj Y) ▷ G.obj (F.obj Z) ≫
          μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom

Tactic:
← comp_whiskerRight_assoc,

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
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (adj.unit.app X ▷ Y ≫ G.obj (F.obj X) ◁ adj.unit.app Y) ▷ Z ≫
    (G.obj (F.obj X) ⊗ G.obj (F.obj Y)) ◁ adj.unit.app Z ≫
      μ G (F.obj X) (F.obj Y) ▷ G.obj (F.obj Z) ≫
        μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom
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 ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
x✝ : C
⊢ (adj.homEquiv x✝ (𝟙_ D ⊗ F.obj x✝)) (λ_ (F.obj x✝)).inv =
    (λ_ x✝).inv ≫
      (adj.unit.app (𝟙_ C) ⊗ₘ adj.unit.app x✝) ≫
        (G.map ((adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G)) ⊗ₘ 𝟙 (G.obj (F.obj x✝))) ≫ μ G (𝟙_ D) (F.obj x✝)

Tactic:
tensorHom_comp_tensorHom_assoc

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
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
x✝ : C
⊢ (adj.homEquiv x✝ (𝟙_ D ⊗ F.obj x✝)) (λ_ (F.obj x✝)).inv =
    (λ_ x✝).inv ≫
      (adj.unit.app (𝟙_ C) ≫ G.map ((adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G)) ⊗ₘ
          adj.unit.app x✝ ≫ 𝟙 (G.obj (F.obj x✝))) ≫
        μ G (𝟙_ D) (F.obj x✝)
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 ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
x✝ : C
⊢ (adj.homEquiv x✝ (F.obj x✝ ⊗ 𝟙_ D)) (ρ_ (F.obj x✝)).inv =
    (ρ_ x✝).inv ≫
      (adj.unit.app x✝ ⊗ₘ adj.unit.app (𝟙_ C)) ≫
        (𝟙 (G.obj (F.obj x✝)) ⊗ₘ G.map ((adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G))) ≫ μ G (F.obj x✝) (𝟙_ D)

Tactic:
tensorHom_comp_tensorHom_assoc

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
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
x✝ : C
⊢ (adj.homEquiv x✝ (F.obj x✝ ⊗ 𝟙_ D)) (ρ_ (F.obj x✝)).inv =
    (ρ_ x✝).inv ≫
      (adj.unit.app x✝ ≫ 𝟙 (G.obj (F.obj x✝)) ⊗ₘ
          adj.unit.app (𝟙_ C) ≫ G.map ((adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G))) ≫
        μ G (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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.Monoidal
inst✝ : adj.IsMonoidal
⊢ F.map (η G) ≫ η F = adj.counit.app (𝟙_ D)

Tactic:
by
  simp [← adj.map_ε_comp_counit_app_unit]

Goal state after: