mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Quiver.IsThin C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : Quiver.IsThin D
F : C ⥤ D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
hfg : HasPullback f g
⊢ Nonempty (IsLimit (BinaryFan.mk (pullback.fst f g) (pullback.snd f g)))

Tactic:
← CategoryTheory.isPullback_iff_isLimit_binaryFan_of_isThin (f := f) (g := g)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Quiver.IsThin C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : Quiver.IsThin D
F : C ⥤ D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
hfg : HasPullback f g
⊢ IsPullback (pullback.fst f g) (pullback.snd f g) f g
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
⊢ T.η.app (F.obj X) ≫ T.map (i.inv.app X) ≫ T.μ.app X ≫ i.hom.app X = 𝟙 (F.obj X)

Tactic:
slice_lhs 1 2 => rw [← T.η.naturality (i.inv.app X), ]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
⊢ (((𝟭 C).map (i.inv.app X) ≫ T.η.app (T.obj X)) ≫ T.μ.app X) ≫ i.hom.app X = 𝟙 (F.obj X)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ l (mk m 1) = l (↑s • mk m s)

Tactic:
LocalizedModule.smul'_mk

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ l (mk m 1) = l (mk (↑s • m) s)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ fromLocalizedModule' S f (LocalizedModule.mk a b + LocalizedModule.mk a' b') =
    fromLocalizedModule' S f (LocalizedModule.mk a b) + fromLocalizedModule' S f (LocalizedModule.mk a' b')

Tactic:
simp only [LocalizedModule.mk_add_mk, fromLocalizedModule'_mk]

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (f (b' • a + b • a')) = ↑⋯.unit⁻¹ (f a) + ↑⋯.unit⁻¹ (f a')
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M''
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
x : M
⊢ (linearEquiv S f g) (f x) = g x

Tactic:
by
  simp [linearEquiv]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M''
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
x : M
⊢ (linearEquiv S f g).symm (g x) = f x

Tactic:
by
  simp [linearEquiv]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s₁ s₂ : ↥S
⊢ mk' f (s₂ • m) (s₁ * s₂) = mk' f m s₁

Tactic:
by
  delta mk'
  rw [LocalizedModule.mk_cancel_common_right]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
j : WalkingPair
⊢ (A.coproductCocone B).ι.app { as := j } ≫
      ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom =
    s.ι.app { as := j }

Tactic:
cases j

Goal state after:
case left
A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
⊢ (A.coproductCocone B).ι.app { as := WalkingPair.left } ≫
      ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom =
    s.ι.app { as := WalkingPair.left }

case right
A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
⊢ (A.coproductCocone B).ι.app { as := WalkingPair.right } ≫
      ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom =
    s.ι.app { as := WalkingPair.right }
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPair ⥤ CommRingCat
⊢ IsLocalHom (Hom.hom (limit.π F zero))

Tactic:
refine Limits.π_isLocalHom _ (limit.isLimit _) zero fun x hx i ↦ ?_

Goal state after:
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPair ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
i : WalkingParallelPair
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app i)) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁵ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝¹⁴ : AddCommMonoid M₀
inst✝¹³ : AddCommMonoid M₀'
inst✝¹² : Module R M₀
inst✝¹¹ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝¹⁰ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_11
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₁'
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝⁵ : IsLocalizedModule S f₁
M₂ : Type u_8
M₂' : Type u_10
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₂'
inst✝² : Module R M₂
inst✝¹ : Module R M₂'
f₂ : M₂ →ₗ[R] M₂'
inst✝ : IsLocalizedModule S f₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
⊢ (map S f₀ f₂) (h ∘ₗ g) = (map S f₁ f₂) h ∘ₗ (map S f₀ f₁) g

Tactic:
ext x
  obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f₀ x
  simp

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: case h
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ∀ b ∈ Finset.range (n + m + 1), J ^ b * K ^ (n + m - b) * ↑((n + m).choose b) ≤ I

Tactic:
refine fun i _ => mul_le_left.trans ?_

Goal state after:
case h
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
⊢ J ^ i * K ^ (n + m - i) ≤ I
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C✝ : Type u_1
inst✝¹ : Category.{v_1, u_1} C✝
C : Type u_1
inst✝ : Category.{v_1, u_1} C
hC : LocallySmall.{w, v_1, u_1} C
⊢ EssentiallySmall.{w, v_1, u_1} C ↔ ∃ J x, Nonempty (C ≌ J)

Tactic:
refine ⟨fun H ↦ H.1, fun H ↦ ⟨H⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G : D ≌ C
⊢ ∀ (X : Grothendieck (G.functor ⋙ F)),
    (pre F G.functor).map
          ((eqToIso ⋯ ≪≫
                  (map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).isoWhiskerLeft
                      (Grothendieck.preUnitIso F G) ≪≫
                    eqToIso ⋯).hom.app
            X) ≫
        (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X) =
      𝟙 ((pre F G.functor).obj X)

Tactic:
intro X
    simp only [preInv, Grothendieck.preUnitIso, pre_id,
      Iso.trans_hom, eqToIso.hom, eqToHom_app, eqToHom_refl, isoWhiskerLeft_hom, NatTrans.comp_app]
    fapply Grothendieck.ext <;> simp [preNatIso, transportIso]

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

Goal state before:
pp: case h
J : Type v₁
p : Set (WidePullbackShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : WidePullbackShape J
⊢ j ∈ p

Tactic:
cases j

Goal state after:
case h.none
J : Type v₁
p : Set (WidePullbackShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ none ∈ p

case h.some
J : Type v₁
p : Set (WidePullbackShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
val✝ : J
⊢ some val✝ ∈ p
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: case h
J : Type v₁
p : Set (WidePushoutShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : WidePushoutShape J
⊢ j ∈ p

Tactic:
cases j

Goal state after:
case h.none
J : Type v₁
p : Set (WidePushoutShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ none ∈ p

case h.some
J : Type v₁
p : Set (WidePushoutShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
val✝ : J
⊢ some val✝ ∈ p
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: case h
p : Set WalkingParallelPair
a✝ : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : WalkingParallelPair
⊢ j ∈ p

Tactic:
cases j

Goal state after:
case h.zero
p : Set WalkingParallelPair
a✝ : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ WalkingParallelPair.zero ∈ p

case h.one
p : Set WalkingParallelPair
a✝ : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ WalkingParallelPair.one ∈ p
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }

Tactic:
let y₁ := colimit.ι (F ⋙ coyoneda.obj (op d)) X₁ f₁

Goal state after:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : (fun X ↦ X) (colimit (F ⋙ coyoneda.obj (op d))) :=
  (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) X₁)) f₁
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
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 : C
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsColimit (Cofork.ofπ f.op ⋯)
⊢ IsLimit (ofι f ⋯)

Tactic:
by
    refine Fork.isLimitOfIsos _ (Cofork.isColimitOfπEquivIsLimitUnop f.op f.op
      pullback.condition (by simp only [← unop_comp, pullback.condition]) rfl h) _ (.refl _)
        ((pushoutIsoUnopPullback f f).symm) (.refl _) ?_ ?_ (by simp)
    · rw [Iso.symm_hom, ← Quiver.Hom.unop_op (pushoutIsoUnopPullback f f).inv, ← unop_comp,
        pushoutIsoUnopPullback_inv_fst, Quiver.Hom.unop_op, Iso.refl_hom, Category.id_comp]
    · rw [Iso.symm_hom, ← Quiver.Hom.unop_op (pushoutIsoUnopPullback f f).inv, ← unop_comp,
        pushoutIsoUnopPullback_inv_snd, Quiver.Hom.unop_op, Iso.refl_hom, Category.id_comp]

Goal state after:
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)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
⊢ { l // l ≫ (Fork.ofι g ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = l }

Tactic:
have l₁ : (Fork.ι s ≫ k) ≫ hr.left = (Fork.ι s ≫ k) ≫ hr.right := by
      rw [Category.assoc, s.condition, Category.assoc]

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)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
⊢ { l // l ≫ (Fork.ofι g ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = l }
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt
hm : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j
⊢ ∀ (j : WalkingCospan),
    m ≫ (IsPullback.cone small_k).π.app j = small_k.lift s.fst s.snd ⋯ ≫ (IsPullback.cone small_k).π.app j

Tactic:
apply PullbackCone.equalizer_ext small_k.cone _ _

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt
hm : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j
⊢ m ≫ (IsPullback.cone small_k).fst = small_k.lift s.fst s.snd ⋯ ≫ (IsPullback.cone small_k).fst

C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt
hm : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j
⊢ m ≫ (IsPullback.cone small_k).snd = small_k.lift s.fst s.snd ⋯ ≫ (IsPullback.cone small_k).snd
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
⊢ pullback.fst f (a₁ ≫ g) ≫ 𝟙 X = pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯ ≫ pullback.fst f g

Tactic:
pullback.lift_fst

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
⊢ pullback.fst f (a₁ ≫ g) ≫ 𝟙 X = pullback.fst f (a₁ ≫ g) ≫ 𝟙 X
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
⊢ snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i =
    snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯ ≫ fst f f

Tactic:
pullback.lift_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
⊢ snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i =
    snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i
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
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).hom ≫ fst f g =
    snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i)

Tactic:
delta pullbackDiagonalMapIdIso

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (asIso
            (map (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) (diagonal i)
              (map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
                ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯)
              (𝟙 T) (congrHom ⋯ ⋯).hom (𝟙 (diagonalObj i)) ⋯ ⋯) ≪≫
          pullbackDiagonalMapIso i (𝟙 S) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) ≪≫
            asIso (map (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) f g (𝟙 X) (𝟙 Y) (fst i (𝟙 S)) ⋯ ⋯)).hom ≫
      fst f g =
    snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i)
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
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).hom ≫ snd f g =
    snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd (f ≫ i) (g ≫ i)

Tactic:
delta pullbackDiagonalMapIdIso

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (asIso
            (map (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) (diagonal i)
              (map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
                ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯)
              (𝟙 T) (congrHom ⋯ ⋯).hom (𝟙 (diagonalObj i)) ⋯ ⋯) ≪≫
          pullbackDiagonalMapIso i (𝟙 S) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) ≪≫
            asIso (map (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) f g (𝟙 X) (𝟙 Y) (fst i (𝟙 S)) ⋯ ⋯)).hom ≫
      snd f g =
    snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd (f ≫ i) (g ≫ i)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
⊢ W.IsStableUnderLimitsOfShape J → W.limitsOfShape J ≤ W

Tactic:
rintro h _ _ _ ⟨_, _, _, _, h₁, h₂, f, hf⟩

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.IsStableUnderLimitsOfShape J
X Y : C
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cone X₁✝
c₂✝ : Cone X₂✝
h₁ : IsLimit c₁✝
h₂ : IsLimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W.functorCategory J f
⊢ W (h₂.lift { pt := c₁✝.pt, π := c₁✝.π ≫ f })
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

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
J : Type u'
inst✝¹ : Category.{v', u'} J
P : ObjectProperty D
inst✝ : P.IsClosedUnderIsomorphisms
e : C ≌ D
⊢ (P.inverseImage e.functor).IsClosedUnderLimitsOfShape J ↔ P.IsClosedUnderLimitsOfShape J

Tactic:
by
  refine ⟨fun H ↦ ?_, fun _ ↦ inferInstance⟩
  convert!
    (inferInstance :
      ((P.inverseImage e.functor).inverseImage e.inverse).IsClosedUnderLimitsOfShape J)
  ext X
  simpa using P.prop_iff_of_iso (e.counitIso.app X).symm

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

Tactic:
pullback.lift_fst

Goal state after:
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₃
⊢ map f g f' g' i₁ i₂ i₃ e₁ e₂ = map f g f' g' i₁ i₂ i₃ e₁ e₂
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
⊢ W.IsStableUnderColimitsOfShape J → W.colimitsOfShape J ≤ W

Tactic:
rintro h _ _ _ ⟨_, _, _, _, h₁, h₂, f, hf⟩

Goal state after:
case mp
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
⊢ W (h₁.desc { pt := c₂✝.pt, ι := f ≫ c₂✝.ι })
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 ≫ fst Y X = snd X Y

Tactic:
by
  simp [fst_def, snd_def, ← BraidedCategory.braiding_naturality_left_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 g h : WithConv (C →ₗ[R] A)
x✝ : C
⊢ ((f + g) * h).ofConv x✝ = (f * h + g * h).ofConv x✝

Tactic:
simp [map_add_left]

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 (snd X Y)

Tactic:
trans F.map (toUnit X ▷ Y) ≫ F.map (λ_ Y).hom

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 ≫ snd (F.obj X) (F.obj Y) = F.map (toUnit X ▷ Y) ≫ F.map (λ_ Y).hom

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.map (toUnit X ▷ Y) ≫ F.map (λ_ Y).hom = F.map (snd X Y)