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

Goal state before:
pp: case 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
⊢ ∀ a ∈ univ, (prodCongrLeft fun k ↦ a k ⋯) ∈ preserving_snd

Tactic:
intro σ _

Goal state after:
case 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
σ : (a : o) → a ∈ univ → Perm n
ha✝ : σ ∈ univ
⊢ (prodCongrLeft fun k ↦ σ k ⋯) ∈ preserving_snd
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 : ι) → AddCommMonoid (M₁ i)
inst✝⁹ : (i : ι) → Module R (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M₂
inst✝⁶ : Semiring S
inst✝⁵ : Module S M₂
inst✝⁴ : SMulCommClass R S M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module S M₃
inst✝¹ : Module R M₃
inst✝ : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f₁ f₂ : MultilinearMap R M₁ M₂
⊢ { toFun := ⇑(f₁ + f₂) ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ } =
    { toFun := ⇑f₁ ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ } +
      { toFun := ⇑f₂ ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ }

Tactic:
by
    ext
    simp only [Function.comp, coe_mk, add_apply]

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

Goal state before:
pp: case refine_3.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
σ : 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)
⊢ (prodCongrLeft fun k ↦
      (fun k x ↦ { toFun := fun x ↦ (σ (x, k)).1, invFun := fun x ↦ (σ.symm (x, k)).1, left_inv := ⋯, right_inv := ⋯ })
        k ⋯) =
    σ

Tactic:
ext ⟨k, x⟩

Goal state after:
case refine_3.refine_4.fst
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)) := ⋯
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 : n
x : o
⊢ ((prodCongrLeft fun k ↦
          (fun k x ↦
              { toFun := fun x ↦ (σ (x, k)).1, invFun := fun x ↦ (σ.symm (x, k)).1, left_inv := ⋯, right_inv := ⋯ })
            k ⋯)
        (k, x)).1 =
    (σ (k, x)).1

case refine_3.refine_4.snd
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)) := ⋯
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 : n
x : o
⊢ ((prodCongrLeft fun k ↦
          (fun k x ↦
              { toFun := fun x ↦ (σ (x, k)).1, invFun := fun x ↦ (σ.symm (x, k)).1, left_inv := ⋯, right_inv := ⋯ })
            k ⋯)
        (k, x)).2 =
    (σ (k, x)).2
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
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 σ _

Goal state after:
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 : o) → a ∈ univ → Perm n
ha✝ : σ ∈ univ
⊢ ∏ x, ↑↑(sign (σ x ⋯)) * ∏ x_1, M x ((σ x ⋯) x_1) x_1 =
    ↑↑(sign (prodCongrLeft fun k ↦ σ k ⋯)) * ∏ i, blockDiagonal M ((prodCongrLeft fun k ↦ σ k ⋯) i) i
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

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
⊢ ∀ a ∈ univ,
    (↑↑(sign a.1) * ∏ i, A (a.1 i) i) * (↑↑(sign a.2) * ∏ i, D (a.2 i) i) =
      ↑↑(sign (a.1.sumCongr a.2)) * ∏ i, fromBlocks A B 0 D ((a.1.sumCongr a.2) i) i

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

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
⊢ ∀ a ∈ univ,
    (↑↑(sign a.1) * ∏ i, A (a.1 i) i) * (↑↑(sign a.2) * ∏ i, D (a.2 i) i) =
      ↑↑(sign (a.1.sumCongr a.2)) * ∏ i, fromBlocks A B 0 D ((a.1.sumCongr a.2) i) i
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

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

Tactic:
obtain ⟨j, x, rfl⟩ := x.mk_surjective
      rw [colimit_one_eq F j, colimit_mul_mk_eq', mul_one]

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:
by
  ext; rw [mkPiRing_apply, smul_zero, zero_apply]

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

Goal state before:
pp: F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((limitCone F).π.app (Opposite.op 0)))

Tactic:
intro a

Goal state after:
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
a : F.obj (Opposite.op 0)
⊢ ∃ a_1, (ConcreteCategory.hom ((limitCone F).π.app (Opposite.op 0))) a_1 = a
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 ι
inst✝ : Fintype ι
x h h' : (i : ι) → M₁ i
⊢ f x + ((f.linearDeriv x) h + ∑ s with 2 ≤ #s, f (s.piecewise h x)) -
        (f x + ((f.linearDeriv x) h' + ∑ s with 2 ≤ #s, f (s.piecewise h' x))) -
      (f.linearDeriv x) (h - h') =
    ∑ s with 2 ≤ #s, (f (s.piecewise h x) - f (s.piecewise h' x))

Tactic:
add_sub_add_comm,

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 ι
inst✝ : Fintype ι
x h h' : (i : ι) → M₁ i
⊢ f x - f x +
        ((f.linearDeriv x) h - (f.linearDeriv x) h' +
          (∑ s with 2 ≤ #s, f (s.piecewise h x) - ∑ s with 2 ≤ #s, f (s.piecewise h' x))) -
      (f.linearDeriv x) (h - h') =
    ∑ s with 2 ≤ #s, (f (s.piecewise h x) - f (s.piecewise h' x))
Module: Mathlib.CategoryTheory.Limits.Types.Yoneda

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
X : C
t : (const J).obj X ⟶ F
⊢ t.app ∈ (F ⋙ coyoneda.obj (op X)).sections

Tactic:
by
    simp [Functor.sections, ← t.naturality]

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ᵒᵖ
P : C ⥤ Type w
Y : Cᵒᵖ
f : Y ⟶ X
g : shrinkCoyoneda.{w, v, u}.obj X ⟶ P
⊢ (ConcreteCategory.hom ((shrinkCoyonedaEquiv.symm (shrinkCoyonedaEquiv g)).app (unop Y)))
      (shrinkCoyonedaObjObjEquiv.symm f.unop) =
    (ConcreteCategory.hom (P.map f.unop)) (shrinkCoyonedaEquiv g)

Tactic:
simp [map_shrinkCoyonedaEquiv]

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✝ Y✝ : Cᵒᵖ
g : X✝ ⟶ Y✝
x✝¹ : C
x✝ : (uliftCoyoneda.{w', v, u}.obj X✝).obj x✝¹
⊢ (ConcreteCategory.hom
          ((uliftCoyoneda.{w', v, u}.map g ≫
                (NatIso.ofComponents (fun Y ↦ (Equiv.ulift.trans shrinkCoyonedaObjObjEquiv.symm).toIso) ⋯).hom).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((NatIso.ofComponents (fun Y ↦ (Equiv.ulift.trans shrinkCoyonedaObjObjEquiv.symm).toIso) ⋯).hom ≫
                shrinkCoyoneda.{max w' v, v, u}.map g).app
            x✝¹)).toFun
      x✝

Tactic:
exact (shrinkCoyoneda_map_app_shrinkCoyonedaObjObjEquiv_symm _ _).symm

Goal state after:
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.CategoryTheory.Monoidal.Discrete

Goal state before:
pp: M : Type u
inst✝ : Monoid M
X x✝¹ x✝ : Discrete M
f : x✝¹ ⟶ x✝
⊢ { as := X.as * x✝¹.as } = { as := X.as * x✝.as }

Tactic:
eq_of_hom f

Goal state after:
M : Type u
inst✝ : Monoid M
X x✝¹ x✝ : Discrete M
f : x✝¹ ⟶ x✝
⊢ { as := X.as * x✝.as } = { as := X.as * x✝.as }
Module: Mathlib.CategoryTheory.Monoidal.Discrete

Goal state before:
pp: M : Type u
inst✝ : Monoid M
X₁✝ X₂✝ : Discrete M
f : X₁✝ ⟶ X₂✝
X : Discrete M
⊢ { as := X₁✝.as * X.as } = { as := X₂✝.as * X.as }

Tactic:
eq_of_hom f

Goal state after:
M : Type u
inst✝ : Monoid M
X₁✝ X₂✝ : Discrete M
f : X₁✝ ⟶ X₂✝
X : Discrete M
⊢ { as := X₂✝.as * X.as } = { as := X₂✝.as * X.as }
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:
by
    dsimp only [comp_μ, monoidalFunctorComp, Iso.refl, Discrete.monoidalFunctor_μ]
    simp [eqToHom_map]

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 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)

Tactic:
by
    simp_rw [← tensorHom_id, ← id_tensorHom, associativity]

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
⊢ Hom.hom (X✝ ◁ 0) = Hom.hom 0

Tactic:
refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
x : ↑X✝
y : ↑Y✝
⊢ (((TensorProduct.mk R ↑X✝ ↑Y✝).compr₂ₛₗ (Hom.hom (X✝ ◁ 0))) x) y =
    (((TensorProduct.mk R ↑X✝ ↑Y✝).compr₂ₛₗ (Hom.hom 0)) x) y
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
⊢ Hom.hom (0 ▷ X✝) = Hom.hom 0

Tactic:
refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
x : ↑Y✝
y : ↑X✝
⊢ (((TensorProduct.mk R ↑Y✝ ↑X✝).compr₂ₛₗ (Hom.hom (0 ▷ X✝))) x) y =
    (((TensorProduct.mk R ↑Y✝ ↑X✝).compr₂ₛₗ (Hom.hom 0)) x) y
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_3
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : Y✝ ⟶ Z✝
⊢ Hom.hom (X✝ ◁ (f✝ + g✝)) = Hom.hom (X✝ ◁ f✝ + X✝ ◁ g✝)

Tactic:
refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

Goal state after:
case refine_3
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : Y✝ ⟶ Z✝
x : ↑X✝
y : ↑Y✝
⊢ (((TensorProduct.mk R ↑X✝ ↑Y✝).compr₂ₛₗ (Hom.hom (X✝ ◁ (f✝ + g✝)))) x) y =
    (((TensorProduct.mk R ↑X✝ ↑Y✝).compr₂ₛₗ (Hom.hom (X✝ ◁ f✝ + X✝ ◁ g✝))) x) y
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_4
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : Y✝ ⟶ Z✝
⊢ Hom.hom ((f✝ + g✝) ▷ X✝) = Hom.hom (f✝ ▷ X✝ + g✝ ▷ X✝)

Tactic:
refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

Goal state after:
case refine_4
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : Y✝ ⟶ Z✝
x : ↑Y✝
y : ↑X✝
⊢ (((TensorProduct.mk R ↑Y✝ ↑X✝).compr₂ₛₗ (Hom.hom ((f✝ + g✝) ▷ X✝))) x) y =
    (((TensorProduct.mk R ↑Y✝ ↑X✝).compr₂ₛₗ (Hom.hom (f✝ ▷ X✝ + g✝ ▷ X✝))) x) y
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
r✝ : R
f✝ : Y✝ ⟶ Z✝
⊢ Hom.hom (X✝ ◁ (r✝ • f✝)) = Hom.hom (r✝ • X✝ ◁ f✝)

Tactic:
refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
r✝ : R
f✝ : Y✝ ⟶ Z✝
x : ↑X✝
y : ↑Y✝
⊢ (((TensorProduct.mk R ↑X✝ ↑Y✝).compr₂ₛₗ (Hom.hom (X✝ ◁ (r✝ • f✝)))) x) y =
    (((TensorProduct.mk R ↑X✝ ↑Y✝).compr₂ₛₗ (Hom.hom (r✝ • X✝ ◁ f✝))) x) y
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
r✝ : R
Y✝ Z✝ : ModuleCat R
f✝ : Y✝ ⟶ Z✝
X✝ : ModuleCat R
⊢ Hom.hom ((r✝ • f✝) ▷ X✝) = Hom.hom (r✝ • f✝ ▷ X✝)

Tactic:
refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
r✝ : R
Y✝ Z✝ : ModuleCat R
f✝ : Y✝ ⟶ Z✝
X✝ : ModuleCat R
x : ↑Y✝
y : ↑X✝
⊢ (((TensorProduct.mk R ↑Y✝ ↑X✝).compr₂ₛₗ (Hom.hom ((r✝ • f✝) ▷ X✝))) x) y =
    (((TensorProduct.mk R ↑Y✝ ↑X✝).compr₂ₛₗ (Hom.hom (r✝ • f✝ ▷ X✝))) 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
F : C ⥤ D
⊢ Function.Injective (@toLaxMonoidal C inst✝³ inst✝² D inst✝¹ inst✝ F)

Tactic:
intro a

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
a : F.Monoidal
⊢ ∀ ⦃a₂ : F.Monoidal⦄, a.toLaxMonoidal = a₂.toLaxMonoidal → a = a₂
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
⊢ Function.Injective (@toOplaxMonoidal C inst✝³ inst✝² D inst✝¹ inst✝ F)

Tactic:
intro a

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
a : F.Monoidal
⊢ ∀ ⦃a₂ : F.Monoidal⦄, a.toOplaxMonoidal = a₂.toOplaxMonoidal → a = a₂
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✝ F : C ⥤ D
G : E ⥤ C'
inst✝² : MonoidalCategory C'
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C × E
⊢ μ (F.prod G) x✝¹ x✝ ≫ δ (F.prod G) x✝¹ x✝ = 𝟙 ((F.prod G).obj x✝¹ ⊗ (F.prod G).obj x✝)

Tactic:
by ext <;> apply Monoidal.μ_δ

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ F.map (𝟙 ((diag C).obj (𝟙_ C)).1) ≫ (η (F.prod G)).1 = η F

Tactic:
rw [Functor.map_id, Category.id_comp]

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ (η (F.prod G)).1 = η F
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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ G.map (𝟙 ((diag C).obj (𝟙_ C)).2) ≫ (η (F.prod G)).2 = η G

Tactic:
rw [Functor.map_id, Category.id_comp]

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ (η (F.prod G)).2 = η G
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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ F.map (𝟙 ((diag C).obj (X ⊗ Y)).1) ≫ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 = δ F X Y

Tactic:
rw [Functor.map_id, Category.id_comp]

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 = δ F 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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ G.map (𝟙 ((diag C).obj (X ⊗ Y)).2) ≫ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 = δ G X Y

Tactic:
rw [Functor.map_id, Category.id_comp]

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 = δ G X Y
Module: Mathlib.CategoryTheory.Monoidal.Functor

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
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
⊢ (ε (F.prod' G) ≫ η (F.prod' G)).2 = (𝟙 (𝟙_ (D × E))).2

Tactic:
· simp only [CategoryTheory.prod_comp_snd, prod'_ε_snd, prod'_η_snd, ε_η,
        prodMonoidal_tensorUnit, prod_id]

Goal state after:
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
X : C
⊢ MorphismProperty.surjective C (𝟙 X)

Tactic:
delta MorphismProperty.surjective
    convert! surjective_id
    aesop

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

Goal state before:
pp: case zero
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ x.snd <• x.fst ^ 0 = x.fst ^ 0 •> x.snd

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Semiring R
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) * x = 1

Tactic:
by
    convert! mul_left_eq_one _ _ (invOf_mul_self x.fst)
    ext <;> simp

Goal state after: