mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : ReflectsColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit (H.mapCocone c)
⊢ Nonempty (IsColimit c)

Tactic:
refine ⟨isColimitExtendCoconeEquiv F _ (isColimitOfReflects H ?_)⟩
    let hc' := (isColimitExtendCoconeEquiv (G := G ⋙ H) F _).symm hc
    exact IsColimit.ofIsoColimit hc' (Cocone.ext (Iso.refl _) (by simp))

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
⊢ m₂ = desc X π (fun a ↦ π a ≫ m₂) ⋯

Tactic:
apply EffectiveEpiFamily.uniq

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
⊢ ∀ (a : α), π a ≫ m₂ = π a ≫ m₂
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.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : F.obj Z₁ ⟶ Y
k₂ : F.obj Z₂ ⟶ Y
g : Z₁ ⟶ Z₂
a : F.map g ≫ k₂ = k₁
z : c.π.app Z₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
⊢ c.π.app Z₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f

Tactic:
rw [← a, Functor.map_comp, ← Functor.comp_map, ← Category.assoc, ← Category.assoc,
                c.w] at 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.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : F.obj Z₁ ⟶ Y
k₂ : F.obj Z₂ ⟶ Y
g : Z₁ ⟶ Z₂
a : F.map g ≫ k₂ = k₁
z : c.π.app Z₂ ≫ G.map k₂ = (c.π.app (lift F X) ≫ G.map (homToLift F X)) ≫ G.map f
⊢ c.π.app Z₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork f g
⊢ c.unop.π.app WalkingParallelPair.one = (c.ι.app WalkingParallelPair.zero).unop

Tactic:
by
  simp [unop]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork f g
⊢ c.unop.π.app WalkingParallelPair.zero = (c.ι.app WalkingParallelPair.one).unop

Tactic:
by
  simp [unop]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Fork f g
⊢ c.unop.ι.app WalkingParallelPair.one = (c.π.app WalkingParallelPair.zero).unop

Tactic:
by
  simp [unop]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Fork f g
⊢ c.unop.ι.app WalkingParallelPair.zero = (c.π.app WalkingParallelPair.one).unop

Tactic:
by
  simp [unop]

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

Goal state before:
pp: case z
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
s : Cone (F ⋙ G)
j : C
⊢ s.π.app ?X₀ ≫ G.map ?k₀ = s.π.app j

pp: case X₀
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
s : Cone (F ⋙ G)
j : C
⊢ 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.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cone (F ⋙ G)
j : C
⊢ F.obj ?X₀ ⟶ F.obj j

Tactic:
· exact s.w (𝟙 _)

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := sC.inverse.whiskerLeft (whiskerRight α Cat.asSmallFunctor)
this : ∀ (X : AsSmall C), (α'.app X).toFunctor.Final
hα' : (map (sC.symm.functor.whiskerLeft (whiskerRight α Cat.asSmallFunctor))).Final
i :
  map (sC.symm.functor.whiskerLeft (whiskerRight α Cat.asSmallFunctor)) ≅
    (preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
        (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse
⊢ (map α).Final

Tactic:
have := final_of_natIso i

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := sC.inverse.whiskerLeft (whiskerRight α Cat.asSmallFunctor)
this✝ : ∀ (X : AsSmall C), (α'.app X).toFunctor.Final
hα' : (map (sC.symm.functor.whiskerLeft (whiskerRight α Cat.asSmallFunctor))).Final
i :
  map (sC.symm.functor.whiskerLeft (whiskerRight α Cat.asSmallFunctor)) ≅
    (preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
        (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse
this :
  ((preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
        (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse).Final
⊢ (map α).Final
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

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

Tactic:
← isStableUnderBaseChange_iff_pullbacks_le

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderBaseChange
⊢ P.IsStableUnderBaseChange
Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
hf : f.FiniteType
⊢ ∃ T e, f = e.toRingHom.comp (algebraMap R ↑(FGAlgCatSkeleton.eval R T).obj)

Tactic:
algebraize [f]

Goal state after:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
hf : f.FiniteType
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.FiniteType R S
⊢ ∃ T e, f = e.toRingHom.comp (algebraMap R ↑(FGAlgCatSkeleton.eval R T).obj)
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
⊢ s.pt ⟶ (extendFan c₁ c₂).pt

Tactic:
apply (BinaryFan.IsLimit.lift' t₂ (s.π.app ⟨0⟩) _).1

Goal state after:
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
⊢ ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 } ⟶ c₁.pt
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
this : ∀ (f : Fin n → C), PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
⊢ PreservesLimit (Discrete.functor f) F

Tactic:
apply
      preservesLimit_of_preserves_limit_cone
        (extendFanIsLimit f (limit.isLimit _) (limit.isLimit _)) _

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
this : ∀ (f : Fin n → C), PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
⊢ IsLimit
    (F.mapCone
      (extendFan (limit.cone (Discrete.functor fun i ↦ f i.succ))
        (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i ↦ f i.succ)).pt))))
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
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
e : { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
⊢ W.limitsOfShape J (Arrow.hom { left := Y₁, right := Y₂, hom := g })

Tactic:
have fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift (Cone.mk _ (c₁.π ≫ f)) :=
      e.inv.w.symm

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
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
e : { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }
⊢ W.limitsOfShape J (Arrow.hom { left := Y₁, right := Y₂, hom := g })
Module: Mathlib.CategoryTheory.ObjectProperty.Retract

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

Tactic:
exact Subtype.ext_iff.1 h₂.2

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

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

Tactic:
by simp [reassoc_of% hri]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x ↦ X₁) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₁)
c₂ : Cocone (Discrete.functor fun x ↦ X₂) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ { pt := c₂.pt, ι := (Discrete.natTrans fun x ↦ f) ≫ c₂.ι }.ι.app (⊥_ Discrete PUnit.{w + 1}) =
    c₁.ι.app (⊥_ Discrete PUnit.{w + 1}) ≫ f

Tactic:
simp [c₁, c₂]

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

Goal state before:
pp: J : Type w
inst✝⁶ : Category.{w', w} J
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : HasLimitsOfShape J C
inst✝² : PreservesLimitsOfShape J F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ F.essImage.strictLimitsOfShape J ≤ F.essImage

Tactic:
by
    rintro _ ⟨G, hG⟩
    exact ⟨limit (Functor.essImage.liftFunctor G F hG),
      ⟨IsLimit.conePointsIsoOfNatIso
        (isLimitOfPreserves F (limit.isLimit _)) (limit.isLimit _)
        (Functor.essImage.liftFunctorCompIso _ _ _)⟩⟩

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

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} Q
⊢ P ≤ Q → coproducts.{w, v, u} P ≤ Q

Tactic:
· intro h
    exact le_trans (coproducts_monotone h) Q.coproducts_le

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ (P.strictColimitsOfShape J).isoClosure = P.colimitsOfShape J

Tactic:
by
  refine le_antisymm ?_ ?_
  · rw [isoClosure_le_iff]
    apply strictColimitsOfShape_le_colimitsOfShape
  · intro X ⟨h⟩
    have := h.hasColimit
    exact ⟨colimit h.diag, strictColimitsOfShape.colimit h.diag h.prop_diag_obj,
      ⟨h.isColimit.coconePointUniqueUpToIso (colimit.isColimit _)⟩⟩

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

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

Tactic:
by
  simp [uncurry_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ Preadditive.preadditiveHasZeroMorphisms = Limits.hasZeroMorphismsOpposite

Tactic:
by
  with_reducible_and_instances rfl

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

Tactic:
by
  simp [uncurry_eq]

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
x y : M
h : b.toDual x = b.toDual y
i : ι
⊢ (b.repr x) i = (b.repr y) i

Tactic:
← toDual_eq_repr

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
x y : M
h : b.toDual x = b.toDual y
i : ι
⊢ (b.toDual x) (b i) = (b.toDual y) (b i)
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ (l.sum fun a b ↦ (ε i) (b • e a)) = l i

Tactic:
Finsupp.sum_eq_single i (g := fun a b ↦ (ε i) (b • e a))

Goal state after:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ (ε i) (l i • e i) = l i

case h₀
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ ∀ (b : ι), l b ≠ 0 → b ≠ i → (ε i) (l b • e b) = 0

case h₁
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ l i = 0 → (ε i) (0 • e i) = 0
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: case inl
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
i : ι
⊢ (h.basis.repr (e i)) i = (Finsupp.single i 1) i

pp: case inr
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
i j : ι
hne : i ≠ j
⊢ (h.basis.repr (e i)) j = (Finsupp.single i 1) j

Tactic:
· simp [h.eval_same]

Goal state after:
case inr
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
i j : ι
hne : i ≠ j
⊢ (h.basis.repr (e i)) j = (Finsupp.single i 1) j
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
g : ᘁX ⟶ Z
⊢ (ᘁf) ≫ g = 𝟙 ᘁY ⊗≫ η_ (ᘁX) X ▷ ᘁY ⊗≫ ᘁX ◁ f ▷ ᘁY ⊗≫ (ᘁX ◁ ε_ (ᘁY) Y ≫ g ▷ 𝟙_ C) ⊗≫ 𝟙 Z

Tactic:
dsimp only [leftAdjointMate]; monoidal

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: case e'_3
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ #(M →ₐ[K] L) = lift.{max u_2 v, max u_2 v} #(M →ₐ[K] L)

pp: case e'_4
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ lift.{v, u_2} (Module.rank K M) = lift.{max u_2 v, max u_2 v} (Module.rank L (M →ₗ[K] L))

Tactic:
· rw [lift_id]

Goal state after:
case e'_4
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ lift.{v, u_2} (Module.rank K M) = lift.{max u_2 v, max u_2 v} (Module.rank L (M →ₗ[K] L))
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring R₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst✝ : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
⊢ (B a) (a + b + c) = (B (a + b + c)) c

Tactic:
hAdd,

Goal state after:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring R₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst✝ : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
⊢ (B a) 0 = (B 0) c
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B' ∘ₗ f = B.compl₂ g
x✝ : M
y✝ : M₁
⊢ (B' (f x✝)) y✝ = ((B.compl₂ g) x✝) y✝

Tactic:
← comp_apply,

Goal state after:
case mpr
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B' ∘ₗ f = B.compl₂ g
x✝ : M
y✝ : M₁
⊢ ((B' ∘ₗ f) x✝) y✝ = ((B.compl₂ g) x✝) y✝
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
f : Dual R (M ⊗[R] N)
⊢ (dualDistribInvOfBasis b c) f = ∑ i, ∑ j, f (b i ⊗ₜ[R] c j) • b.dualBasis i ⊗ₜ[R] c.dualBasis j

Tactic:
by
  simp [dualDistribInvOfBasis]

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case inr
R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x ≤ 0
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Tactic:
replace hx : B x x = 0 := le_antisymm hx (hs x)

Goal state after:
case inr
R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f ↦ F.obj f.fst.1
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ s = F.map f.snd ≫ c₂.ι.app { as := f.fst.2 }
ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ t = c₂.ι.app { as := f.fst.1 }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
⊢ s ≫ t₂.desc (Cofan.mk q.1 fun j ↦ q.ι.app j) = t ≫ t₂.desc (Cofan.mk q.1 fun j ↦ q.ι.app j)

Tactic:
· apply t₁.hom_ext
      intro ⟨j⟩
      have reassoced_s (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} (h : _ ⟶ W) :
        c₁.ι.app ⟨f⟩ ≫ s ≫ h = F.map f.snd ≫ c₂.ι.app ⟨f.fst.snd⟩ ≫ h := by
          simp only [← Category.assoc]
          apply eq_whisker (hs f)
      have reassoced_t (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} (h : _ ⟶ W) :
        c₁.ι.app ⟨f⟩ ≫ t ≫ h = c₂.ι.app ⟨f.fst.fst⟩ ≫ h := by
          simp only [← Category.assoc]
          apply eq_whisker (ht f)
      simp [reassoced_s, reassoced_t]

Goal state after: