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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p // p ≫ p = p }
g : {X Y : C} → Retract Y X → Q X → α := fun {X Y} h hX ↦ ⟨⟨X, hX⟩, ⟨h.r ≫ h.i, ⋯⟩⟩
R : α → Prop := fun a ↦ ∃ X Y h, ∃ (hX : Q X), g h hX = a
X Y : Subtype R → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = ↑a
y x : C
hx : Q x
r : Retract y x
⊢ (r.r ≫ r.i) ≫ r.r ≫ r.i = r.r ≫ r.i

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.IsStableUnderColimitsOfShape J
X Y : C
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cocone X₁✝
c₂✝ : Cocone X₂✝
h₁ : IsColimit c₁✝
h₂ : IsColimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W.functorCategory J f
⊢ ∀ (j : J), c₁✝.ι.app j ≫ h₁.desc { pt := c₂✝.pt, ι := f ≫ c₂✝.ι } = f.app j ≫ c₂✝.ι.app j

Tactic:
by simp

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 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₃
⊢ (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).symm.hom ≫ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) =
    lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯

Tactic:
by simp

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 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₃
⊢ (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).symm.hom ≫ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) =
    lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯

Tactic:
by simp

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
⊢ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ ≫ fst g h = fst (fst f g) (fst f h) ≫ snd f g

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
H : P.diagonal f
⊢ (e.hom ≫ f) ≫ 𝟙 Z = e.hom ≫ f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
⊢ 𝟙 Y ≫ g ≫ f = g ≫ f

Tactic:
by simp

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
f : X ⟶ Y
inst✝ : HasPushout f f
H : IsIso (codiagonal f)
Z✝ : C
x✝¹ x✝ : Y ⟶ Z✝
e : f ≫ x✝¹ = f ≫ x✝
⊢ inl f f ≫ codiagonal f = inr f f ≫ codiagonal f

Tactic:
by simp

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✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ i ≫ f = 𝟙 S ≫ i ≫ f

Tactic:
by simp

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✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ i ≫ g = 𝟙 S ≫ i ≫ g

Tactic:
by simp

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✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ (i ≫ f) ≫ 𝟙 X = i ≫ f

Tactic:
by simp

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✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ (i ≫ g) ≫ 𝟙 Y = i ≫ g

Tactic:
by simp

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.map f.op g.op (f.op ≫ i.op) (g.op ≫ i.op) (𝟙 (Opposite.op X)) (𝟙 (Opposite.op Y)) i.op ⋯ ⋯ ≫
      (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)).hom =
    (pullbackIsoOpPushout f.op g.op).hom ≫
      (pullbackIsoOpPushout f.op g.op).inv ≫
        pullback.map f.op g.op (f.op ≫ i.op) (g.op ≫ i.op) (𝟙 (Opposite.op X)) (𝟙 (Opposite.op Y)) i.op ⋯ ⋯ ≫
          (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)).hom

Tactic:
by simp

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.diagonal i.op ≫ (pullbackIsoOpPushout i.op i.op).hom =
    (Iso.refl (Opposite.op T)).hom ≫ pullback.diagonal i.op ≫ (pullbackIsoOpPushout i.op i.op).hom

Tactic:
by simp

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.map (f.op ≫ i.op) (g.op ≫ i.op) i.op i.op f.op g.op (𝟙 (Opposite.op S)) ⋯ ⋯ ≫
      (pullbackIsoOpPushout i.op i.op).hom =
    (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)).hom ≫
      (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)).inv ≫
        pullback.map (f.op ≫ i.op) (g.op ≫ i.op) i.op i.op f.op g.op (𝟙 (Opposite.op S)) ⋯ ⋯ ≫
          (pullbackIsoOpPushout i.op i.op).hom

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape WalkingParallelPair
X Y : C
h : Retract X Y
hY : P Y
⊢ (h.r ≫ h.i) ≫ h.r = 𝟙 Y ≫ h.r

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : IsEmpty J
X : C
x✝ : Nonempty (IsTerminal X)
h : IsTerminal X
⊢ ∀ (j : J),
    P
      ({ diag := (Functor.const J).obj X, π := 𝟙 ((Functor.const J).obj X),
              isLimit :=
                (isLimitEquivIsTerminalOfIsEmpty C { pt := X, π := 𝟙 ((Functor.const J).obj X) }).symm h }.diag.obj
        j)

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : IsEmpty J
X : C
x✝ : Nonempty (IsInitial X)
h : IsInitial X
⊢ ∀ (j : J),
    P
      ({ diag := (Functor.const J).obj X, ι := 𝟙 ((Functor.const J).obj X),
              isColimit :=
                (isColimitEquivIsInitialOfIsEmpty C { pt := X, ι := 𝟙 ((Functor.const J).obj X) }).symm h }.diag.obj
        j)

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ Z₁ Z₂ : C
this : MonoidalCategoryStruct C :=
  { tensorObj := ofChosenFiniteProducts.tensorObj ℬ,
    whiskerLeft := fun X {x x_1} g ↦ ofChosenFiniteProducts.tensorHom ℬ (𝟙 X) g,
    whiskerRight := fun {x x_1} f Y ↦ ofChosenFiniteProducts.tensorHom ℬ f (𝟙 Y),
    tensorHom := fun {X₁ Y₁ X₂ Y₂} ↦ ofChosenFiniteProducts.tensorHom ℬ, tensorUnit := 𝒯.cone.pt,
    associator := BinaryFan.associatorOfLimitCone ℬ,
    leftUnitor := fun X ↦ BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X).isLimit,
    rightUnitor := fun X ↦ BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit }
x✝¹ : C
x✝ : x✝¹ ⟶ 𝟙_ C
⊢ ∀ (j : Discrete PEmpty.{1}), x✝ ≫ 𝒯.cone.π.app j = 𝒯.isLimit.lift (asEmptyCone x✝¹) ≫ 𝒯.cone.π.app j

Tactic:
by simp

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
X Y Z : C
x✝ : Z ⟶ X ⊗ Y
⊢ (fun f ↦ lift f.1 f.2) ((fun f ↦ (f ≫ fst X Y, f ≫ snd X Y)) x✝) = x✝

Tactic:
by simp

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
X Y Z : C
x✝ : (Z ⟶ X) × (Z ⟶ Y)
⊢ (fun f ↦ (f ≫ fst X Y, f ≫ snd X Y)) ((fun f ↦ lift f.1 f.2) x✝) = x✝

Tactic:
by 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
inst✝ : BraidedCategory C
X Y : C
⊢ (β_ X Y).hom ≫ snd Y X = fst X Y

Tactic:
by
  simp [fst_def, snd_def, ← BraidedCategory.braiding_naturality_right_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
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : CartesianMonoidalCategory D
F : C ⥤ D
A B A' B' : C
f : A ⟶ A'
g : B ⟶ B'
⊢ F.map (f ⊗ₘ g) ≫ prodComparison F A' B' = prodComparison F A B ≫ (F.map f ⊗ₘ F.map g)

Tactic:
by
  apply hom_ext <;>
  simp only [Category.assoc, prodComparison_fst, tensorHom_fst, prodComparison_fst_assoc,
    prodComparison_snd, tensorHom_snd, prodComparison_snd_assoc, ← F.map_comp]

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : CommBialgCat R
a : ↑A
⊢ (ConcreteCategory.hom (𝟙 A)) a = a

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C : CommBialgCat R
f : A ⟶ B
g : B ⟶ C
a : ↑A
⊢ (ConcreteCategory.hom (f ≫ g)) a = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) a)

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B : CommBialgCat R
e : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B : CommBialgCat R
e : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommBialgCat R
X Y Z : Type v
inst✝⁵ : CommRing X
inst✝⁴ : Bialgebra R X
inst✝³ : CommRing Y
inst✝² : Bialgebra R Y
inst✝¹ : CommRing Z
inst✝ : Bialgebra R Z
i : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommBialgCat R
X Y Z : Type v
inst✝⁵ : CommRing X
inst✝⁴ : Bialgebra R X
inst✝³ : CommRing Y
inst✝² : Bialgebra R Y
inst✝¹ : CommRing Z
inst✝ : Bialgebra R Z
i : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom i.hom) ((ConcreteCategory.hom i.inv) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.WithConv

Goal state before:
pp: A : Type u_2
B : Type u_3
f : A ≃ B
x : WithConv B
⊢ (WithConv.congr f).symm x = toConv (f.symm x.ofConv)

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.WithConv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝ : AddMonoid A
⊢ ∀ (x y : WithConv A), (WithConv.equiv A).toFun (x + y) = (WithConv.equiv A).toFun x + (WithConv.equiv A).toFun y

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.WithConv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝² : AddCommMonoid A
inst✝¹ : Semiring R
inst✝ : Module R A
⊢ ∀ (m : R) (x : WithConv A), (WithConv.addEquiv A).toFun (m • x) = (RingHom.id R) m • (WithConv.addEquiv A).toFun x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.WithConv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Semiring R
inst✝² : Module R A
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
f : A ≃ₗ[R] B
x : WithConv B
⊢ (congrLinearEquiv f).symm x = toConv (f.symm x.ofConv)

Tactic:
by simp

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)
⊢ ∀ (j : Discrete PEmpty.{1}), P ((Functor.empty C).obj j)

Tactic:
by simp

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 Y : P.FullSubcategory
⊢ ObjectProperty.homMk (snd X.obj Y.obj) =
    (IsTerminal.ofUniqueHom (fun X ↦ ObjectProperty.homMk (toUnit X.obj)) ⋯).from X ▷ Y ≫ (λ_ Y).hom

Tactic:
by ext; exact snd_def X.1 Y.1

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

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

Tactic:
rw [← whiskerRight_snd (F.map (toUnit X)), δ_natural_left_assoc]
    simp [← OplaxMonoidal.left_unitality_hom, leftUnitor_hom (F.obj Y)]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
X Y Z : C
inst✝ : F.Monoidal
f : X ⟶ Y
g : X ⟶ Z
⊢ (lift (F.map f) (F.map g) ≫ μ F Y Z) ≫ (μIso F Y Z).inv = F.map (lift f g) ≫ (μIso F Y Z).inv

Tactic:
by 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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
⊢ (μIso F X Y).inv ≫ μ F X Y ≫ F.map (fst X Y) = (μIso F X Y).inv ≫ fst (F.obj X) (F.obj Y)

Tactic:
by 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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
⊢ (μIso F X Y).inv ≫ μ F X Y ≫ F.map (snd X Y) = (μIso F X Y).inv ≫ snd (F.obj X) (F.obj Y)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
G X : C
inst✝¹ : GrpObj G
A✝ B A : C
inst✝ : GrpObj A
⊢ ι ≫ ι = 𝟙 A

Tactic:
by 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 : C
inst✝ : GrpObj A
⊢ μ ▷ A ≫ μ = ((α_ A A A).hom ≫ A ◁ μ) ≫ μ

Tactic:
by 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 : C
inst✝ : GrpObj A
s : PullbackCone μ μ
⊢ (lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫ μ ▷ A) ≫
      snd A A =
    s.fst ≫ snd A A

Tactic:
by 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 : C
inst✝ : GrpObj A
s : PullbackCone μ μ
⊢ (lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫
        (α_ A A A).hom ≫ A ◁ μ) ≫
      fst A A =
    s.snd ≫ fst A A

Tactic:
by simp

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✝¹ : Semiring A
inst✝ : HopfAlgebra R A
⊢ MulOpposite.op ((↑(MulOpposite.opLinearEquiv R) ∘ₗ antipode R) 1) = MulOpposite.op 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : HopfAlgebra R A
a b : A
⊢ (antipode R) (a * b) = (antipode R) a * (antipode R) b

Tactic:
antipode_mul_antidistrib,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : HopfAlgebra R A
a b : A
⊢ (antipode R) b * (antipode R) a = (antipode R) a * (antipode R) b
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : HopfAlgebra R A
⊢ ((counitAlgHom R A).comp (antipodeAlgHom R A)).toLinearMap = (counitAlgHom R A).toLinearMap

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A X : C
inst✝ : Closed A
⊢ curry (𝟙 (A ⊗ (𝟭 C).obj X)) = (ihom.coev A).app X

Tactic:
rw [curry_eq, (ihom A).map_id (A ⊗ _)]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A X : C
inst✝ : Closed A
⊢ (ihom.coev A).app ((𝟭 C).obj X) ≫ 𝟙 ((ihom A).obj (A ⊗ (𝟭 C).obj X)) = (ihom.coev A).app X
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
f : W ⟶ X
g : Y ⟶ Z
⊢ (pre f).app Y ≫ (ihom W).map g = (ihom X).map g ≫ (pre f).app Z

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B X✝ X' Y✝ Y' Z : C
inst✝¹ : Closed A
X Y : C
inst✝ : Closed X
x✝ : X ⟶ Y
⊢ uncurry' (curry' x✝) = x✝

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B X✝ X' Y✝ Y' Z : C
inst✝¹ : Closed A
X Y : C
inst✝ : Closed X
x✝ : 𝟙_ C ⟶ (ihom X).obj Y
⊢ curry' (uncurry' x✝) = x✝

Tactic:
by simp

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

Goal state before:
pp: l : List ℕ
m n : ℕ
h : m < n
⊢ List.IsChain (fun x1 x2 ↦ x1 < x2)
    (m ::
      match l, n with
      | [], x => []
      | m :: l, n => (m + n) :: raise' l (m + n + 1))

Tactic:
cases l with grind [isChain_cons_raise']

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
x✝ : IsEmpty α
⊢ #(WType β) ≤ max (lift.{v, u} #α) ℵ₀

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : (a : α) → Fintype (β a)
t : WType β
⊢ 0 < t.depth

Tactic:
cases t

Goal state after:
case mk
α : Type u_1
β : α → Type u_2
inst✝ : (a : α) → Fintype (β a)
a✝ : α
f✝ : β a✝ → WType β
⊢ 0 < (mk a✝ f✝).depth
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
f : ι →₀ R
i : ι
⊢ ∑ x ∈ f.support, (b.toDual (b i)) (f x • b x) = f i

Tactic:
simp_rw [map_smul, toDual_apply, smul_eq_mul, mul_boole, Finset.sum_ite_eq,
    Finsupp.if_mem_support]

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 ι
f : Dual R M
i : ι
⊢ (b.toDual ((Finsupp.linearCombination R ⇑b) (Finsupp.equivFunOnFinite.symm fun i ↦ f (b i)))) (b i) = f (b i)

Tactic:
by 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 ε
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
i j : ι
⊢ (h.basis.dualBasis i) (h.basis j) = (ε i) (h.basis j)

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
⊢ lift.{u, v} (Module.rank R ↥f.range) + lift.{v, u} (Module.rank R ↥f.ker) = lift.{v, u} (Module.rank R M)

Tactic:
by
  have := fun p : Submodule R M => Classical.decEq (M ⧸ p)
  rw [← f.quotKerEquivRange.lift_rank_eq, ← lift_add, rank_quotient_add_rank]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this✝ : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
this : Infinite ιK
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
bK.repr.toEquiv.cardinal_eq,

Goal state after:
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this✝ : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
this : Infinite ιK
⊢ Module.rank K (ι → K) = #(ιK →₀ K)
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : CommHopfAlgCat R
a : ↑A
⊢ (ConcreteCategory.hom (𝟙 A)) a = a

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C : CommHopfAlgCat R
f : A ⟶ B
g : B ⟶ C
a : ↑A
⊢ (ConcreteCategory.hom (f ≫ g)) a = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) a)

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B : CommHopfAlgCat R
e : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B : CommHopfAlgCat R
e : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommHopfAlgCat R
X Y Z : Type v
inst✝⁵ : CommRing X
inst✝⁴ : HopfAlgebra R X
inst✝³ : CommRing Y
inst✝² : HopfAlgebra R Y
inst✝¹ : CommRing Z
inst✝ : HopfAlgebra R Z
i : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) x) = x

Tactic:
by simp

Goal state after: