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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ (g ≫ k) ≫ hr.left = g ≫ k ≫ hr.right

Tactic:
← eq_whisker comm

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ (f ≫ h) ≫ hr.left = g ≫ k ≫ hr.right
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ (f ≫ h) ≫ hr.left = (g ≫ k) ≫ hr.right

Tactic:
← eq_whisker comm

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ (f ≫ h) ≫ hr.left = (f ≫ h) ≫ hr.right
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝² : HasPullback f₁ f₂
inst✝¹ : HasPullback f₃ f₄
inst✝ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
⊢ IsLimit
    (PullbackCone.mk (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      ⋯)

Tactic:
simpa using! pasteVertIsPullback rfl (pullbackIsPullback _ _)
    (pullbackPullbackLeftIsPullback f₁ f₂ f₃ f₄)

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

Goal state before:
pp: case pos
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : P d
this : Nonempty (CostructuredArrow P.ι d)
⊢ IsConnected (CostructuredArrow P.ι d)

Tactic:
refine zigzag_isConnected (fun j₁ j₂ ↦ Zigzag.trans
      (j₂ := by exact CostructuredArrow.mk (Y := ⟨d, hd⟩) (𝟙 _)) (.of_hom ?_) (.of_inv ?_))

Goal state after:
case pos.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : P d
this : Nonempty (CostructuredArrow P.ι d)
j₁ j₂ : CostructuredArrow P.ι d
⊢ j₁ ⟶ CostructuredArrow.mk (𝟙 (P.ι.obj { obj := d, property := hd }))

case pos.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : P d
this : Nonempty (CostructuredArrow P.ι d)
j₁ j₂ : CostructuredArrow P.ι d
⊢ j₂ ⟶ CostructuredArrow.mk (𝟙 (P.ι.obj { obj := d, property := hd }))
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
⊢ (g ≫ (PushoutCocone.mk h k comm).inr) ≫ m = g ≫ (PushoutCocone.mk h k comm).inr ≫ p

Tactic:
← eq_whisker comm

Goal state after:
case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
⊢ (f ≫ h) ≫ m = g ≫ (PushoutCocone.mk h k comm).inr ≫ p
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
⊢ (f ≫ h) ≫ m = (g ≫ (PushoutCocone.mk h k comm).inr) ≫ p

Tactic:
← eq_whisker comm

Goal state after:
case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
⊢ (f ≫ h) ≫ m = (f ≫ h) ≫ p
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

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

Tactic:
← Category.comp_id (pullback.fst _ _)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
| fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
n : ℕ
K : Discrete (Fin n) ⥤ C
⊢ HasLimit K

Tactic:
let that : (Discrete.functor fun n => K.obj ⟨n⟩) ≅ K := Discrete.natIso fun ⟨_⟩ => Iso.refl _

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryProducts C
inst✝ : HasTerminal C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : (Discrete.functor fun n_1 ↦ K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x ↦
    match x with
    | { as := as } => Iso.refl ((Discrete.functor fun n_1 ↦ K.obj { as := n_1 }).obj { as := as })
⊢ HasLimit K
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : Nonempty J
⊢ ⊥.strictLimitsOfShape J ≤ ⊥

Tactic:
rintro _ ⟨_, h⟩

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : Nonempty J
F✝ : J ⥤ C
inst✝ : HasLimit F✝
h : ∀ (j : J), ⊥ (F✝.obj j)
⊢ ⊥ (limit F✝)
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✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), α ≫ c₂.π.app j = c₁.π.app j ≫ f.app j
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j ↦ f.app { as := j }
this : HasLimit X₁
⊢ W α

Tactic:
have : HasLimit X₂ := ⟨c₂, hc₂⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), α ≫ c₂.π.app j = c₁.π.app j ≫ f.app j
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j ↦ f.app { as := j }
this✝ : HasLimit X₁
this : HasLimit X₂
⊢ W α
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : Nonempty J
⊢ ⊥.strictColimitsOfShape J ≤ ⊥

Tactic:
rintro _ ⟨_, h⟩

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : Nonempty J
F✝ : J ⥤ C
inst✝ : HasColimit F✝
h : ∀ (j : J), ⊥ (F✝.obj j)
⊢ ⊥ (colimit F✝)
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
⊢ X ◁ α.homEquiv'.symm 1 ≫ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) = (ρ_ X).hom

Tactic:
by
    apply α.homEquiv'.injective
    simp only [α.homEquiv'_comp, Equiv.apply_symm_apply, map_mul]
    simp only [← α.homEquiv'_comp]
    simp only [whiskerLeft_fst, whiskerLeft_snd, α.homEquiv'_comp, Equiv.apply_symm_apply]
    simp [rightUnitor_hom, -op_tensorObj, -op_whiskerRight, -op_tensorUnit]

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
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ (ConcreteCategory.hom (α.app (op (𝟙_ C)))) (toUnit (𝟙_ C) ≫ η) = η

Tactic:
← Category.id_comp η[N.X],

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
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ (ConcreteCategory.hom (α.app (op (𝟙_ C)))) (toUnit (𝟙_ C) ≫ η) = 𝟙 (𝟙_ C) ≫ η
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
M N : Mon C
α : yonedaMon.obj M ⟶ yonedaMon.obj N
⊢ μ ≫ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ μ

Tactic:
by
        dsimp only [yonedaMon_obj] at α ⊢
        rw [← yonedaMon_naturality, Category.comp_id, ← Category.id_comp μ[M.X], ← lift_fst_snd]
        refine ((α.app _).hom.map_mul _ _).trans ?_
        change lift _ _ ≫ μ[N.X] = _
        congr 1
        ext <;> simp only [lift_fst, tensorHom_fst, lift_snd, tensorHom_snd,
          ← yonedaMon_naturality, Category.comp_id]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D T✝ : CommAlgCat R
f : A ⟶ T✝
g : B ⟶ T✝
m : (A.binaryCofan B).pt ⟶ T✝
hm₁ : (A.binaryCofan B).inl ≫ m = f
hm₂ : (A.binaryCofan B).inr ≫ m = g
⊢ Hom.hom m = Hom.hom (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯))

Tactic:
refine liftEquiv.symm_apply_eq (y := ⟨⟨_, _⟩, fun _ _ ↦ .all _ _⟩).mp ?_

Goal state after:
R : Type u
inst✝ : CommRing R
A B C D T✝ : CommAlgCat R
f : A ⟶ T✝
g : B ⟶ T✝
m : (A.binaryCofan B).pt ⟶ T✝
hm₁ : (A.binaryCofan B).inl ≫ m = f
hm₂ : (A.binaryCofan B).inr ≫ m = g
⊢ Algebra.TensorProduct.liftEquiv.symm (Hom.hom m) = ⟨(ConcreteCategory.hom f, ConcreteCategory.hom g), ⋯⟩
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 ≫ fst (F.obj X) (F.obj Y) = F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom

Tactic:
← whiskerLeft_fst _ (F.map (toUnit Y)),

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.OplaxMonoidal
X Y : C
⊢ δ F X Y ≫ F.obj X ◁ F.map (toUnit Y) ≫ fst (F.obj X) (F.obj (𝟙_ C)) = F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom
Module: Mathlib.RingTheory.Bialgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Semiring C
inst✝² : Bialgebra R C
inst✝¹ : Algebra R A
inst✝ : Algebra R B
h : A →ₐ[R] B
f g : WithConv (C →ₐ[R] A)
⊢ (h.comp (f * g).ofConv).toLinearMap = (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv.toLinearMap

Tactic:
apply WithConv.toConv_injective

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Semiring C
inst✝² : Bialgebra R C
inst✝¹ : Algebra R A
inst✝ : Algebra R B
h : A →ₐ[R] B
f g : WithConv (C →ₐ[R] A)
⊢ toConv (h.comp (f * g).ofConv).toLinearMap =
    toConv (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv.toLinearMap
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
⊢ lift (ι ≫ ι) ι ≫ μ = lift (𝟙 A) ι ≫ μ

Tactic:
rw [right_inv, ← comp_toUnit_assoc ι, ← left_inv, comp_lift_assoc, Category.comp_id]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
⊢ antipode R ∘ₗ LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A) = LinearMap.mul' R A ∘ₗ (antipode R ⊗ₘ antipode R)

Tactic:
apply WithConv.toConv_injective

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
⊢ toConv (antipode R ∘ₗ LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) =
    toConv (LinearMap.mul' R A ∘ₗ (antipode R ⊗ₘ antipode R))
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
⊢ toConv (antipode R) * toConv id = 1

Tactic:
ext c; rw [(ℛ R c).convMul_apply]; simp [sum_antipode_mul_eq_algebraMap_counit (ℛ R c)]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
h₁ h₂ : GrpObj X
e : h₁.toMonObj = h₂.toMonObj
⊢ ι = ι

Tactic:
apply lift_left_mul_ext (𝟙 _)

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
h₁ h₂ : GrpObj X
e : h₁.toMonObj = h₂.toMonObj
⊢ lift ι (𝟙 X) ≫ μ = lift ι (𝟙 X) ≫ μ
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
⊢ (toConv (antipodeAlgHom R A) * toConv (AlgHom.id R A)).ofConv.toLinearMap = (ofConv 1).toLinearMap

Tactic:
apply WithConv.toConv_injective

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : HopfAlgebra R A
⊢ toConv (toConv (antipodeAlgHom R A) * toConv (AlgHom.id R A)).ofConv.toLinearMap = toConv (ofConv 1).toLinearMap
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M : ModuleCat R
⊢ ∀ {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:
by
                intros
                ext : 1
                apply TensorProduct.ext'
                intro m n
                rfl

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

Goal state before:
pp: case intro
R : Type uR
M : Type uM
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ b.dualBasis.toDual.range = ⊤

Tactic:
toDual_range _

Goal state after:
case intro
R : Type uR
M : Type uM
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ ⊤ = ⊤
Module: Mathlib.LinearAlgebra.Dual.Basis

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

Tactic:
by
  simp [-toDualEquiv_apply, Basis.dualBasis]

Goal state after:
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
N : Submodule R M
h : Module.rank R ↥N < 0 + Module.rank R ↥N
e : Module.rank R (M ⧸ N) = 0
⊢ False

Tactic:
zero_add

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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R ↥N
e : Module.rank R (M ⧸ N) = 0
⊢ False
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: R : Type u
S : Type u'
M : Type v
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : StrongRankCondition R
inst✝² : StrongRankCondition S
inst✝¹ : Module R S
inst✝ : SMulCommClass R S S
⊢ Module.rank S (M →ₗ[R] S) = lift.{u', v} (Module.rank R M)

Tactic:
by
  rw [rank_linearMap, rank_self, lift_one, mul_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : Dual R M
n : N
g : Dual R N
p : P
m : M
⊢ f m • g n • p = g n • f m • p

Tactic:
smul_comm

Goal state after:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : Dual R M
n : N
g : Dual R N
p : P
m : M
⊢ g n • f m • p = g n • f m • p
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type uK
V : Type uV
inst✝³ : CommSemiring K
inst✝² : AddCommMonoid V
inst✝¹ : Module K V
inst✝ : Free K V
h : Module.Finite K (Dual K V)
ι : Type uV
b : Basis ι K V
h✝ : Infinite ι
a✝ : Nontrivial K
⊢ Module.Finite K V

Tactic:
have ⟨n, hn⟩ := Module.Finite.exists_nat_not_surjective K (Dual K V)

Goal state after:
K : Type uK
V : Type uV
inst✝³ : CommSemiring K
inst✝² : AddCommMonoid V
inst✝¹ : Module K V
inst✝ : Free K V
h : Module.Finite K (Dual K V)
ι : Type uV
b : Basis ι K V
h✝ : Infinite ι
a✝ : Nontrivial K
n : ℕ
hn : ∀ (f : Dual K V →ₗ[K] Fin n → K), ¬Function.Surjective ⇑f
⊢ Module.Finite K V
Module: Mathlib.Algebra.Category.FGModuleCat.Colimits

Goal state before:
pp: J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
k : Type u
inst✝ : Ring k
F : J ⥤ FGModuleCat k
⊢ ModuleCat.isFG k (colimit (F ⋙ forget₂ (FGModuleCat k) (ModuleCat k)))

Tactic:
by rw [ModuleCat.isFG_iff]; infer_instance

Goal state after:
Module: Mathlib.Algebra.Category.FGModuleCat.Limits

Goal state before:
pp: J : Type
inst✝³ : SmallCategory J
inst✝² : FinCategory J
k : Type u
inst✝¹ : Ring k
inst✝ : IsNoetherianRing k
F : J ⥤ FGModuleCat k
⊢ ModuleCat.isFG k (limit (F ⋙ forget₂ (FGModuleCat k) (ModuleCat k)))

Tactic:
by rw [ModuleCat.isFG_iff]; infer_instance

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

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

Tactic:
simp [hb']

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| 0

Tactic:
show 0 = a ≫ (0 : Y ⟶ Y) by simp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| a ≫ 0
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
          rw [← y.2.choose_spec, leftCoset_assoc]
          let b' : B := y.2.choose
          use b * b'

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
s : PushoutCocone f g
hs : IsColimit s
⊢ Mono s.inr

Tactic:
by
  have : Mono (NatTrans.app (colimit.cocone (span f g)).ι WalkingCospan.right) :=
    Abelian.mono_pushout_of_mono_f f g
  apply
    mono_of_mono_fac (IsColimit.comp_coconePointUniqueUpToIso_hom hs (colimit.isColimit _) _)

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₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ QuasiIso φ

Tactic:
by
  rw [((LeftHomologyMapData.ofEpiOfIsIsoOfMono φ) S₁.leftHomologyData).quasiIso_iff]
  dsimp
  infer_instance

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 S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
⊢ h₁.f' ≫ φK ≫ h₂.π = 0

Tactic:
by rw [reassoc_of% commf', h₂.f'_π, comp_zero]

Goal state after: