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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
x y : F.Elements
f : y ⟶ x
⊢ ((𝟭 F.Elementsᵒᵖ).map (op f) ≫
        (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op y)))) (unop (op y))
              (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op y)))).fst) ⋯).op.hom).unop =
    ((isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op x)))) (unop (op x))
              (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op x)))).fst) ⋯).op.hom ≫
        (toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).map (op f)).unop

Tactic:
by ext; simp

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u₂
inst✝² : Category.{v₂, u₂} C
inst✝¹ : IsConnected J
F : J ⥤ C
inst✝ : HasLimit F
c : Cone F
hc : IsLimit c
⊢ limMap c.π =
    ((limit.isLimit ((Functor.const J).obj c.pt)).conePointUniqueUpToIso (isLimitConstCone J c.pt) ≪≫
        hc.conePointUniqueUpToIso (limit.isLimit F)).hom

Tactic:
ext j

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u₂
inst✝² : Category.{v₂, u₂} C
inst✝¹ : IsConnected J
F : J ⥤ C
inst✝ : HasLimit F
c : Cone F
hc : IsLimit c
j : J
⊢ limMap c.π ≫ limit.π F j =
    ((limit.isLimit ((Functor.const J).obj c.pt)).conePointUniqueUpToIso (isLimitConstCone J c.pt) ≪≫
          hc.conePointUniqueUpToIso (limit.isLimit F)).hom ≫
      limit.π F j
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x y : WithTerminal C ⥤ D
f : x ⟶ y
t : WithTerminal C
⊢ ((𝟭 (WithTerminal C ⥤ D)).map f ≫
          (liftUnique (incl ⋙ y) (fun x ↦ y.map (starTerminal.from (of x))) ⋯ y (Iso.refl (incl ⋙ y))
              (Iso.refl (y.obj star)) ⋯).hom).app
      t =
    ((liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starTerminal.from (of x_1))) ⋯ x (Iso.refl (incl ⋙ x))
              (Iso.refl (x.obj star)) ⋯).hom ≫
          ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
            f).app
      t

Tactic:
cases t <;> simp [incl]

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u₂
inst✝² : Category.{v₂, u₂} C
inst✝¹ : IsConnected J
F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
hc : IsColimit c
⊢ colimMap c.ι =
    ((colimit.isColimit F).coconePointUniqueUpToIso hc ≪≫
        (isColimitConstCocone J c.pt).coconePointUniqueUpToIso (colimit.isColimit ((Functor.const J).obj c.pt))).hom

Tactic:
ext j

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u₂
inst✝² : Category.{v₂, u₂} C
inst✝¹ : IsConnected J
F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
hc : IsColimit c
j : J
⊢ colimit.ι F j ≫ colimMap c.ι =
    colimit.ι F j ≫
      ((colimit.isColimit F).coconePointUniqueUpToIso hc ≪≫
          (isColimitConstCocone J c.pt).coconePointUniqueUpToIso (colimit.isColimit ((Functor.const J).obj c.pt))).hom
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit c
⊢ Nonempty (IsColimit (H.mapCocone c))

Tactic:
refine ⟨isColimitExtendCoconeEquiv (G := G ⋙ H) F (H.mapCocone c) ?_⟩

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit c
⊢ IsColimit (extendCocone.obj (H.mapCocone c))
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : HasColimitsOfShape D E
inst✝ : HasColimitsOfShape C E
X✝ Y✝ : D ⥤ E
f : X✝ ⟶ Y✝
⊢ ((whiskeringLeft C D E).obj F ⋙ colim).map f ≫ (colimitIso F Y✝).hom = (colimitIso F X✝).hom ≫ colim.map f

Tactic:
simp only [comp_obj, whiskeringLeft_obj_obj, colim_obj, comp_map, whiskeringLeft_obj_map,
      colim_map, colimitIso_hom]
    ext
    simp only [comp_obj, ι_colimMap_assoc, whiskerLeft_app, colimit.ι_pre, colimit.ι_pre_assoc,
      ι_colimMap]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y P : Cᵒᵖ
f g : X ⟶ Y
ι ι' : P ⟶ X
w : ι ≫ f = ι ≫ g
w' : f.unop ≫ ι'.unop = g.unop ≫ ι'.unop
h : ι = ι'
⊢ (ofι ι w).unop.π ≫ (Iso.refl (ofι ι w).unop.pt).hom = (Cofork.ofπ ι'.unop w').π

Tactic:
simp [Fork.unop_π, h]

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x y : WithInitial C ⥤ D
f : x ⟶ y
t : WithInitial C
⊢ ((𝟭 (WithInitial C ⥤ D)).map f ≫
          (liftUnique (incl ⋙ y) (fun x ↦ y.map (starInitial.to (of x))) ⋯ y (Iso.refl (incl ⋙ y))
              (Iso.refl (y.obj star)) ⋯).hom).app
      t =
    ((liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starInitial.to (of x_1))) ⋯ x (Iso.refl (incl ⋙ x))
              (Iso.refl (x.obj star)) ⋯).hom ≫
          ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
            f).app
      t

Tactic:
cases t <;> simp [incl]

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

Goal state before:
pp: case h₁.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) ⋯) ⋯) ≫
        snd (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
      fst (snd f' g') i₂ =
    (𝟙 (pullback (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
      fst (snd f' g') i₂

Tactic:
apply pullback.hom_ext
        · simp only [Category.assoc, lift_snd_assoc, lift_fst_assoc, lift_fst, Category.id_comp]
          rw [← condition_assoc, condition]
        · simp only [Category.assoc, lift_snd, lift_fst_assoc, lift_snd_assoc, Category.id_comp]
          rw [condition]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : MonObj B
f g h : A ⟶ B
this : lift (lift f g ≫ μ) h ≫ μ = lift f (lift g h) ≫ B ◁ μ ≫ μ
⊢ lift (lift f g ≫ μ) h ≫ μ = lift f (lift g h ≫ μ) ≫ μ

Tactic:
lift_whiskerLeft_assoc

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : MonObj B
f g h : A ⟶ B
this : lift (lift f g ≫ μ) h ≫ μ = lift f (lift g h ≫ μ) ≫ μ
⊢ lift (lift f g ≫ μ) h ≫ μ = lift f (lift g h ≫ μ) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z : C
f : Y ⟶ Z
⊢ X ◁ f ≫ snd X Z = snd X Y ≫ f

Tactic:
simp [snd_def, whisker_exchange_assoc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z : C
⊢ (α_ X Y Z).hom ≫ snd X (Y ⊗ Z) ≫ snd Y Z = snd (X ⊗ Y) Z

Tactic:
by
  simp [snd_def, ← leftUnitor_whiskerRight_assoc, -leftUnitor_whiskerRight,
    ← comp_whiskerRight_assoc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z : C
⊢ (α_ X Y Z).inv ≫ snd (X ⊗ Y) Z = snd X (Y ⊗ Z) ≫ snd Y Z

Tactic:
by
  simp [snd_def, ← leftUnitor_whiskerRight_assoc, -leftUnitor_whiskerRight,
    ← comp_whiskerRight_assoc]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : CoalgebraStruct R C
f : WithConv (C →ₗ[R] A)
⊢ 0 * f = 0

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : CoalgebraStruct R C
f : WithConv (C →ₗ[R] A)
⊢ f * 0 = 0

Tactic:
by ext; simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
A : C
⊢ prodComparisonNatTrans (𝟭 C) A = 𝟙 ((curriedTensor C).obj A ⋙ 𝟭 C)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
x y : A
⊢ toConv (toSpanSingleton R A x) * toConv (toSpanSingleton R A y) = toConv (toSpanSingleton R A (x * y))

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
⊢ (mul' R A ∘ₗ lTensor A (mul' R A)) ∘ₗ (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ =
    mul' R A ∘ₗ (f.ofConv ⊗ₘ mul' R A ∘ₗ (g.ofConv ⊗ₘ h.ofConv) ∘ₗ δ) ∘ₗ δ

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
⊢ counit ((antipode R) a) = counit a

Tactic:
by
  calc
        counit (antipode R a)
    _ = counit (∑ i ∈ (ℛ R a).index, (ℛ R a).left i * antipode R ((ℛ R a).right i)) := by
      simp_rw [map_sum, counit_mul, ← smul_eq_mul, ← map_smul, ← map_sum, sum_counit_smul]
    _ = counit a := by simpa using congr(counit (R := R) $(sum_mul_antipode_eq_smul (ℛ R a)))

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ LinearMap.mul' R R ∘ₗ LinearMap.rTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul =
    Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ LinearMap.mul' R R ∘ₗ LinearMap.lTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul =
    Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit

Tactic:
by ext; simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ lift (ι ≫ f) f ≫ μ = toUnit A ≫ η

Tactic:
by
  have := left_inv A =≫ f
  rwa [assoc, IsMonHom.mul_hom, assoc, IsMonHom.one_hom, lift_map_assoc, id_comp] at this

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
⊢ δ ∘ₗ ofConv 1 = Algebra.linearMap R (C ⊗[R] C) ∘ₗ ε

Tactic:
simp [LinearMap.convOne_def, show (δ ∘ₗ η : R →ₗ[R] C ⊗[R] C) = η by ext; simp; rfl,
          ← comp_assoc]

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
H : (lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv) = f.ofConv.comp (lmul' R)
⊢ f⁻¹ * f = 1

Tactic:
trans toConv <| ((lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv)).comp
      ((Algebra.TensorProduct.map
      (HopfAlgebra.antipodeAlgHom R A) (.id _ _)).comp (comulAlgHom R A))

Goal state after:
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
H : (lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv) = f.ofConv.comp (lmul' R)
⊢ f⁻¹ * f =
    toConv
      (((lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv)).comp
        ((Algebra.TensorProduct.map (antipodeAlgHom R A) (AlgHom.id R A)).comp (comulAlgHom R A)))

R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
H : (lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv) = f.ofConv.comp (lmul' R)
⊢ toConv
      (((lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv)).comp
        ((Algebra.TensorProduct.map (antipodeAlgHom R A) (AlgHom.id R A)).comp (comulAlgHom R A))) =
    1
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
⊢ f⁻¹ * f = 1

Tactic:
have H : (lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv) =
      f.ofConv.comp (lmul' R) := by ext <;> simp
    trans toConv <| ((lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv)).comp
      ((Algebra.TensorProduct.map
      (HopfAlgebra.antipodeAlgHom R A) (.id _ _)).comp (comulAlgHom R A))
    · rw [AlgHom.comp_assoc, ← AlgHom.comp_assoc (Algebra.TensorProduct.map f.ofConv f.ofConv),
        ← Algebra.TensorProduct.map_comp]; rfl
    rw [H, AlgHom.comp_assoc, WithConv.ext_iff, ← AlgHom.toLinearMap_injective.eq_iff]
    change f.ofConv.toLinearMap.comp (toConv (antipode R (A := A)) * toConv LinearMap.id).ofConv =
      ofConv (1 : WithConv <| A →ₗ[R] C)
    rw [LinearMap.antipode_mul_id]
    ext
    simp

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 ε
i : ι
⊢ h.basis.repr (e i) = Finsupp.single i 1

Tactic:
ext j

Goal state after:
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 ε
i j : ι
⊢ (h.basis.repr (e i)) j = (Finsupp.single i 1) j
Module: Mathlib.LinearAlgebra.Dimension.DivisionRing

Goal state before:
pp: K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
| Module.rank K (V₂ × V₃)

Tactic:
rank_eq_of_surjective hf

Goal state after:
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
| Module.rank K V + Module.rank K ↥(db.coprod eb).ker
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
f : Dual R M
m : M
⊢ Dual.transpose ((dualTensorHom R M M) (f ⊗ₜ[R] m)) =
    (dualTensorHom R (Dual R M) (Dual R M)) ((Dual.eval R M) m ⊗ₜ[R] f)

Tactic:
by
  ext f' m'
  simp only [Dual.transpose_apply, coe_comp, Function.comp_apply, dualTensorHom_apply,
    map_smulₛₗ, RingHom.id_apply, smul_eq_mul, Dual.eval_apply,
    LinearMap.smul_apply]
  exact mul_comm _ _

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
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
b : Basis ι R M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ (∑ i, (TensorProduct.mk R (Dual R M) N) (b.dualBasis i) ∘ₗ applyₗ (b i)) ∘ₗ dualTensorHom R M N = LinearMap.id

Tactic:
ext f m
      simp only [applyₗ_apply_apply, coe_sum, dualTensorHom_apply, mk_apply, id_coe, _root_.id,
        Fintype.sum_apply, Function.comp_apply, Basis.coe_dualBasis, coe_comp, compr₂ₛₗ_apply,
        tmul_smul, smul_tmul', ← sum_tmul, Basis.sum_dual_apply_smul_coord]

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

Goal state before:
pp: case mp
R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I : R₁ →+* R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B.IsAlt
x✝¹ x✝ : M₁
⊢ (B x✝¹) x✝ = -(B x✝) x✝¹

Tactic:
exact (h.neg _ _).symm

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Finite ι
h : Function.Bijective ⇑(dualTensorHom R M N)
⊢ ↑(Finsupp.linearEquivFunOnFinite R N ι) ∘ₗ ↑(Finsupp.linearEquivFunOnFinite R N ι).symm = LinearMap.id

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, (B x) y = 0
y : M
⊢ ∃ u ∈ W, ∃ v ∈ B.ker, u + v = y

Tactic:
rw [← Submodule.mem_sup, hW.sup_eq_top]

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, (B x) y = 0
y : M
⊢ y ∈ ⊤
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: case refine_3.right
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)
⊢ (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app { as := WalkingPair.right } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
        c.ι.app WalkingParallelPair.one =
    (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app { as := WalkingPair.right } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
        c.ι.app WalkingParallelPair.one

Tactic:
· simp only [BinaryCofan.ι_app_right, BinaryCofan.mk_inr, ←
              G.map_comp_assoc, coprod.inr_desc]
            exact
              (c.ι.naturality WalkingParallelPairHom.left).trans
                (c.ι.naturality WalkingParallelPairHom.right).symm

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x : M
hx : x ∉ p
hp' : Projective R (M ⧸ p)
⊢ ∃ f, f (p.mkQ x) ≠ 0

Tactic:
← Submodule.Quotient.mk_eq_zero,

Goal state after:
R : Type u_3
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x : M
hx : ¬Quotient.mk x = 0
hp' : Projective R (M ⧸ p)
⊢ ∃ f, f (p.mkQ x) ≠ 0
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i ↦ p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
this : ⨅ i, (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i, c i • L' i = K'
i : ι
| c i • L i

Tactic:
rw [← p.liftQ_mkQ (L i) (iInf_le _ i)]

Goal state after:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i ↦ p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
this : ⨅ i, (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i, c i • L' i = K'
i : ι
| c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∏ᶜ K.obj
Q : C := ∏ᶜ fun f ↦ K.obj f.fst.2
s : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ PreservesLimit K G

Tactic:
apply preservesLimit_of_preserves_limit_cone
        (buildIsLimit s t (by simp [P, s]) (by simp [P, t]) (limit.isLimit _)
          (limit.isLimit _) (limit.isLimit _))

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ⋯
Q : C := ⋯
s : P ⟶ Q := ⋯
t : P ⟶ Q := ⋯
I : C := ⋯
i : I ⟶ P := ⋯
⊢ IsLimit (G.mapCone (buildLimit s t ⋯ ⋯ (limit.cone (parallelPair s t))))