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

Goal state before:
pp: case rel.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map f)) x.snd
⊢ Relation.ReflTransGen Zag (StructuredArrow.mk x.snd) ?rel.b

pp: case rel.b
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map f)) x.snd
⊢ StructuredArrow d F

pp: case rel.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map f)) x.snd
⊢ Zag ?rel.b (StructuredArrow.mk y.snd)

Tactic:
· fconstructor

Goal state after:
case rel.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map f)) x.snd
⊢ Zag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
h : IsTerminal (colimit (F ⋙ yoneda))
⊢ F.Final

Tactic:
refine final_of_colimit_comp_coyoneda_iso_pUnit _ (fun d => ?_)

Goal state after:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
h : IsTerminal (colimit (F ⋙ yoneda))
d : D
⊢ colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
          fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
        i₁) ≫
      fst f i =
    ((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
          snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
        i₂) ≫
      fst f i

pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
          fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
        i₁) ≫
      snd f i =
    ((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
          snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
        i₂) ≫
      snd f i

Tactic:
· simp only [Category.assoc, pullback_diagonal_map_snd_fst_fst,
      pullback_diagonal_map_snd_snd_fst]

Goal state after:
case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
          fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
        i₁) ≫
      snd f i =
    ((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
          snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
        i₂) ≫
      snd f i
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (pullbackDiagonalMapIso f i i₁ i₂).hom ≫ fst i₁ i₂ =
    snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)

Tactic:
delta pullbackDiagonalMapIso
  simp only [limit.lift_π, PullbackCone.mk_π_app]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (pullbackDiagonalMapIso f i i₁ i₂).hom ≫ snd i₁ i₂ =
    snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)

Tactic:
delta pullbackDiagonalMapIso
  simp only [limit.lift_π, PullbackCone.mk_π_app]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (pullbackDiagonalMapIso f i i₁ i₂).inv ≫
      fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) =
    fst i₁ i₂ ≫ i₁ ≫ fst f i

Tactic:
delta pullbackDiagonalMapIso
  simp only [limit.lift_π, PullbackCone.mk_π_app]

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

Goal state before:
pp: 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₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
⊢ (b : Fin (n + 1)) → c₂.pt ⟶ f b

Tactic:
by
      refine Fin.cases ?_ ?_
      · apply c₂.fst
      · intro i
        apply c₂.snd ≫ c₁.π.app ⟨i⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
J : Type u_2
inst✝ : Category.{v_2, u_2} J
⊢ W₁.limitsOfShape J ≤ W₂.limitsOfShape J

Tactic:
by
  rintro _ _ _ ⟨_, _, _, _, h₁, _, f, hf⟩
  exact ⟨_, _, _, _, h₁, _, f, fun j ↦ h _ (hf j)⟩

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

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
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
e : J ≌ J'
inst✝ : P.IsClosedUnderLimitsOfShape J
⊢ P.IsClosedUnderLimitsOfShape J'

Tactic:
rwa [← P.isClosedUnderLimitsOfShape_iff_of_equivalence e]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ ((lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁)
            (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯ ≫
          lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯) ≫
        fst (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
      snd (fst f' g') i₁ =
    (𝟙 (pullback (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
      snd (fst f' g') i₁

Tactic:
simp only [Category.assoc, lift_snd, lift_fst, Category.id_comp]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x ↦ X₁) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₁)
c₂ : Cocone (Discrete.functor fun x ↦ X₂) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
x✝ : Discrete PUnit.{w + 1}
⊢ (Discrete.functor fun x ↦ X₁).obj x✝ ⟶ (Discrete.functor fun x ↦ X₂).obj x✝

Tactic:
exact f

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x ↦ X₁) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₁)
c₂ : Cocone (Discrete.functor fun x ↦ X₂) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
x : Discrete PUnit.{w + 1}
⊢ x = ⊥_ Discrete PUnit.{w + 1}

Tactic:
by ext

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ (pullback.fst f.op g.op ≫ f.op) ≫ (Iso.refl (Opposite.op T)).hom =
    (pullbackIsoOpPushout f.op g.op).hom ≫ (pushout.inl f g).op ≫ f.op

Tactic:
simp [← Iso.inv_comp_eq]

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : P.limitsOfShape J X
h : P.LimitOfShape J X
⊢ P.op.ColimitOfShape Jᵒᵖ (Opposite.op X)

pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : (P.op.colimitsOfShape Jᵒᵖ).unop X
h : P.op.ColimitOfShape Jᵒᵖ (Opposite.op X)
⊢ P.LimitOfShape J X

Tactic:
· exact
      { diag := h.diag.op
        ι := NatTrans.op h.π
        isColimit := isColimitOfUnop h.isLimit
        prop_diag_obj _ := h.prop_diag_obj _ }

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : (P.op.colimitsOfShape Jᵒᵖ).unop X
h : P.op.ColimitOfShape Jᵒᵖ (Opposite.op X)
⊢ P.LimitOfShape J X
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
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : CartesianMonoidalCategory E
F : C ⥤ D
G : D ⥤ E
inst✝² : F.Monoidal
inst✝¹ : G.Monoidal
inst✝ : (F ⋙ G).Monoidal
X Y : C
⊢ μ (F ⋙ G) X Y = μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)

Tactic:
rw [← cancel_mono (μIso _ _ _).inv]; ext <;> simp [← Functor.comp_obj, ← Functor.map_comp]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ihom.ev x).app y ≫ (ρ_ y).inv ≫ uncurry (id y ≫ 𝟙 ((ihom y).obj y)) = uncurry (𝟙 ((ihom x).obj y))

Tactic:
simp [id_eq, uncurry_id_eq_ev]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i j : ι
⊢ (b.dualBasis.repr (b.dualBasis i)) j = (b.dualBasis j) (b i)

Tactic:
Basis.repr_self,

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i j : ι
⊢ (Finsupp.single i 1) j = (b.dualBasis j) (b i)
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
⊢ h.coeffs (lc e l) = l

Tactic:
by
  ext i
  rw [h.coeffs_apply, h.dual_lc]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
c : R
v : M
⊢ h.coeffs (c • v) = (RingHom.id R) c • h.coeffs v

Tactic:
ext i
        exact (ε i).map_smul c v

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 Z : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
g : Xᘁ ⟶ Z
⊢ 𝟙 Yᘁ ⊗≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ⊗≫ (ε_ Y Yᘁ ▷ Xᘁ ≫ 𝟙_ C ◁ g) ⊗≫ 𝟙 Z =
    (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ (f ⊗ₘ g) ≫ (α_ Yᘁ Y Z).inv ≫ ε_ Y Yᘁ ▷ Z ≫ (λ_ Z).hom

Tactic:
← whisker_exchange,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
g : Xᘁ ⟶ Z
⊢ 𝟙 Yᘁ ⊗≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ⊗≫ ((Yᘁ ⊗ Y) ◁ g ≫ ε_ Y Yᘁ ▷ Z) ⊗≫ 𝟙 Z =
    (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ (f ⊗ₘ g) ≫ (α_ Yᘁ Y Z).inv ≫ ε_ Y Yᘁ ▷ Z ≫ (λ_ Z).hom
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
r : R
hr : r ≠ 0
⊢ r • v ∈ N → r = 0

Tactic:
have := linearIndependent_iff.mp hs' (Finsupp.single ⟨_, hv⟩ r)

Goal state after:
R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
r : R
hr : r ≠ 0
this :
  (Finsupp.linearCombination R Subtype.val) (Finsupp.single ⟨N.mkQ v, hv⟩ r) = 0 → Finsupp.single ⟨N.mkQ v, hv⟩ r = 0
⊢ r • v ∈ N → r = 0
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
inst✝¹ : DivisionRing K
ι : Type u_1
inst✝ : Fintype ι
b : ι → ι → K
hb : LinearIndependent K b
⊢ ⇑(basisOfPiSpaceOfLinearIndependent hb) = b

Tactic:
by
  by_cases hι : Nonempty ι
  · simp [hι, basisOfPiSpaceOfLinearIndependent]
  · rw [basisOfPiSpaceOfLinearIndependent, dif_neg hι]
    ext i
    exact ((not_nonempty_iff.mp hι).false i).elim

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 X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ 𝟙 (𝟙_ C ⊗ X) ⊗≫ (η_ X' Y ▷ X ≫ (X' ⊗ Y) ◁ i.hom) ⊗≫ (i.inv ▷ (Y ⊗ X') ≫ X ◁ ε_ X' Y) ⊗≫ 𝟙 (X ⊗ 𝟙_ C) =
    𝟙 (𝟙_ C ⊗ X) ⊗≫ i.hom ⊗≫ (η_ X' Y ▷ X' ⊗≫ X' ◁ ε_ X' Y) ⊗≫ i.inv ⊗≫ 𝟙 (X ⊗ 𝟙_ C)

Tactic:
← whisker_exchange,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ 𝟙 (𝟙_ C ⊗ X) ⊗≫ (𝟙_ C ◁ i.hom ≫ η_ X' Y ▷ X') ⊗≫ (i.inv ▷ (Y ⊗ X') ≫ X ◁ ε_ X' Y) ⊗≫ 𝟙 (X ⊗ 𝟙_ C) =
    𝟙 (𝟙_ C ⊗ X) ⊗≫ i.hom ⊗≫ (η_ X' Y ▷ X' ⊗≫ X' ◁ ε_ X' Y) ⊗≫ i.inv ⊗≫ 𝟙 (X ⊗ 𝟙_ C)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x✝ : M₁
⊢ (B x) (g x✝) + (B' (f' x)) x✝ = (B x) (g x✝) + (B x) (g' x✝)

Tactic:
h'

Goal state after:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x✝ : M₁
⊢ (B x) (g x✝) + (B x) (g' x✝) = (B x) (g x✝) + (B x) (g' x✝)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B : M →ₗ[R] M →ₗ[R] M₂
B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂
f f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x✝ : M₁
⊢ (B x) (g x✝) - (B' (f' x)) x✝ = (B x) (g x✝) - (B x) (g' x✝)

Tactic:
h'

Goal state after:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B : M →ₗ[R] M →ₗ[R] M₂
B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂
f f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x✝ : M₁
⊢ (B x) (g x✝) - (B x) (g' x✝) = (B x) (g x✝) - (B x) (g' x✝)
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: case zero
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ G.map (K.map WalkingParallelPairHom.left) ≫ c.ι.app WalkingParallelPair.one = c.ι.app WalkingParallelPair.zero

Tactic:
exact (c.ι.naturality WalkingParallelPairHom.left).trans (Category.comp_id _)

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K✝ : Type uK
V✝ : Type uV
inst✝¹³ : CommSemiring K✝
inst✝¹² : AddCommMonoid V✝
inst✝¹¹ : Module K✝ V✝
inst✝¹⁰ : Projective K✝ V✝
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : IsReflexive R M
K : Type u_4
V : Type u_5
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsReflexive K V
contra : ℵ₀ ≤ Module.rank K V
this : lift.{max u_5 u_4, u_5} (Module.rank K V) < Module.rank K (Dual K (Dual K V))
heq : lift.{max u_5 u_4, u_5} (Module.rank K V) = lift.{u_5, max u_5 u_4} (Module.rank K (Dual K (Dual K V)))
⊢ False

Tactic:
heq,

Goal state after:
K✝ : Type uK
V✝ : Type uV
inst✝¹³ : CommSemiring K✝
inst✝¹² : AddCommMonoid V✝
inst✝¹¹ : Module K✝ V✝
inst✝¹⁰ : Projective K✝ V✝
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : IsReflexive R M
K : Type u_4
V : Type u_5
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsReflexive K V
contra : ℵ₀ ≤ Module.rank K V
this : lift.{u_5, max u_5 u_4} (Module.rank K (Dual K (Dual K V))) < Module.rank K (Dual K (Dual K V))
heq : lift.{max u_5 u_4, u_5} (Module.rank K V) = lift.{u_5, max u_5 u_4} (Module.rank K (Dual K (Dual K V)))
⊢ False
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 ⟨⟩

Goal state after:
case zero
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)
⊢ (kernelCone g).π.app WalkingParallelPair.zero =
    (LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
              LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯).toModuleIso.symm.hom ≫
      (KernelFork.ofι f ⋯).π.app WalkingParallelPair.zero

case one
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)
⊢ (kernelCone g).π.app WalkingParallelPair.one =
    (LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
              LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯).toModuleIso.symm.hom ≫
      (KernelFork.ofι f ⋯).π.app WalkingParallelPair.one
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.Surjective ⇑(Hom.hom g)
⊢ ∀ (j : WalkingParallelPair),
    (cokernelCocone f).ι.app j ≫
        (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
            ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom =
      (CokernelCofork.ofπ g ⋯).ι.app j

Tactic:
rintro ⟨⟩

Goal state after:
case zero
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.Surjective ⇑(Hom.hom g)
⊢ (cokernelCocone f).ι.app WalkingParallelPair.zero ≫
      (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
          ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom =
    (CokernelCofork.ofπ g ⋯).ι.app WalkingParallelPair.zero

case one
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.Surjective ⇑(Hom.hom g)
⊢ (cokernelCocone f).ι.app WalkingParallelPair.one ≫
      (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
          ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom =
    (CokernelCofork.ofπ g ⋯).ι.app WalkingParallelPair.one
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₁
⊢ Injective ⇑B.flip ↔ Surjective ⇑B

Tactic:
rw [← dualMap_surjective_iff, ← (evalEquiv K V₁).toEquiv.surjective_comp]; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_4
V : Type u_5
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Subspace K V
inst✝ : FiniteDimensional K ↥W
⊢ (dualAnnihilator W).dualAnnihilator = map (Dual.eval K V) W

Tactic:
let e1 := (Free.chooseBasis K W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm
  have := e1.finiteDimensional
  let e2 := (Free.chooseBasis K _).toDualEquiv ≪≫ₗ W.dualAnnihilator.dualQuotEquivDualAnnihilator
  have := LinearEquiv.finiteDimensional (V₂ := W.dualAnnihilator.dualAnnihilator) e2
  rw [eq_of_le_of_finrank_eq (map_le_dualAnnihilator_dualAnnihilator W)]
  rw [← (equivMapOfInjective _ (eval_apply_injective K (V := V)) W).finrank_eq, e1.finrank_eq]
  exact e2.finrank_eq

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasKernels C
inst✝² : IsNormalMonoCategory C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
⊢ s.fst ≫ a ≫ f = s.fst ≫ 0

Tactic:
haf

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasKernels C
inst✝² : IsNormalMonoCategory C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
⊢ s.fst ≫ 0 = s.fst ≫ 0