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

Goal state before:
pp: case zero
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y B X : C
f : X ⟶ B
inst✝ : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
this : f ≫ EffectiveEpi.desc f (s.ι.app WalkingParallelPair.one) ⋯ = s.ι.app WalkingParallelPair.one
⊢ (Cofork.ofπ f ⋯).ι.app WalkingParallelPair.zero ≫ EffectiveEpi.desc f (s.ι.app WalkingParallelPair.one) ⋯ =
    s.ι.app WalkingParallelPair.zero

pp: case one
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y B X : C
f : X ⟶ B
inst✝ : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
this : f ≫ EffectiveEpi.desc f (s.ι.app WalkingParallelPair.one) ⋯ = s.ι.app WalkingParallelPair.one
⊢ (Cofork.ofπ f ⋯).ι.app WalkingParallelPair.one ≫ EffectiveEpi.desc f (s.ι.app WalkingParallelPair.one) ⋯ =
    s.ι.app WalkingParallelPair.one

Tactic:
all_goals simp_all

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 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₂
⊢ (fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f =
    map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯ ≫
      map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯

Tactic:
by
        ext
        · simp only [Category.assoc, diagonal_fst, Category.comp_id, limit.lift_π,
          PullbackCone.mk_π_app, limit.lift_π_assoc, cospan_left]
        · simp only [condition_assoc, Category.assoc, diagonal_snd, Category.comp_id, limit.lift_π,
          PullbackCone.mk_π_app, limit.lift_π_assoc, cospan_right]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P Q : ObjectProperty C
inst✝ : P.ContainsZero
⊢ ∃ Z, IsZero Z ∧ P.isoClosure Z

Tactic:
obtain ⟨Z, hZ, hP⟩ := P.exists_prop_of_containsZero
    exact ⟨Z, hZ, P.le_isoClosure _ hP⟩

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
inst✝ : BraidedCategory C
M : Mon C
f : M ⟶ 𝟙_ (Mon C)
⊢ f = { hom := toUnit M.X, isMonHom_hom := ⋯ }

Tactic:
by ext; exact toUnit_unique ..

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

Goal state before:
pp: case h_fst
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
A B B' : C
g : B ⟶ B'
⊢ (F.map (A ◁ g) ≫ prodComparison F A B') ≫ fst (F.obj A) (F.obj B') =
    (prodComparison F A B ≫ F.obj A ◁ F.map g) ≫ fst (F.obj A) (F.obj B')

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_snd
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
A B B' : C
g : B ⟶ B'
⊢ (F.map (A ◁ g) ≫ prodComparison F A B') ≫ snd (F.obj A) (F.obj B') =
    (prodComparison F A B ≫ F.obj A ◁ F.map g) ≫ snd (F.obj A) (F.obj B')

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_fst
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
A B A' : C
f : A ⟶ A'
⊢ (F.map (f ▷ B) ≫ prodComparison F A' B) ≫ fst (F.obj A') (F.obj B) =
    (prodComparison F A B ≫ F.map f ▷ F.obj B) ≫ fst (F.obj A') (F.obj B)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_snd
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
A B A' : C
f : A ⟶ A'
⊢ (F.map (f ▷ B) ≫ prodComparison F A' B) ≫ snd (F.obj A') (F.obj B) =
    (prodComparison F A B ≫ F.map f ▷ F.obj B) ≫ snd (F.obj A') (F.obj B)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_fst
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
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
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : CartesianMonoidalCategory E
G : D ⥤ E
A B A' B' x y : C
f : x ⟶ y
z : C
⊢ ((curriedTensor C ⋙ (Functor.whiskeringRight C C D).obj F).map f ≫ prodComparisonNatTrans F y).app z ≫
      fst (F.obj y) (F.obj z) =
    (prodComparisonNatTrans F x ≫ (F ⋙ curriedTensor D ⋙ (Functor.whiskeringLeft C D D).obj F).map f).app z ≫
      fst (F.obj y) (F.obj z)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_snd
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
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
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : CartesianMonoidalCategory E
G : D ⥤ E
A B A' B' x y : C
f : x ⟶ y
z : C
⊢ ((curriedTensor C ⋙ (Functor.whiskeringRight C C D).obj F).map f ≫ prodComparisonNatTrans F y).app z ≫
      snd (F.obj y) (F.obj z) =
    (prodComparisonNatTrans F x ≫ (F ⋙ curriedTensor D ⋙ (Functor.whiskeringLeft C D D).obj F).map f).app z ≫
      snd (F.obj y) (F.obj z)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
x✝¹ : P.FullSubcategory
x✝ : x✝¹ ⟶ 𝟙_ P.FullSubcategory
⊢ x✝.hom = (ObjectProperty.homMk (toUnit x✝¹.obj)).hom

Tactic:
apply toUnit_unique

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

Goal state before:
pp: case h_fst
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
X✝¹ Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
X✝ Y✝ : C
f : X✝ ⟶ Y✝
X : C
⊢ (CartesianMonoidalCategory.prodComparison F X✝ X ≫ F.map f ▷ F.obj X) ≫ fst (F.obj Y✝) (F.obj X) =
    (F.map (f ▷ X) ≫ CartesianMonoidalCategory.prodComparison F Y✝ X) ≫ fst (F.obj Y✝) (F.obj X)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_snd
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
X✝¹ Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
X✝ Y✝ : C
f : X✝ ⟶ Y✝
X : C
⊢ (CartesianMonoidalCategory.prodComparison F X✝ X ≫ F.map f ▷ F.obj X) ≫ snd (F.obj Y✝) (F.obj X) =
    (F.map (f ▷ X) ≫ CartesianMonoidalCategory.prodComparison F Y✝ X) ≫ snd (F.obj Y✝) (F.obj X)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_fst
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
X✝¹ Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
X✝ Y✝ X : C
g : X✝ ⟶ Y✝
⊢ (CartesianMonoidalCategory.prodComparison F X X✝ ≫ F.obj X ◁ F.map g) ≫ fst (F.obj X) (F.obj Y✝) =
    (F.map (X ◁ g) ≫ CartesianMonoidalCategory.prodComparison F X Y✝) ≫ fst (F.obj X) (F.obj Y✝)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_snd
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
X✝¹ Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
X✝ Y✝ X : C
g : X✝ ⟶ Y✝
⊢ (CartesianMonoidalCategory.prodComparison F X X✝ ≫ F.obj X ◁ F.map g) ≫ snd (F.obj X) (F.obj Y✝) =
    (F.map (X ◁ g) ≫ CartesianMonoidalCategory.prodComparison F X Y✝) ≫ snd (F.obj X) (F.obj Y✝)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_fst
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
X Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
x✝² x✝¹ x✝ : C
⊢ (CartesianMonoidalCategory.prodComparison F (x✝² ⊗ x✝¹) x✝ ≫
        CartesianMonoidalCategory.prodComparison F x✝² x✝¹ ▷ F.obj x✝ ≫ (α_ (F.obj x✝²) (F.obj x✝¹) (F.obj x✝)).hom) ≫
      fst (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝) =
    (F.map (α_ x✝² x✝¹ x✝).hom ≫
        CartesianMonoidalCategory.prodComparison F x✝² (x✝¹ ⊗ x✝) ≫
          F.obj x✝² ◁ CartesianMonoidalCategory.prodComparison F x✝¹ x✝) ≫
      fst (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_snd.h_fst
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
X Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
x✝² x✝¹ x✝ : C
⊢ ((CartesianMonoidalCategory.prodComparison F (x✝² ⊗ x✝¹) x✝ ≫
          CartesianMonoidalCategory.prodComparison F x✝² x✝¹ ▷ F.obj x✝ ≫ (α_ (F.obj x✝²) (F.obj x✝¹) (F.obj x✝)).hom) ≫
        snd (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝)) ≫
      fst (F.obj x✝¹) (F.obj x✝) =
    ((F.map (α_ x✝² x✝¹ x✝).hom ≫
          CartesianMonoidalCategory.prodComparison F x✝² (x✝¹ ⊗ x✝) ≫
            F.obj x✝² ◁ CartesianMonoidalCategory.prodComparison F x✝¹ x✝) ≫
        snd (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝)) ≫
      fst (F.obj x✝¹) (F.obj x✝)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_snd
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
X Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
x✝² x✝¹ x✝ : C
⊢ ((CartesianMonoidalCategory.prodComparison F (x✝² ⊗ x✝¹) x✝ ≫
          CartesianMonoidalCategory.prodComparison F x✝² x✝¹ ▷ F.obj x✝ ≫ (α_ (F.obj x✝²) (F.obj x✝¹) (F.obj x✝)).hom) ≫
        snd (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝)) ≫
      snd (F.obj x✝¹) (F.obj x✝) =
    ((F.map (α_ x✝² x✝¹ x✝).hom ≫
          CartesianMonoidalCategory.prodComparison F x✝² (x✝¹ ⊗ x✝) ≫
            F.obj x✝² ◁ CartesianMonoidalCategory.prodComparison F x✝¹ x✝) ≫
        snd (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝)) ≫
      snd (F.obj x✝¹) (F.obj x✝)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_snd
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
X Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
x✝ : C
⊢ (λ_ (F.obj x✝)).inv ≫ snd (𝟙_ D) (F.obj x✝) =
    (F.map (λ_ x✝).inv ≫
        CartesianMonoidalCategory.prodComparison F (𝟙_ C) x✝ ≫
          CartesianMonoidalCategory.terminalComparison F ▷ F.obj x✝) ≫
      snd (𝟙_ D) (F.obj x✝)

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_fst
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
X Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
x✝ : C
⊢ (ρ_ (F.obj x✝)).inv ≫ fst (F.obj x✝) (𝟙_ D) =
    (F.map (ρ_ x✝).inv ≫
        CartesianMonoidalCategory.prodComparison F x✝ (𝟙_ C) ≫
          F.obj x✝ ◁ CartesianMonoidalCategory.terminalComparison F) ≫
      fst (F.obj x✝) (𝟙_ D)

Tactic:
simp [← Functor.map_comp]

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

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

Tactic:
· rw [AlgHom.comp_assoc, ← AlgHom.comp_assoc (Algebra.TensorProduct.map f.ofConv f.ofConv),
        ← Algebra.TensorProduct.map_comp]; rfl

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)
⊢ 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.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H H₁ H₂ G : Grp C
f : G ⟶ 𝟙_ (Grp C)
⊢ f = homMk' (toUnit G.toMon)

Tactic:
by ext; exact toUnit_unique ..

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
⊢ x ◁ (λ_ ((ihom x).obj y)).inv ≫
      x ◁ curry (ρ_ x).hom ▷ (ihom x).obj y ≫
        (α_ x ((ihom x).obj x) ((ihom x).obj y)).inv ≫ (ihom.ev x).app x ▷ (ihom x).obj y ≫ (ihom.ev x).app y =
    uncurry (𝟙 ((ihom x).obj y))

Tactic:
associator_inv_naturality_middle_assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
x y : C
inst✝ : Closed x
⊢ x ◁ (λ_ ((ihom x).obj y)).inv ≫
      (α_ x (𝟙_ C) ((ihom x).obj y)).inv ≫
        (x ◁ curry (ρ_ x).hom) ▷ (ihom x).obj y ≫ (ihom.ev x).app x ▷ (ihom x).obj y ≫ (ihom.ev x).app y =
    uncurry (𝟙 ((ihom x).obj y))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
w x y z : C
inst✝² : Closed w
inst✝¹ : Closed x
inst✝ : Closed y
⊢ w ◁ (α_ ((ihom w).obj x) ((ihom x).obj y) ((ihom y).obj z)).inv ≫
      w ◁
          curry
              ((α_ w ((ihom w).obj x) ((ihom x).obj y)).inv ≫ (ihom.ev w).app x ▷ (ihom x).obj y ≫ (ihom.ev x).app y) ▷
            (ihom y).obj z ≫
        (α_ w ((ihom w).obj y) ((ihom y).obj z)).inv ≫ (ihom.ev w).app y ▷ (ihom y).obj z ≫ (ihom.ev y).app z =
    w ◁
        (ihom w).obj x ◁
          curry
            ((α_ x ((ihom x).obj y) ((ihom y).obj z)).inv ≫ (ihom.ev x).app y ▷ (ihom y).obj z ≫ (ihom.ev y).app z) ≫
      (α_ w ((ihom w).obj x) ((ihom x).obj z)).inv ≫ (ihom.ev w).app x ▷ (ihom x).obj z ≫ (ihom.ev x).app z

Tactic:
associator_inv_naturality_middle_assoc,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
w x y z : C
inst✝² : Closed w
inst✝¹ : Closed x
inst✝ : Closed y
⊢ w ◁ (α_ ((ihom w).obj x) ((ihom x).obj y) ((ihom y).obj z)).inv ≫
      (α_ w ((ihom w).obj x ⊗ (ihom x).obj y) ((ihom y).obj z)).inv ≫
        (w ◁
              curry
                ((α_ w ((ihom w).obj x) ((ihom x).obj y)).inv ≫
                  (ihom.ev w).app x ▷ (ihom x).obj y ≫ (ihom.ev x).app y)) ▷
            (ihom y).obj z ≫
          (ihom.ev w).app y ▷ (ihom y).obj z ≫ (ihom.ev y).app z =
    w ◁
        (ihom w).obj x ◁
          curry
            ((α_ x ((ihom x).obj y) ((ihom y).obj z)).inv ≫ (ihom.ev x).app y ▷ (ihom y).obj z ≫ (ihom.ev y).app z) ≫
      (α_ w ((ihom w).obj x) ((ihom x).obj z)).inv ≫ (ihom.ev w).app x ▷ (ihom x).obj z ≫ (ihom.ev x).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 : X ⟶ Y
⊢ X ◁ (λ_ ((ihom Y).obj Z)).inv ≫
      X ◁ curry' f ▷ (ihom Y).obj Z ≫
        (α_ X ((ihom X).obj Y) ((ihom Y).obj Z)).inv ≫ (ihom.ev X).app Y ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z =
    f ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z

Tactic:
associator_inv_naturality_middle_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
⊢ X ◁ (λ_ ((ihom Y).obj Z)).inv ≫
      (α_ X (𝟙_ C) ((ihom Y).obj Z)).inv ≫
        (X ◁ curry' f) ▷ (ihom Y).obj Z ≫ (ihom.ev X).app Y ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z =
    f ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z
Module: Mathlib.Data.W.Cardinal

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

Tactic:
by simp_rw [lift_id]; exact hκ

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

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝¹ : (a : α) → Fintype (β a)
inst✝ : (a : α) → Encodable (β a)
n : ℕ
t : WType β
h : t.depth ≤ n + 1
⊢ (a : α) × (β a → WType' β n)

Tactic:
by
    obtain ⟨a, f⟩ := t
    have h₀ : ∀ i : β a, WType.depth (f i) ≤ n := fun i =>
      Nat.le_of_lt_succ (lt_of_lt_of_le (WType.depth_lt_depth_mk a f i) h)
    exact ⟨a, fun i : β a => ⟨f i, h₀ i⟩⟩

Goal state after:
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
inst✝ : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
⊢ finrank K ↥(p ⊔ K ∙ v) + ?m.40 = finrank K ↥p + 1 + ?m.40

pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
⊢ ℕ

Tactic:
finrank_sup_add_finrank_inf_eq,

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
⊢ finrank K ↥p + finrank K ↥(K ∙ v) = finrank K ↥p + 1 + finrank K ↥(p ⊓ K ∙ 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
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)

Tactic:
by_cases! h_cases : m < finrank K V

Goal state after:
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : m < finrank K V
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)

case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : finrank K V ≤ m
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case neg
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
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
he : (B x) y * (B y) x = (B x) x * (B y) y
hz : (B x) y • x - (B x) x • y = 0
hL : LinearIndependent R ![x, y]
hx : ¬x = 0
h : (B x) x • y - (B x) y • x = 0
⊢ False

Tactic:
rw [sub_eq_add_neg, ← neg_smul, add_comm] at h

Goal state after:
case neg
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
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
he : (B x) y * (B y) x = (B x) x * (B y) y
hz : (B x) y • x - (B x) x • y = 0
hL : LinearIndependent R ![x, y]
hx : ¬x = 0
h : -(B x) y • x + (B x) x • y = 0
⊢ False
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
W : Subspace K V
⊢ finrank K ↥W + finrank K ↥(dualAnnihilator W) = finrank K V

Tactic:
rw [← W.quotEquivAnnihilator.finrank_eq, add_comm, Submodule.finrank_quotient_add_finrank]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
this✝¹ : HasFiniteColimits C
this✝ : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteCoproducts G

Tactic:
refine ⟨fun _ ↦ ?_⟩

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
this✝¹ : HasFiniteColimits C
this✝ : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝)) G
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✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
⊢ g ≫ b ≫ s.inr = 0 ≫ s.inr

Tactic:
rw [← Category.assoc, eq_whisker hgb]

Goal state after: