mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case refine_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
j : Fin (n + 1)
⊢ ∀ (i : Fin n),
    (extendCofan c₁ c₂).ι.app { as := i.castSucc } ≫
          ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
              (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } })) =
        s.ι.app { as := i.castSucc } →
      (extendCofan c₁ c₂).ι.app { as := i.succ } ≫
          ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
              (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } })) =
        s.ι.app { as := i.succ }

Tactic:
rintro i -

Goal state after:
case refine_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
j : Fin (n + 1)
i : Fin n
⊢ (extendCofan c₁ c₂).ι.app { as := i.succ } ≫
      ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
          (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } })) =
    s.ι.app { as := i.succ }
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
X Y : C
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e : { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ (Functor.const J).map e₁.hom }
c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ (Functor.const J).map e₂.hom }
h₁' : IsColimit c₁'
h₂' : IsColimit c₂'
hg : h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } = g
⊢ W.colimitsOfShape J (Arrow.hom { left := Y₁, right := Y₂, hom := g })

Tactic:
rw [← hg]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
X Y : C
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e : { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ (Functor.const J).map e₁.hom }
c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ (Functor.const J).map e₂.hom }
h₁' : IsColimit c₁'
h₂' : IsColimit c₂'
hg : h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } = g
⊢ W.colimitsOfShape J (Arrow.hom { left := Y₁, right := Y₂, hom := h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } })
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : F₁ ⟶ F₂
x✝ : ∀ (j : J), IsIso (f.app j)
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
⊢ MorphismProperty.isomorphisms C φ

Tactic:
have := NatIso.isIso_of_isIso_app f
    exact ⟨h₂.desc (Cocone.mk _ (inv f ≫ c₁.ι)),
      h₁.hom_ext (fun j ↦ by simp [reassoc_of% (hφ j)]),
      h₂.hom_ext (by simp [hφ])⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
P : MorphismProperty C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.RespectsIso
⊢ ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P.diagonal g → P.diagonal (pullback.fst f g)

Tactic:
introv h
      rw [diagonal_iff, diagonal_pullback_fst, P.cancel_left_of_respectsIso,
        P.cancel_right_of_respectsIso]
      exact P.overPullbackMap f _ (by simpa)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

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
P : ObjectProperty C
J : Type u'
inst✝⁶ : Category.{v', u'} J
J' : Type u''
inst✝⁵ : Category.{v'', u''} J'
inst✝⁴ : ObjectProperty.Small.{w, v_1, u_1} P
inst✝³ : LocallySmall.{w, v_1, u_1} C
inst✝² : Small.{w, u'} J
inst✝¹ : LocallySmall.{w, v', u'} J
F : J ⥤ C
inst✝ : HasColimit F
hF : ∀ (j : J), P (F.obj j)
⊢ ∃ a, (fun F ↦ ⟨colimit (↑F ⋙ P.ι), ⋯⟩) a = ⟨colimit F, ⋯⟩

Tactic:
exact ⟨⟨P.lift F hF, by assumption⟩, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.colimitsOfShape J = (P.op.limitsOfShape Jᵒᵖ).unop

Tactic:
by
  ext X
  refine ⟨fun ⟨h⟩ => ⟨?_⟩, fun ⟨h⟩ => ⟨?_⟩⟩
  · exact
      { diag := h.diag.op
        π := NatTrans.op h.ι
        isLimit := isLimitOfUnop h.isColimit
        prop_diag_obj _ := h.prop_diag_obj _ }
  · exact
      { diag := h.diag.unop
        ι := NatTrans.unop h.π
        isColimit := isColimitOfOp h.isLimit
        prop_diag_obj _ := h.prop_diag_obj _ }

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ α.homEquiv' (X ◁ α.homEquiv'.symm 1 ≫ fst X X) * α.homEquiv' (X ◁ α.homEquiv'.symm 1 ≫ snd X X) =
    α.homEquiv' (ρ_ X).hom

Tactic:
simp only [whiskerLeft_fst, whiskerLeft_snd, α.homEquiv'_comp, Equiv.apply_symm_apply]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ α.homEquiv' (fst X (𝟙_ C)) * (ConcreteCategory.hom (F.map (snd X (𝟙_ C)).op)) 1 = α.homEquiv' (ρ_ X).hom
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f : X ⟶ M
⊢ lift (toUnit X ≫ η) (f ≫ 𝟙 M) ≫ μ = f ≫ 𝟙 M

Tactic:
← lift_map_assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f : X ⟶ M
⊢ lift (toUnit X) f ≫ (η ⊗ₘ 𝟙 M) ≫ μ = f ≫ 𝟙 M
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f : X ⟶ M
⊢ lift (f ≫ 𝟙 M) (toUnit X ≫ η) ≫ μ = f ≫ 𝟙 M

Tactic:
← lift_map_assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f : X ⟶ M
⊢ lift f (toUnit X) ≫ (𝟙 M ⊗ₘ η) ≫ μ = f ≫ 𝟙 M
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Bialgebra R A
⊢ op (of R A) ◁ (ofHom (counitAlgHom R A)).op ≫ (ofHom (comulAlgHom R A)).op = (ρ_ (op (of R A))).hom

Tactic:
by ext; exact Coalgebra.lTensor_counit_comul _

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y : C
⊢ δ F X Y ≫ fst (F.obj X) (F.obj Y) = F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom

Tactic:
rw [← whiskerLeft_fst _ (F.map (toUnit Y)), δ_natural_right_assoc]
    simp [← OplaxMonoidal.right_unitality_hom, rightUnitor_hom (F.obj X)]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y : C
⊢ δ F X Y ≫ fst (F.obj X) (F.obj Y) = F.map (fst X Y)

Tactic:
trans F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom
  · rw [← whiskerLeft_fst _ (F.map (toUnit Y)), δ_natural_right_assoc]
    simp [← OplaxMonoidal.right_unitality_hom, rightUnitor_hom (F.obj X)]
  · simp [← Functor.map_comp, rightUnitor_hom]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ μ ≫ toUnit A ≫ η = lift ((β_ A A).hom ≫ (ι ⊗ₘ ι) ≫ μ) μ ≫ μ

Tactic:
← Category.assoc (β_ A A).hom,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ μ ≫ toUnit A ≫ η = lift (((β_ A A).hom ≫ (ι ⊗ₘ ι)) ≫ μ) μ ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ (λ_ ((ihom Y).obj Z)).inv ≫ curry' f ▷ (ihom Y).obj Z ≫ comp X Y Z =
    (λ_ ((ihom Y).obj Z)).inv ≫ (λ_ ((ihom Y).obj Z)).hom ≫ (pre f).app Z

Tactic:
Iso.inv_hom_id_assoc

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ (λ_ ((ihom Y).obj Z)).inv ≫ curry' f ▷ (ihom Y).obj Z ≫ comp X Y Z = (pre f).app Z
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ (ρ_ ((ihom X).obj Y)).inv ≫ (ihom X).obj Y ◁ curry' f ≫ comp X Y Z =
    (ρ_ ((ihom X).obj Y)).inv ≫ (ρ_ ((ihom X).obj Y)).hom ≫ (ihom X).map f

Tactic:
Iso.inv_hom_id_assoc

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ (ρ_ ((ihom X).obj Y)).inv ≫ (ihom X).obj Y ◁ curry' f ≫ comp X Y Z = (ihom X).map f
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ (ρ_ (X ⊗ (ihom X).obj Y)).inv ≫ (ρ_ (X ⊗ (ihom X).obj Y)).hom ≫ (ihom.ev X).app Y ≫ f = (ihom.ev X).app Y ≫ f

Tactic:
Iso.inv_hom_id_assoc

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ (ihom.ev X).app Y ≫ f = (ihom.ev X).app Y ≫ f
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ (ihom X).obj Y ◁ curry' f ≫ comp X Y Z = (ρ_ ((ihom X).obj Y)).hom ≫ (ihom X).map f

Tactic:
by
  rw [← cancel_epi (ρ_ _).inv, Iso.inv_hom_id_assoc]
  apply uncurry_injective
  rw [uncurry_ihom_map, comp_eq, ← curry_natural_left, ← curry_natural_left, uncurry_curry,
    compTranspose_eq, associator_inv_naturality_right_assoc, whisker_exchange_assoc]
  dsimp
  rw [whiskerLeft_curry'_ihom_ev_app, whiskerLeft_rightUnitor_inv,
    MonoidalCategory.whiskerRight_id_assoc, Category.assoc,
    Iso.inv_hom_id_assoc, Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc]

Goal state after:
Module: Mathlib.Logic.Equiv.Multiset

Goal state before:
pp: m : ℕ
l : List ℕ
n : ℕ
h : (n :: m :: l).SortedLE
this : n ≤ m
⊢ raise (lower (m :: l) n) n = m :: l

Tactic:
simp [raise, lower, Nat.sub_add_cancel this, raise_lower h.pairwise.of_cons.sortedLE]

Goal state after:
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type u
⊢ (sum fun a ↦ #(WType β) ^ lift.{u, u} #(β a)) = sum fun a ↦ #(WType β) ^ #(β a)

Tactic:
by simp_rw [lift_id]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (tensorLeftHomEquiv (ᘁY) (ᘁX) X (𝟙_ C)) (f ▷ ᘁY ≫ ε_ (ᘁY) Y) = (ᘁf) ≫ (ρ_ ᘁX).inv

Tactic:
dsimp [tensorLeftHomEquiv, leftAdjointMate]
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case hl.fst
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : Dual R N
q : Q
x✝ : M
⊢ ((prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) ∘ₗ inl R M N) x✝).1 =
    (((dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q) q) ∘ₗ inl R M N) x✝).1

Tactic:
simp only [coe_comp, coe_inr, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
      snd_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case hl.snd
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : Dual R N
q : Q
x✝ : M
⊢ ((prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) ∘ₗ inl R M N) x✝).2 =
    (((dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q) q) ∘ₗ inl R M N) x✝).2

Tactic:
simp only [coe_comp, coe_inr, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
      snd_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case hr.fst
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : Dual R N
q : Q
x✝ : N
⊢ ((prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) ∘ₗ inr R M N) x✝).1 =
    (((dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q) q) ∘ₗ inr R M N) x✝).1

Tactic:
simp only [coe_comp, coe_inr, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
      snd_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case hr.snd
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : Dual R N
q : Q
x✝ : N
⊢ ((prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) ∘ₗ inr R M N) x✝).2 =
    (((dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q) q) ∘ₗ inr R M N) x✝).2

Tactic:
simp only [coe_comp, coe_inr, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
      snd_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring R₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst✝ : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
⊢ (B a) b = (B b) c

Tactic:
have : B a a + B a b + B a c = B a c + B b c + B c c := by
    simp_rw [← map_add, ← map_add₂, hAdd, map_zero, LinearMap.zero_apply]

Goal state after:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring R₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst✝ : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
this : (B a) a + (B a) b + (B a) c = (B a) c + (B b) c + (B c) c
⊢ (B a) b = (B b) c
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Function.Bijective ⇑(dualTensorHom R M R)

Tactic:
simpa only [dualTensorHom_self_right] using! LinearEquiv.bijective _

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Projective R M
inst✝² : Module.Finite R M
inst✝¹ : Projective R N
inst✝ : Module.Finite R N
m : M →ₗ[R] P
n : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (((TensorProduct.mk R M N).compr₂ₛₗ
          ((((TensorProduct.mk R (M →ₗ[R] P) (N →ₗ[R] Q)).compr₂ₛₗ ↑(homTensorHomEquiv R M N P Q)) m) n))
        x✝¹)
      x✝ =
    (((TensorProduct.mk R M N).compr₂ₛₗ
          ((((TensorProduct.mk R (M →ₗ[R] P) (N →ₗ[R] Q)).compr₂ₛₗ (homTensorHomMap (RingHom.id R) M N P Q)) m) n))
        x✝¹)
      x✝

Tactic:
simp only [homTensorHomEquiv, compr₂ₛₗ_apply, mk_apply, LinearEquiv.coe_toLinearMap,
    LinearEquiv.trans_apply, lift.equiv_apply, LinearEquiv.arrowCongr_apply, LinearEquiv.refl_symm,
    LinearEquiv.refl_apply, rTensorHomEquivHomRTensor_apply, lTensorHomEquivHomLTensor_apply,
    lTensorHomToHomLTensor_apply, rTensorHomToHomRTensor_apply, homTensorHomMap_apply,
    map_tmul]

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

Goal state before:
pp: n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.flip.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
⊢ B.SeparatingRight

Tactic:
rw [← flip_separatingLeft]

Goal state after:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.flip.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
⊢ B.flip.SeparatingLeft
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
hB : IsSymm B
x y : M
⊢ (B x) y ^ 2 < (B x) x * (B y) y ↔ LinearIndependent R ![x, y]

Tactic:
by
  rw [show B x y ^ 2 = B x y * B y x by rw [sq, ← hB.eq, RingHom.id_apply]]
  exact apply_mul_apply_lt_iff_linearIndependent B hp x y

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Injective ⇑(Hom.hom f)
⊢ ∀ (j : WalkingParallelPair),
    (kernelCone g).π.app j =
      (LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
                LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯).toModuleIso.symm.hom ≫
        (KernelFork.ofι f ⋯).π.app j

Tactic:
· rintro ⟨⟩ <;> ext x <;> simp [kernelCone]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
x y : ↑N
m : ↑M
w : x = y + (ConcreteCategory.hom f) m
⊢ (ConcreteCategory.hom (cokernel.π f)) x = (ConcreteCategory.hom (cokernel.π f)) y

Tactic:
subst w
  simpa only [map_add, add_eq_left] using! cokernel.condition_apply f m

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks

Goal state before:
pp: case h₁
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := ⋯
π₂ : X ⨯ Y ⟶ Y := ⋯
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := ⋯
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = s.fst
h₂ : m ≫ e ≫ π₂ = s.snd
⊢ (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.fst =
    (equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ ≫
        equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫
      prod.fst

Tactic:
simpa using h₁

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks

Goal state before:
pp: case h₁
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := ⋯
ι₂ : Z ⟶ Y ⨿ Z := ⋯
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := ⋯
s : PushoutCocone f g
m : coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt
h₁ : (ι₁ ≫ c) ≫ m = s.inl
h₂ : (ι₂ ≫ c) ≫ m = s.inr
⊢ coprod.inl ≫ coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫ m =
    coprod.inl ≫
      coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫
        coequalizer.desc (coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)) ⋯

Tactic:
simpa using h₁

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
c : Cone (parallelPair 0 0)
hc : IsLimit c
this : IsIso (Fork.ι c)
⊢ IsLimit (G.mapCone c)

Tactic:
refine (KernelFork.isLimitMapConeEquiv c G).symm ?_

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
c : Cone (parallelPair 0 0)
hc : IsLimit c
this : IsIso (Fork.ι c)
⊢ IsLimit (KernelFork.map c G)