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

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app X₁ →
        G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app X₂

pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app X₂ →
        G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app X₁

pp: case z
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map ?k₀ ≫ c.ι.app ?X₀

pp: case X₀
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ C

pp: case k₀
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ X ⟶ F.obj ?X₀

Tactic:
· intro Z₁ Z₂ k₁ k₂ g a z
              rw [← a, Functor.map_comp, Category.assoc, ← Functor.comp_map, c.w, z]

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app X₂ →
        G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app X₁

case z
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map ?k₀ ≫ c.ι.app ?X₀

case X₀
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ C

case k₀
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ X ⟶ F.obj ?X₀
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx : f p = 0
this✝ :
  (MvPolynomial.map (algebraMap R A)) p + q ∈
    (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid
this : RingHom.ker f.toRingHom ≤ Ideal.comap (MvPolynomial.map (algebraMap R A)) (Ideal.span s₀)
⊢ (MvPolynomial.map (algebraMap R A)) p ∈ Ideal.span s₀

Tactic:
exact this hx

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

Goal state before:
pp: case of.star
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝ : Discrete J
⊢ PUnit.unit = PUnit.unit

pp: case star.star
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
⊢ PUnit.unit = PUnit.unit

Tactic:
· rfl

Goal state after:
case star.star
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
⊢ PUnit.unit = PUnit.unit
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case star.star
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
⊢ PUnit.unit = PUnit.unit

Tactic:
· rfl

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

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

Tactic:
let hc' := isColimitOfPreserves H ((isColimitExtendCoconeEquiv F c).symm hc)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ D
η : F ⟶ G
X : WithInitial C
⊢ ∀ ⦃Y : WithInitial C⦄ (f : X ⟶ Y),
    ((map F).map f ≫
        match Y with
        | of x => η.app x
        | star => 𝟙 star) =
      (match X with
        | of x => η.app x
        | star => 𝟙 star) ≫
        (map G).map f

Tactic:
Y

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ D
η : F ⟶ G
X Y : WithInitial C
⊢ ∀ (f : X ⟶ Y),
    ((map F).map f ≫
        match Y with
        | of x => η.app x
        | star => 𝟙 star) =
      (match X with
        | of x => η.app x
        | star => 𝟙 star) ≫
        (map G).map f
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ (prelaxfunctor.map₂ (Bicategory.associator f✝ g✝ h✝).hom).toNatTrans.app star =
    ((Cat.Hom.isoMk (mapComp (f✝ ≫ g✝).toFunctor h✝.toFunctor)).hom ≫
            Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f✝.toFunctor g✝.toFunctor)).hom (prelaxfunctor.map h✝) ≫
              (Bicategory.associator (prelaxfunctor.map f✝) (prelaxfunctor.map g✝) (prelaxfunctor.map h✝)).hom ≫
                Bicategory.whiskerLeft (prelaxfunctor.map f✝) (Cat.Hom.isoMk (mapComp g✝.toFunctor h✝.toFunctor)).inv ≫
                  (Cat.Hom.isoMk (mapComp f✝.toFunctor (g✝ ≫ h✝).toFunctor)).inv).toNatTrans.app
      star

Tactic:
· rfl

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

Goal state before:
pp: case refine_1
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)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ (s.fst ≫ pullback.snd f g) ≫ g = (s.snd ≫ pullback.snd f g) ≫ g

Tactic:
simp_rw [Category.assoc, ← pullback.condition, ← Category.assoc, s.condition]

Goal state after:
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₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ (pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂ =
    pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂)

Tactic:
by
  trans l₁' ≫ pullback.fst _ _
  · rw [← Category.assoc]
    congr 1
    exact IsLimit.conePointUniqueUpToIso_inv_comp _ _ WalkingCospan.left
  · exact pullback.lift_fst _ _ _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P f → P.pushouts f

Tactic:
Y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
⊢ ∀ (f : X ⟶ Y), P f → P.pushouts f
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), isomorphisms C f → P.pushouts f

Tactic:
Y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
⊢ ∀ (f : X ⟶ Y), isomorphisms C f → P.pushouts f
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X : CommRingCat
⊢ ∀ {Y Z : CommRingCat} (e : X ≅ Y) (f : Y ⟶ Z),
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.hom ≫ f)

Tactic:
Y

Goal state after:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y : CommRingCat
⊢ ∀ {Z : CommRingCat} (e : X ≅ Y) (f : Y ⟶ Z),
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.hom ≫ f)
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X : CommRingCat
⊢ ∀ {Y Z : CommRingCat} (e : Y ≅ Z) (f : X ⟶ Y),
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)

Tactic:
Y

Goal state after:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y : CommRingCat
⊢ ∀ {Z : CommRingCat} (e : Y ≅ Z) (f : X ⟶ Y),
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X : Type u
⊢ ∀ {S T : Type u} [inst : CommRing X] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : X →+* S) (e : S ≃+* T),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)

Tactic:
Y

Goal state after:
case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y : Type u
⊢ ∀ {T : Type u} [inst : CommRing X] [inst_1 : CommRing Y] [inst_2 : CommRing T] (f : X →+* Y) (e : Y ≃+* T),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_4
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X : Type u
⊢ ∀ {S T : Type u} [inst : CommRing X] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : S →+* T) (e : X ≃+* S),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)

Tactic:
Y

Goal state after:
case refine_4
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y : Type u
⊢ ∀ {T : Type u} [inst : CommRing X] [inst_1 : CommRing Y] [inst_2 : CommRing T] (f : Y →+* T) (e : X ≃+* Y),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp e.toRingHom)
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

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✝ : P.IsClosedUnderIsomorphisms
h : P.strictLimitsOfShape J ≤ P
⊢ P.limitsOfShape J ≤ P

Tactic:
by
    conv_rhs => rw [← P.isoClosure_eq_self]
    rw [← isoClosure_strictLimitsOfShape]
    exact monotone_isoClosure h

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} W
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), coproducts.{w, v, u} W f → W f

Tactic:
Y

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} W
X Y : C
⊢ ∀ (f : X ⟶ Y), coproducts.{w, v, u} W f → W f
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X : C
⊢ ∀ {Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P.universally f → P.universally (e.hom ≫ f)

Tactic:
Y

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
⊢ ∀ {Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P.universally f → P.universally (e.hom ≫ f)
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
⊢ P.op.limitsOfShape J = P.op.limitsOfShape Jᵒᵖᵒᵖ

Tactic:
P.op.limitsOfShape_congr (opOpEquivalence J)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.op.limitsOfShape J = P.op.limitsOfShape J
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X : C
⊢ ∀ {Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P.universally f → P.universally (f ≫ e.hom)

Tactic:
Y

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
⊢ ∀ {Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P.universally f → P.universally (f ≫ e.hom)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P.universally f → P f

Tactic:
Y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
⊢ ∀ (f : X ⟶ Y), P.universally f → P f
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : SemiCartesianMonoidalCategory D
M : D
inst✝ : MonObj M
⊢ μ ≫ η = (η ⊗ₘ η) ≫ μ

Tactic:
by simp [toUnit_unique (ρ_ (𝟙_ D)).hom (λ_ (𝟙_ D)).hom]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Bialgebra R A
⊢ (ofHom (comulAlgHom R A)).op ▷ op (of R A) ≫ (ofHom (comulAlgHom R A)).op =
    (α_ (op (of R A)) (op (of R A)) (op (of R A))).hom ≫
      op (of R A) ◁ (ofHom (comulAlgHom R A)).op ≫ (ofHom (comulAlgHom R A)).op

Tactic:
by ext; exact (Coalgebra.coassoc_symm_apply _).symm

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

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_4
C : Type u_5
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
D : Type u_7
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R B
inst✝⁴ : CoalgebraStruct R B
inst✝³ : NonUnitalNonAssocSemiring D
inst✝² : Module R D
inst✝¹ : SMulCommClass R D D
inst✝ : IsScalarTower R D D
f h : WithConv (C →ₗ[R] A)
g k : WithConv (B →ₗ[R] D)
⊢ toConv (mul' R (A ⊗[R] D) ∘ₗ ((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ (h.ofConv ⊗ₘ k.ofConv)) ∘ₗ δ) =
    toConv (mul' R A ∘ₗ (f.ofConv ⊗ₘ h.ofConv) ∘ₗ δ ⊗ₘ mul' R D ∘ₗ (g.ofConv ⊗ₘ k.ofConv) ∘ₗ δ)

Tactic:
comul_def,

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_4
C : Type u_5
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
D : Type u_7
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R B
inst✝⁴ : CoalgebraStruct R B
inst✝³ : NonUnitalNonAssocSemiring D
inst✝² : Module R D
inst✝¹ : SMulCommClass R D D
inst✝ : IsScalarTower R D D
f h : WithConv (C →ₗ[R] A)
g k : WithConv (B →ₗ[R] D)
⊢ toConv
      (mul' R (A ⊗[R] D) ∘ₗ
        ((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ (h.ofConv ⊗ₘ k.ofConv)) ∘ₗ
          ↑(AlgebraTensorModule.tensorTensorTensorComm R R R R C C B B) ∘ₗ AlgebraTensorModule.map δ δ) =
    toConv (mul' R A ∘ₗ (f.ofConv ⊗ₘ h.ofConv) ∘ₗ δ ⊗ₘ mul' R D ∘ₗ (g.ofConv ⊗ₘ k.ofConv) ∘ₗ δ)
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
repr : Coalgebra.Repr R a ι
⊢ ∑ i ∈ repr.index, repr.left i * (antipode R) (repr.right i) = counit a • 1

Tactic:
sum_mul_antipode_eq_algebraMap_counit,

Goal state after:
R : Type u
A : Type v
ι : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
repr : Coalgebra.Repr R a ι
⊢ (algebraMap R A) (counit a) = counit a • 1
Module: Mathlib.CategoryTheory.Adjunction.Parametrized

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj : (X₁ : C₁) → F.obj X₁ ⊣ G.obj (op X₁)
h :
  ∀ {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) {X₂ : C₂} {X₃ : C₃} (g : (F.obj Y₁).obj X₂ ⟶ X₃),
    ((adj X₁).homEquiv X₂ X₃) ((F.map f).app X₂ ≫ g) = ((adj Y₁).homEquiv X₂ X₃) g ≫ (G.map f.op).app X₃
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
⊢ (adj X₁).unit ≫ whiskerRight (F.map f) (G.obj (op X₁)) = (adj Y₁).unit ≫ (F.obj Y₁).whiskerLeft (G.map f.op)

Tactic:
ext X₂

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj : (X₁ : C₁) → F.obj X₁ ⊣ G.obj (op X₁)
h :
  ∀ {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) {X₂ : C₂} {X₃ : C₃} (g : (F.obj Y₁).obj X₂ ⟶ X₃),
    ((adj X₁).homEquiv X₂ X₃) ((F.map f).app X₂ ≫ g) = ((adj Y₁).homEquiv X₂ X₃) g ≫ (G.map f.op).app X₃
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
⊢ ((adj X₁).unit ≫ whiskerRight (F.map f) (G.obj (op X₁))).app X₂ =
    ((adj Y₁).unit ≫ (F.obj Y₁).whiskerLeft (G.map f.op)).app X₂
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 H : Grp C
⊢ homMk' (fst G.toMon H.toMon) = G ◁ (IsTerminal.ofUniqueHom (fun G ↦ homMk' (toUnit G.toMon)) ⋯).from H ≫ (ρ_ G).hom

Tactic:
by ext; apply fst_def

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 Y : C
inst✝¹ : Closed A
inst✝ : Closed B
f : Y ⟶ (ihom A).obj X
g : B ⟶ A
⊢ f ≫ (pre g).app X = curry (uncurry f) ≫ (pre g).app X

Tactic:
curry_uncurry

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B X Y : C
inst✝¹ : Closed A
inst✝ : Closed B
f : Y ⟶ (ihom A).obj X
g : B ⟶ A
⊢ f ≫ (pre g).app X = f ≫ (pre g).app X
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case e'_4.inl
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #↑s < ℵ₀
⊢ max #↑s ℵ₀ = max (lift.{u, 0} #(Fin 6) + #↑s) ℵ₀

Tactic:
rw [max_eq_right h.le, max_eq_right]
        exact (add_lt_aleph0 this h).le

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
i : ι
⊢ b.toDual (b i) = b.coord i

Tactic:
ext
  apply toDual_apply_right

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

Goal state before:
pp: case e_a.refine_1
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
⊢ ⊥ ⊓ (-ce).ker = ⊥

Tactic:
bot_inf_eq

Goal state after:
case e_a.refine_1
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
⊢ ⊥ = ⊥
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:

Tactic:
_ = Y ◁ η_ X' Y ≫ Y ◁ (i.inv ≫ i.hom) ▷ Y ⊗≫ ε_ X' Y ▷ Y := by
        monoidal
      _ = Y ◁ η_ X' Y ⊗≫ ε_ X' Y ▷ Y := by
        rw [Iso.inv_hom_id]; monoidal
      _ = _ := by
        rw [coevaluation_evaluation'']
        simp

Goal state after: