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

Goal state before:
pp: J : Type w
inst✝⁶ : Category.{w', w} J
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : HasColimitsOfShape J C
inst✝² : PreservesColimitsOfShape J F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ F.essImage.strictColimitsOfShape J ≤ F.essImage

Tactic:
by
    rintro _ ⟨G, hG⟩
    exact ⟨colimit (Functor.essImage.liftFunctor G F hG),
      ⟨IsColimit.coconePointsIsoOfNatIso
        (isColimitOfPreserves F (colimit.isColimit _)) (colimit.isColimit _)
        (Functor.essImage.liftFunctorCompIso _ _ _)⟩⟩

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
⊢ IsPullback (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) (fst (fst f g) (fst f h)) (fst g h) (snd f g)

Tactic:
by
  refine ⟨⟨by simp⟩, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩
  · intro c
    refine pullback.lift c.snd
        (pullback.lift (c.snd ≫ pullback.fst _ _) (c.fst ≫ pullback.snd _ _) ?_) ?_
    · simp [pullback.condition, ← c.condition_assoc]
    · simp
  · intro c
    apply pullback.hom_ext <;> simp [c.condition]
  · intro c
    apply pullback.hom_ext <;> simp
  · intro c m hfst hsnd
    refine pullback.hom_ext (by simpa) ?_
    apply pullback.hom_ext <;> simp [← hsnd, pullback.condition, ← hfst]

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

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
⊢ ∀ {Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P.universally f → P.universally (e.hom ≫ f)

Tactic:
Z

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
⊢ ∀ (e : X ≅ Y) (f : Y ⟶ Z), P.universally f → P.universally (e.hom ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
⊢ ∀ {Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P.universally f → P.universally (f ≫ e.hom)

Tactic:
Z

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
⊢ ∀ (e : Y ≅ Z) (f : X ⟶ Y), P.universally f → P.universally (f ≫ e.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 : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ α.homEquiv' (α.homEquiv'.symm 1 ▷ X ≫ fst X X) * α.homEquiv' (α.homEquiv'.symm 1 ▷ X ≫ snd X X) =
    α.homEquiv' (λ_ X).hom

Tactic:
simp only [whiskerRight_fst, whiskerRight_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
⊢ (ConcreteCategory.hom (F.map (fst (𝟙_ C) X).op)) 1 * α.homEquiv' (snd (𝟙_ C) X) = α.homEquiv' (λ_ X).hom
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ Z✝ : CommAlgCat R
f✝ : Y✝ ⟶ Z✝
⊢ X✝ ◁ f✝ ≫ (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom =
    (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Y✝)).hom ≫ f✝ ▷ X✝

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ Z✝ : CommAlgCat R
f✝ : Y✝ ⟶ Z✝
⊢ Hom.hom (X✝ ◁ f✝ ≫ (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom) =
    Hom.hom ((isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Y✝)).hom ≫ f✝ ▷ X✝)
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ : CommAlgCat R
f✝ : X✝ ⟶ Y✝
Z✝ : CommAlgCat R
⊢ f✝ ▷ Z✝ ≫ (isoMk (Algebra.TensorProduct.comm R ↑Y✝ ↑Z✝)).hom =
    (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom ≫ Z✝ ◁ f✝

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ : CommAlgCat R
f✝ : X✝ ⟶ Y✝
Z✝ : CommAlgCat R
⊢ Hom.hom (f✝ ▷ Z✝ ≫ (isoMk (Algebra.TensorProduct.comm R ↑Y✝ ↑Z✝)).hom) =
    Hom.hom ((isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom ≫ Z✝ ◁ f✝)
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
⊢ (α_ S T U).hom ≫ (isoMk (Algebra.TensorProduct.comm R ↑S ↑(T ⊗ U))).hom ≫ (α_ T U S).hom =
    (isoMk (Algebra.TensorProduct.comm R ↑S ↑T)).hom ▷ U ≫
      (α_ T S U).hom ≫ T ◁ (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
⊢ Hom.hom ((α_ S T U).hom ≫ (isoMk (Algebra.TensorProduct.comm R ↑S ↑(T ⊗ U))).hom ≫ (α_ T U S).hom) =
    Hom.hom
      ((isoMk (Algebra.TensorProduct.comm R ↑S ↑T)).hom ▷ U ≫
        (α_ T S U).hom ≫ T ◁ (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)
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✝ : ∀ (A B : C), IsIso (prodComparison F A B)
⊢ PreservesLimitsOfShape (Discrete WalkingPair) F

Tactic:
by
  constructor
  intro K
  refine @preservesLimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoPair K).symm ?_
  apply preservesLimit_pair_of_isIso_prodComparison

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
⊢ (α_ S T U).inv ≫ (isoMk (Algebra.TensorProduct.comm R ↑(S ⊗ T) ↑U)).hom ≫ (α_ U S T).inv =
    S ◁ (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom ≫
      (α_ S U T).inv ≫ (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom ▷ T

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
⊢ Hom.hom ((α_ S T U).inv ≫ (isoMk (Algebra.TensorProduct.comm R ↑(S ⊗ T) ↑U)).hom ≫ (α_ U S T).inv) =
    Hom.hom
      (S ◁ (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom ≫
        (α_ S U T).inv ≫ (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom ▷ T)
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.Monoidal
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μIso F X Y).symm = prodComparisonIso F X Y

Tactic:
ext : 1

Goal state after:
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.Monoidal
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μIso F X Y).symm.hom = (prodComparisonIso F X Y).hom
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ f = lift g (h ≫ ι) ≫ μ → lift f h ≫ μ = g

Tactic:
rintro rfl; simp [lift_lift_assoc]

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ lift f h ≫ μ = g → f = lift g (h ≫ ι) ≫ μ

Tactic:
rintro rfl; simp [lift_lift_assoc]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M N P : ModuleCat R
f : (MonoidalCategory.tensorLeft M).obj N ⟶ P
⊢ (fun f ↦ (β_ M N).hom ≫ ↟(TensorProduct.lift (Hom.hom₂ f)))
      ((fun f ↦ ofHom₂ ((TensorProduct.mk R ↑N ↑M).compr₂ (Hom.hom ((β_ N M).hom ≫ f)))) f) =
    f

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommRing R
M N P : ModuleCat R
f : (MonoidalCategory.tensorLeft M).obj N ⟶ P
⊢ Hom.hom
      ((fun f ↦ (β_ M N).hom ≫ ↟(TensorProduct.lift (Hom.hom₂ f)))
        ((fun f ↦ ofHom₂ ((TensorProduct.mk R ↑N ↑M).compr₂ (Hom.hom ((β_ N M).hom ≫ f)))) f)) =
    Hom.hom f
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M X'✝ X✝ Y✝ : ModuleCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y✝
⊢ (M.monoidalClosedHomEquiv X'✝ Y✝).symm (f✝ ≫ g✝) =
    (MonoidalCategory.tensorLeft M).map f✝ ≫ (M.monoidalClosedHomEquiv X✝ Y✝).symm g✝

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommRing R
M X'✝ X✝ Y✝ : ModuleCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y✝
⊢ Hom.hom ((M.monoidalClosedHomEquiv X'✝ Y✝).symm (f✝ ≫ g✝)) =
    Hom.hom ((MonoidalCategory.tensorLeft M).map f✝ ≫ (M.monoidalClosedHomEquiv X✝ Y✝).symm g✝)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ MonoidalClosed.uncurry (𝟙 ((ihom M).obj N)) =
    ↟((TensorProduct.uncurry (RingHom.id R) ↑M ↑((ihom M).obj N) ↑N)
        (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip))

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ Hom.hom (MonoidalClosed.uncurry (𝟙 ((ihom M).obj N))) =
    Hom.hom
      (↟((TensorProduct.uncurry (RingHom.id R) ↑M ↑((ihom M).obj N) ↑N)
          (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip)))
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case e'_4.inr
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : ℵ₀ ≤ #↑s
⊢ max #↑s ℵ₀ = max (lift.{u, 0} #(Fin 6) + #↑s) ℵ₀

Tactic:
· rw [max_eq_left h, add_eq_right h (this.le.trans h), max_eq_left h]

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
b : Basis ι R M
inst✝ : Fintype ι
f : Dual R M
m : M
⊢ ∑ x, f (b x) * (b.coord x) m = f m

Tactic:
mul_comm (f _),

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Fintype ι
f : Dual R M
m : M
⊢ ∑ x, (b.coord x) m * f (b x) = f m
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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : ↑n < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #↑t = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
⊢ ∃ x, LinearIndependent R (Fin.cons x v)

Tactic:
have : range v ≠ t := by
    refine fun e ↦ h.ne ?_
    rw [← e, ← lift_injective.eq_iff, mk_range_eq_of_injective hv.injective] at h₂
    simpa only [mk_fintype, Fintype.card_fin, lift_natCast, lift_id'] using h₂

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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : ↑n < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #↑t = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
this : Set.range v ≠ t
⊢ ∃ x, LinearIndependent R (Fin.cons x v)
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional K V
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
⊢ span K (Set.range b) = ⊤

Tactic:
by
  by_contra ne_top
  rw [← finrank_span_eq_card lin_ind] at card_eq
  exact ne_of_lt (Submodule.finrank_lt ne_top) card_eq

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

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
⊢ ∀ (a : Subalgebra F E), a = ⊥ ∨ a = ⊤

Tactic:
intro S
      have : FiniteDimensional F E := .of_finrank_eq_succ hr
      have : FiniteDimensional F S :=
        FiniteDimensional.finiteDimensional_submodule (Subalgebra.toSubmodule S)
      have : finrank F S ≤ 2 := hr ▸ S.toSubmodule.finrank_le
      have : 0 < finrank F S := finrank_pos_iff.mpr inferInstance
      interval_cases h : finrank F { x // x ∈ S }
      · left
        exact Subalgebra.eq_bot_of_finrank_one h
      · right
        rw [← hr] at h
        rw [← Algebra.toSubmodule_eq_top]
        exact eq_top_of_finrank_eq h

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

Goal state before:
pp: case mp
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : (B x) y = 0
⊢ (B (a • x)) y = 0

pp: case mpr
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : (B (a • x)) y = 0
⊢ (B x) y = 0

Tactic:
· rw [map_smulₛₗ₂, H, smul_zero]

Goal state after:
case mpr
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : (B (a • x)) y = 0
⊢ (B x) y = 0
Module: Mathlib.Algebra.Category.FGModuleCat.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
V : FGModuleCat K
⊢ FGModuleCatDual K V ◁ FGModuleCatCoevaluation K V ≫
      (α_ (FGModuleCatDual K V) V (FGModuleCatDual K V)).inv ≫ FGModuleCatEvaluation K V ▷ FGModuleCatDual K V =
    (ρ_ (FGModuleCatDual K V)).hom ≫ (λ_ (FGModuleCatDual K V)).inv

Tactic:
ext : 1

Goal state after:
K : Type u
inst✝ : Field K
V : FGModuleCat K
⊢ ModuleCat.Hom.hom
      (FGModuleCatDual K V ◁ FGModuleCatCoevaluation K V ≫
          (α_ (FGModuleCatDual K V) V (FGModuleCatDual K V)).inv ≫
            FGModuleCatEvaluation K V ▷ FGModuleCatDual K V).hom =
    ModuleCat.Hom.hom ((ρ_ (FGModuleCatDual K V)).hom ≫ (λ_ (FGModuleCatDual K V)).inv).hom
Module: Mathlib.Algebra.Category.FGModuleCat.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
V : FGModuleCat K
⊢ FGModuleCatCoevaluation K V ▷ V ≫ (α_ V (FGModuleCatDual K V) V).hom ≫ V ◁ FGModuleCatEvaluation K V =
    (λ_ V).hom ≫ (ρ_ V).inv

Tactic:
ext : 1

Goal state after:
K : Type u
inst✝ : Field K
V : FGModuleCat K
⊢ ModuleCat.Hom.hom
      (FGModuleCatCoevaluation K V ▷ V ≫ (α_ V (FGModuleCatDual K V) V).hom ≫ V ◁ FGModuleCatEvaluation K V).hom =
    ModuleCat.Hom.hom ((λ_ V).hom ≫ (ρ_ V).inv).hom
Module: Mathlib.Algebra.Category.ModuleCat.Products

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
ι : Type v
Z : ι → ModuleCat R
inst✝ : DecidableEq ι
s : Cocone (Discrete.functor Z)
f : (coproductCocone Z).pt ⟶ s.pt
h : ∀ (j : Discrete ι), (coproductCocone Z).ι.app j ≫ f = s.ι.app j
⊢ f = ↟(toModule R ι ↑s.1 fun i ↦ Hom.hom (s.ι.app { as := i }))

Tactic:
ext : 1

Goal state after:
R : Type u
inst✝¹ : Ring R
ι : Type v
Z : ι → ModuleCat R
inst✝ : DecidableEq ι
s : Cocone (Discrete.functor Z)
f : (coproductCocone Z).pt ⟶ s.pt
h : ∀ (j : Discrete ι), (coproductCocone Z).ι.app j ≫ f = s.ι.app j
⊢ Hom.hom f = Hom.hom (↟(toModule R ι ↑s.1 fun i ↦ Hom.hom (s.ι.app { as := i })))
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
h : 1 ∈ (dualTensorHom R M M).range
⊢ Module.Finite R M ∧ Projective R M

Tactic:
have ⟨t, eq⟩ := h
  obtain ⟨s, rfl⟩ := TensorProduct.exists_finset t
  let f : (s → R) →ₗ[R] M := Fintype.linearCombination R (·.1.2)
  have : f ∘ₗ pi (·.1.1) = 1 := by
    ext; simp [f, ← eq, Fintype.linearCombination_apply, ← s.sum_coe_sort]
  exact ⟨.of_surjective f (surjective_of_comp_eq_id _ _ this), .of_split _ f this⟩

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

Goal state before:
pp: 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
F : WalkingParallelPair ⥤ C
⊢ ∀ (s : Cocone F) (m : (coequalizerCocone F).pt ⟶ s.pt),
    (∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = s.ι.app j) →
      m = pushout.desc (s.ι.app WalkingParallelPair.one) (s.ι.app WalkingParallelPair.one) ⋯

Tactic:
intro c m J

Goal state after:
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
F : WalkingParallelPair ⥤ C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j
⊢ m = pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map (q.rightSection ≫ π) = 𝟙 (F.obj Z)

Tactic:
q.rightSection_π,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map (𝟙 Z) = 𝟙 (F.obj Z)
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Φ : Subspace K (Dual K V)
⊢ finrank K ↥(dualCoannihilator Φ) = finrank K ↥(dualAnnihilator Φ)

Tactic:
by
  rw [Submodule.dualCoannihilator, ← Module.evalEquiv_toLinearMap]
  exact LinearEquiv.finrank_eq (LinearEquiv.ofSubmodule' _ _)

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 : M ⟶ N
s : Cofork f 0
m : (cokernelCocone f).pt ⟶ s.pt
h : Cofork.π (cokernelCocone f) ≫ m = s.π
this : Epi (↟(Hom.hom f).range.mkQ)
⊢ ↟(Hom.hom f).range.mkQ ≫ m = ↟(Hom.hom f).range.mkQ ≫ ↟((Hom.hom f).range.liftQ (Hom.hom s.π) ⋯)

Tactic:
exact h

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 : C
f : X ⟶ Y
Z : C
l : IsColimit (CokernelCofork.ofπ 0 ⋯)
Z✝ : C
u v : Y ⟶ Z✝
huv : f ≫ u = f ≫ v
⊢ u = v

Tactic:
obtain ⟨W, w, hw, hl⟩ := normalMonoOfMono (equalizer.ι u v)
    obtain ⟨m, hm⟩ := equalizer.lift' f huv
    have hwf : f ≫ w = 0 := by rw [← hm, Category.assoc, hw, comp_zero]
    obtain ⟨n, hn⟩ := CokernelCofork.IsColimit.desc' l _ hwf
    rw [Cofork.π_ofπ, zero_comp] at hn
    have : IsIso (equalizer.ι u v) := by apply isIso_limit_cone_parallelPair_of_eq hn.symm hl
    apply (cancel_epi (equalizer.ι u v)).1
    exact equalizer.condition _ _

Goal state after:
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
x : ↑B
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↑B
hz : (fun x ↦ x • ↑(Hom.hom f).range) z = ↑y
⊢ (fun x ↦ x • ↑(Hom.hom f).range) (x * z) = x • ↑y

Tactic:
simp [← hz, smul_smul]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ QuasiIso φ ↔ IsIso (leftHomologyMap' φ h₁ h₂)

Tactic:
by
  have γ : LeftHomologyMapData φ h₁ h₂ := default
  rw [γ.quasiIso_iff, γ.leftHomologyMap'_eq]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ QuasiIso φ ↔ IsIso (S₂.liftCycles φ.τ₂ ⋯)

Tactic:
let H : LeftHomologyMapData φ (LeftHomologyData.ofZeros S₁ hf₁ hg₁)
      (LeftHomologyData.ofIsLimitKernelFork S₂ hf₂ _ S₂.cyclesIsKernel) :=
    { φK := S₂.liftCycles φ.τ₂ (by rw [φ.comm₂₃, hg₁, zero_comp])
      φH := S₂.liftCycles φ.τ₂ (by rw [φ.comm₂₃, hg₁, zero_comp]) }

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
H : LeftHomologyMapData φ (LeftHomologyData.ofZeros S₁ hf₁ hg₁)
  (LeftHomologyData.ofIsLimitKernelFork S₂ hf₂ (KernelFork.ofι S₂.iCycles ⋯) S₂.cyclesIsKernel) :=
  { φK := S₂.liftCycles φ.τ₂ ⋯, φH := S₂.liftCycles φ.τ₂ ⋯, commi := ⋯, commf' := ⋯, commπ := ⋯ }
⊢ QuasiIso φ ↔ IsIso (S₂.liftCycles φ.τ₂ ⋯)
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
hK : ψ₁.φK = ψ₂.φK
⊢ ψ₁ = ψ₂

Tactic:
have hH : ψ₁.φH = ψ₂.φH := by rw [← cancel_epi h₁.π, commπ, commπ, hK]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
hK : ψ₁.φK = ψ₂.φK
hH : ψ₁.φH = ψ₂.φH
⊢ ψ₁ = ψ₂
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
A : C
f₁ f₂ : A ⟶ S.rightHomology
h : f₁ ≫ S.rightHomologyι = f₂ ≫ S.rightHomologyι
⊢ f₁ = f₂

Tactic:
simpa only [rightHomology_ext_iff]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ S.homologyπ ≫ h.homologyIso.hom = h.cyclesIso.hom ≫ h.π

Tactic:
dsimp only [homologyπ, homologyIso]
  simp only [Iso.trans_hom, Iso.symm_hom, assoc, Iso.hom_inv_id_assoc,
    leftHomologyπ_comp_leftHomologyIso_hom]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
⊢ S.liftCycles k hk ≫ h.cyclesIso.hom = h.liftK k hk

Tactic:
by
  simp only [← cancel_mono h.i, assoc, LeftHomologyData.cyclesIso_hom_comp_i,
    liftCycles_i, LeftHomologyData.liftK_i]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : h₁.IsPreservedBy F
inst✝ : h₂.IsPreservedBy F
⊢ (h₁.map F).f' ≫ F.map ψ.φK = (F.mapShortComplex.map φ).τ₁ ≫ (h₂.map F).f'

Tactic:
by simpa only [LeftHomologyData.map_f', F.map_comp] using! F.congr_map ψ.commf'

Goal state after: