mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

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

Tactic:
ext X

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
X : ↑(Cat.of (WithTerminal ↑a✝))
⊢ (NatTrans.toCatHom₂ (map₂ (f✝.toFunctor.associator g✝.toFunctor h✝.toFunctor).hom)).toNatTrans.app X =
    (NatTrans.toCatHom₂ (mapComp (f✝.toFunctor ⋙ g✝.toFunctor) h✝.toFunctor).hom ≫
            Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f✝.toFunctor g✝.toFunctor).hom)
                (map h✝.toFunctor).toCatHom ≫
              (Bicategory.associator (map f✝.toFunctor).toCatHom (map g✝.toFunctor).toCatHom
                    (map h✝.toFunctor).toCatHom).hom ≫
                Bicategory.whiskerLeft (map f✝.toFunctor).toCatHom
                    (NatTrans.toCatHom₂ (mapComp g✝.toFunctor h✝.toFunctor).inv) ≫
                  NatTrans.toCatHom₂ (mapComp f✝.toFunctor (g✝.toFunctor ⋙ h✝.toFunctor)).inv).toNatTrans.app
      X
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ prelaxfunctor.map₂ (Bicategory.leftUnitor f✝).hom =
    (Cat.Hom.isoMk (mapComp (𝟙 a✝).toFunctor f✝.toFunctor)).hom ≫
      Bicategory.whiskerRight (Cat.Hom.isoMk (mapId ↑a✝)).hom (prelaxfunctor.map f✝) ≫
        (Bicategory.leftUnitor (prelaxfunctor.map f✝)).hom

Tactic:
ext X

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
X : ↑(prelaxfunctor.obj a✝)
⊢ (prelaxfunctor.map₂ (Bicategory.leftUnitor f✝).hom).toNatTrans.app X =
    ((Cat.Hom.isoMk (mapComp (𝟙 a✝).toFunctor f✝.toFunctor)).hom ≫
            Bicategory.whiskerRight (Cat.Hom.isoMk (mapId ↑a✝)).hom (prelaxfunctor.map f✝) ≫
              (Bicategory.leftUnitor (prelaxfunctor.map f✝)).hom).toNatTrans.app
      X
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ prelaxfunctor.map₂ (Bicategory.rightUnitor f✝).hom =
    (Cat.Hom.isoMk (mapComp f✝.toFunctor (𝟙 b✝).toFunctor)).hom ≫
      Bicategory.whiskerLeft (prelaxfunctor.map f✝) (Cat.Hom.isoMk (mapId ↑b✝)).hom ≫
        (Bicategory.rightUnitor (prelaxfunctor.map f✝)).hom

Tactic:
ext X

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
X : ↑(prelaxfunctor.obj a✝)
⊢ (prelaxfunctor.map₂ (Bicategory.rightUnitor f✝).hom).toNatTrans.app X =
    ((Cat.Hom.isoMk (mapComp f✝.toFunctor (𝟙 b✝).toFunctor)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f✝) (Cat.Hom.isoMk (mapId ↑b✝)).hom ≫
              (Bicategory.rightUnitor (prelaxfunctor.map f✝)).hom).toNatTrans.app
      X
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
d : D
Z : (X : C) → (d ⟶ F.obj X) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : d ⟶ F.obj X₁) → (k₂ : d ⟶ F.obj X₂) → (f : X₁ ⟶ X₂) → k₁ ≫ F.map f = k₂ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : d ⟶ F.obj X₁) → (k₂ : d ⟶ F.obj X₂) → (f : X₁ ⟶ X₂) → k₁ ≫ F.map f = k₂ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : d ⟶ F.obj X₀
z : Z X₀ k₀
⊢ Z (lift F d) (homToLift F d)

Tactic:
apply Nonempty.some
  refine isPreconnected_induction (Z := fun Y : StructuredArrow d F => Z Y.right Y.hom)
    ?_ ?_ (j₀ := StructuredArrow.mk k₀) z _
  · exact fun f a ↦ h₁ _ _ _ _ f.right f.w a
  · exact fun f a ↦ h₂ _ _ _ _ f.right f.w a

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
⊢ 𝟙 (G.functor ⋙ F) = G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F)

Tactic:
ext X

Goal state after:
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 : D
⊢ ((𝟙 (G.functor ⋙ F)).app X).toFunctor =
    ((G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F)).app X).toFunctor
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case of.star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (starTerminal.from (incl.obj x)) ≫ hG.hom = h.hom.app x ≫ M x
X : C
f : of X ⟶ star
⊢ G.map f ≫
      (match star with
        | of x => h.app x
        | star => hG).hom =
    (match of X with
        | of x => h.app x
        | star => hG).hom ≫
      (lift F M hM).map f

Tactic:
cases f
        exact hh _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝ y✝ : WidePullbackShape J
x y : J
f : widePullbackShapeEquivObj (some x) ⟶ widePullbackShapeEquivObj (some y)
eq : x = y
⊢ WidePullbackShape.Hom (some y) (some y) = (some x ⟶ some y)

Tactic:
eq

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝ y✝ : WidePullbackShape J
x y : J
f : widePullbackShapeEquivObj (some x) ⟶ widePullbackShapeEquivObj (some y)
eq : x = y
⊢ WidePullbackShape.Hom (some y) (some y) = (some y ⟶ some y)
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ NatTrans.toCatHom₂ (map₂ (𝟙 f✝).toNatTrans) = 𝟙 (map f✝.toFunctor).toCatHom

Tactic:
ext X

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
X : ↑(Cat.of (WithInitial ↑a✝))
⊢ (NatTrans.toCatHom₂ (map₂ (𝟙 f✝).toNatTrans)).toNatTrans.app X = (𝟙 (map f✝.toFunctor).toCatHom).toNatTrans.app X
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : f✝ ⟶ g✝
θ✝ : g✝ ⟶ h✝
⊢ NatTrans.toCatHom₂ (map₂ (η✝ ≫ θ✝).toNatTrans) =
    NatTrans.toCatHom₂ (map₂ η✝.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ✝.toNatTrans)

Tactic:
ext X

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : f✝ ⟶ g✝
θ✝ : g✝ ⟶ h✝
X : ↑(Cat.of (WithInitial ↑a✝))
⊢ (NatTrans.toCatHom₂ (map₂ (η✝ ≫ θ✝).toNatTrans)).toNatTrans.app X =
    (NatTrans.toCatHom₂ (map₂ η✝.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ✝.toNatTrans)).toNatTrans.app X
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: 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 =
    (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

Tactic:
ext X

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
X : ↑(prelaxfunctor.obj a✝)
⊢ (prelaxfunctor.map₂ (Bicategory.associator f✝ g✝ h✝).hom).toNatTrans.app X =
    ((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
      X
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.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
⊢ (extendCone.obj c).π.app Y = c.π.app X ≫ G.map f

Tactic:
apply induction (k₀ := f) (z := rfl) F fun Z g =>
    c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f
  · intro _ _ _ _ _ h₁ h₂
    simp [← h₂, ← h₁, ← Functor.comp_map]
  · intro _ _ _ _ _ h₁ h₂
    simp [← h₁, ← Functor.comp_map, h₂]

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

Goal state before:
pp: case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork f g
⊢ IsLimit c.unop → IsColimit c

Tactic:
intro h
    exact (IsColimit.equivIsoColimit c.unopOpIso).toFun
      ((IsColimit.precomposeHomEquiv _ _).invFun ((IsColimit.whiskerEquivalenceEquiv _).toFun h.op))

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Surjective ⇑f
hker : (ker f).FG
⊢ f.FinitePresentation

Tactic:
by
  rw [← f.comp_id]
  exact (id A).comp_surjective hf hker

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this✝ : Algebra R S := f.toAlgebra
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] S
g' : MvPolynomial (Fin n) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : g'.comp MvPolynomial.C = f
⊢ Q R S f

Tactic:
subst this

Goal state after:
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
g' : MvPolynomial (Fin n) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
g : MvPolynomial (Fin n) R →ₐ[R] S
⊢ Q R S (g'.comp MvPolynomial.C)
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 : D ⥤ Cat
G : C ⥤ D
d : D
f : ↑(F.obj d)
X✝ Y✝ : StructuredArrow d G
g : X✝ ⟶ Y✝
⊢ ((G ⋙ F).map (StructuredArrow.Hom.right g)).toFunctor.obj
      (StructuredArrow.mk { base := X✝.hom, fiber := _root_.id (𝟙 ((F.map X✝.hom).toFunctor.obj f)) }).right.fiber =
    (StructuredArrow.mk { base := Y✝.hom, fiber := _root_.id (𝟙 ((F.map Y✝.hom).toFunctor.obj f)) }).right.fiber

Tactic:
dsimp +instances

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
d : D
f : ↑(F.obj d)
X✝ Y✝ : StructuredArrow d G
g : X✝ ⟶ Y✝
⊢ (F.map (G.map (StructuredArrow.Hom.right g))).toFunctor.obj ((F.map X✝.hom).toFunctor.obj f) =
    (F.map Y✝.hom).toFunctor.obj f
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin 0) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ Ideal.comap MvPolynomial.C (ker g') = Ideal.map (MvPolynomial.isEmptyRingEquiv R (Fin 0)).toRingHom (ker g')

Tactic:
simp only [RingEquiv.toRingHom_eq_coe, ← MvPolynomial.isEmptyRingEquiv_symm_toRingHom]

Goal state after:
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin 0) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ Ideal.comap (↑(MvPolynomial.isEmptyRingEquiv R (Fin 0)).symm) (ker g') =
    Ideal.map (↑(MvPolynomial.isEmptyRingEquiv R (Fin 0))) (ker g')
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₄).hom ≫ pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄ =
    pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄

Tactic:
trans l₂ ≫ pullback.snd _ _
  · rw [← Category.assoc]
    congr 1
    exact IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.right
  · exact pullback.lift_snd _ _ _

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.pullbacks ≤ P → P.IsStableUnderBaseChange

Tactic:
· intro h
    constructor
    intro _ _ _ _ _ _ _ _ h₁ h₂
    exact h _ ⟨_, _, _, _, _, h₂, h₁⟩

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.pushouts ≤ P → P.IsStableUnderCobaseChange

Tactic:
· intro h
    constructor
    intro _ _ _ _ _ _ _ _ h₁ h₂
    exact h _ ⟨_, _, _, _, _, h₂, h₁⟩

Goal state after:
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
H : (P.inverseImage e.functor).IsClosedUnderLimitsOfShape J
⊢ P = (P.inverseImage e.functor).inverseImage e.inverse

Tactic:
ext X

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

Tactic:
ext X

Goal state after:
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
H : (P.inverseImage e.functor).IsClosedUnderColimitsOfShape J
X : D
⊢ P X ↔ (P.inverseImage e.functor).inverseImage e.inverse X
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.colimitsOfShape J = (P.op.limitsOfShape Jᵒᵖ).unop

Tactic:
ext X

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
X : C
⊢ P.colimitsOfShape J X ↔ (P.op.limitsOfShape Jᵒᵖ).unop X
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.limitsOfShape J = (P.op.colimitsOfShape Jᵒᵖ).unop

Tactic:
ext X

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
X : C
⊢ P.limitsOfShape J X ↔ (P.op.colimitsOfShape Jᵒᵖ).unop X
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
inst✝ toBraidedCategory✝¹ : BraidedCategory C
symmetry✝¹ : ∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
toBraidedCategory✝ : BraidedCategory C
symmetry✝ : ∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
⊢ toBraidedCategory✝¹ = toBraidedCategory✝

Tactic:
exact Subsingleton.elim _ _

Goal state after:
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
c : C
⊢ ∑ i ∈ (ℛ R c).index, (toConv (antipode R)).ofConv ((ℛ R c).left i) * (toConv id).ofConv ((ℛ R c).right i) =
    (ofConv 1) c

Tactic:
simp [sum_antipode_mul_eq_algebraMap_counit (ℛ R c)]

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
⊢ (m ≫ fst (A ⊗ A) A) ≫ snd A A =
    (lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫
        fst (A ⊗ A) A) ≫
      snd A A

pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
⊢ m ≫ snd (A ⊗ A) A =
    lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫ snd (A ⊗ A) A

Tactic:
· have h : m ≫ fst _ _ ≫ fst _ _ = s.snd ≫ fst _ _ := by simpa using hm₂ =≫ fst _ _
        have := hm₁ =≫ fst _ _
        simp only [assoc, whiskerRight_fst, lift_fst, lift_snd] at this ⊢
        rw [← assoc, ← lift_comp_fst_snd (m ≫ _), assoc, assoc, h] at this
        rwa [← assoc s.snd, eq_lift_inv_left]

Goal state after:
case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
⊢ m ≫ snd (A ⊗ A) A =
    lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫ snd (A ⊗ A) A
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ X ◁ (λ_ ((ihom Y).obj Z)).inv ≫
      (α_ X (𝟙_ C) ((ihom Y).obj Z)).inv ≫ ((ρ_ X).hom ≫ f) ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z =
    f ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z

Tactic:
comp_whiskerRight_assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ X ◁ (λ_ ((ihom Y).obj Z)).inv ≫
      (α_ X (𝟙_ C) ((ihom Y).obj Z)).inv ≫ (ρ_ X).hom ▷ (ihom Y).obj Z ≫ f ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z =
    f ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
this✝¹ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
hLK : #ιL < ℵ₀
this : Fintype ιL
card_K : ℵ₀ < #(↥L)ᵐᵒᵖ ^ Fintype.card ιL
⊢ #(↥L)ᵐᵒᵖ ^ Fintype.card ιL ≤ #↥L

Tactic:
← MulOpposite.opEquiv.cardinal_eq

Goal state after:
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
this✝¹ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
hLK : #ιL < ℵ₀
this : Fintype ιL
card_K : ℵ₀ < #↥L ^ Fintype.card ιL
⊢ #↥L ^ Fintype.card ιL ≤ #↥L
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
m m' : M
⊢ (Dual.eval R M) m = (Dual.eval R M) m' → m = m'

Tactic:
eq

Goal state after:
R : Type uR
M : Type uM
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
m m' : M
eq : (Dual.eval R M) m = (Dual.eval R M) m'
⊢ m = m'
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case left
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Finite R M
inst✝ : Projective R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
g : M →ₗ[R] Fin n → R
eq : f ∘ₗ g = LinearMap.id
⊢ Function.Injective ⇑(dualTensorHom R (Fin n → R) N ∘ₗ rTensor N f.dualMap)

Tactic:
coe_comp,

Goal state after:
case left
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Finite R M
inst✝ : Projective R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
g : M →ₗ[R] Fin n → R
eq : f ∘ₗ g = LinearMap.id
⊢ Function.Injective (⇑(dualTensorHom R (Fin n → R) N) ∘ ⇑(rTensor N f.dualMap))