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
s : Cocone (F ⋙ G)
j j₁ j₂ : C
⊢ ∀ (k₁ : F.obj j ⟶ F.obj j₁) (k₂ : F.obj j ⟶ F.obj j₂) (f : j₁ ⟶ j₂),
    k₁ ≫ F.map f = k₂ → G.map k₁ ≫ s.ι.app j₁ = s.ι.app j → G.map k₂ ≫ s.ι.app j₂ = s.ι.app j

Tactic:
k₁

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
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
⊢ ∀ (k₂ : F.obj j ⟶ F.obj j₂) (f : j₁ ⟶ j₂),
    k₁ ≫ F.map f = k₂ → G.map k₁ ≫ s.ι.app j₁ = s.ι.app j → G.map k₂ ≫ s.ι.app j₂ = s.ι.app j
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
s : Cocone (F ⋙ G)
j j₁ j₂ : C
⊢ ∀ (k₁ : F.obj j ⟶ F.obj j₁) (k₂ : F.obj j ⟶ F.obj j₂) (f : j₁ ⟶ j₂),
    k₁ ≫ F.map f = k₂ → G.map k₂ ≫ s.ι.app j₂ = s.ι.app j → G.map k₁ ≫ s.ι.app j₁ = s.ι.app j

Tactic:
k₁

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
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
⊢ ∀ (k₂ : F.obj j ⟶ F.obj j₂) (f : j₁ ⟶ j₂),
    k₁ ≫ F.map f = k₂ → G.map k₂ ≫ s.ι.app j₂ = s.ι.app j → G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
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) (f_1 : Z₁ ⟶ Z₂),
    F.map f_1 ≫ k₂ = k₁ →
      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:
k₁

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) (f_1 : Z₁ ⟶ Z₂),
    F.map f_1 ≫ k₂ = k₁ →
      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.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) (f_1 : Z₁ ⟶ Z₂),
    F.map f_1 ≫ k₂ = k₁ →
      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:
k₁

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) (f_1 : Z₁ ⟶ Z₂),
    F.map f_1 ≫ k₂ = k₁ →
      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.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
s : Cone (F ⋙ G)
j j₁ j₂ : C
⊢ ∀ (k₁ : F.obj j₁ ⟶ F.obj j) (k₂ : F.obj j₂ ⟶ F.obj j) (f : j₁ ⟶ j₂),
    F.map f ≫ k₂ = k₁ → s.π.app j₁ ≫ G.map k₁ = s.π.app j → s.π.app j₂ ≫ G.map k₂ = s.π.app j

Tactic:
k₁

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
s : Cone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j₁ ⟶ F.obj j
⊢ ∀ (k₂ : F.obj j₂ ⟶ F.obj j) (f : j₁ ⟶ j₂),
    F.map f ≫ k₂ = k₁ → s.π.app j₁ ≫ G.map k₁ = s.π.app j → s.π.app j₂ ≫ G.map k₂ = s.π.app j
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
s : Cone (F ⋙ G)
j j₁ j₂ : C
⊢ ∀ (k₁ : F.obj j₁ ⟶ F.obj j) (k₂ : F.obj j₂ ⟶ F.obj j) (f : j₁ ⟶ j₂),
    F.map f ≫ k₂ = k₁ → s.π.app j₂ ≫ G.map k₂ = s.π.app j → s.π.app j₁ ≫ G.map k₁ = s.π.app j

Tactic:
k₁

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
s : Cone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j₁ ⟶ F.obj j
⊢ ∀ (k₂ : F.obj j₂ ⟶ F.obj j) (f : j₁ ⟶ j₂),
    F.map f ≫ k₂ = k₁ → s.π.app j₂ ≫ G.map k₂ = s.π.app j → s.π.app j₁ ≫ G.map k₁ = s.π.app j
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
inst✝ : IsFilteredOrEmpty C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop := fun h ↦ ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
Z : C
q₁ : (StructuredArrow.mk (g ≫ Final.homToLift F Y)).right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
h : (StructuredArrow.mk (g ≫ Final.homToLift F Y)).hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
| f ≫ Final.homToLift F Y ≫ F.map (q₁ ≫ IsFiltered.coeqHom q₁ q₂)

Tactic:
rw [IsFiltered.coeq_condition]

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
inst✝ : IsFilteredOrEmpty C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop := fun h ↦ ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
Z : C
q₁ : (StructuredArrow.mk (g ≫ Final.homToLift F Y)).right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
h : (StructuredArrow.mk (g ≫ Final.homToLift F Y)).hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
| f ≫ Final.homToLift F Y ≫ F.map (q₂ ≫ IsFiltered.coeqHom q₁ q₂)
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).hom ≫ fst (snd g g ≫ g) f ≫ fst g g = fst (fst f g) (fst f g) ≫ snd f g

Tactic:
delta diagonalObjPullbackFstIso
  simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).hom ≫ fst (snd g g ≫ g) f ≫ snd g g = snd (fst f g) (fst f g) ≫ snd f g

Tactic:
delta diagonalObjPullbackFstIso
  simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).hom ≫ snd (snd g g ≫ g) f = fst (fst f g) (fst f g) ≫ fst f g

Tactic:
delta diagonalObjPullbackFstIso
  simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).inv ≫ fst (fst f g) (fst f g) ≫ fst f g = snd (snd g g ≫ g) f

Tactic:
delta diagonalObjPullbackFstIso
  simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).inv ≫ fst (fst f g) (fst f g) ≫ snd f g = fst (snd g g ≫ g) f ≫ fst g g

Tactic:
delta diagonalObjPullbackFstIso
  simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).inv ≫ snd (fst f g) (fst f g) ≫ fst f g = snd (snd g g ≫ g) f

Tactic:
delta diagonalObjPullbackFstIso
  simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (diagonalObjPullbackFstIso f g).inv ≫ snd (fst f g) (fst f g) ≫ snd f g = fst (snd g g ≫ g) f ≫ snd g g

Tactic:
delta diagonalObjPullbackFstIso
  simp

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

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

Tactic:
refine (W.arrow_mk_iso_iff ?_).2 hf'

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.RespectsIso
inst✝ : P.IsStableUnderBaseChange
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
h₁ : P.diagonal x✝¹
h₂ : P.diagonal x✝
⊢ P
    ((pullbackDiagonalMapIdIso x✝¹ x✝¹ x✝).inv ≫
      pullback.snd (pullback.diagonal x✝) (pullback.map (x✝¹ ≫ x✝) (x✝¹ ≫ x✝) x✝ x✝ x✝¹ x✝¹ (𝟙 Z✝) ⋯ ⋯))

Tactic:
by simpa only [cancel_left_of_respectsIso] using P.pullback_snd _ _ h₂

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 : C
f : X ⟶ Y
inst✝ : HasPushout f f
⊢ (codiagonal f).op = pullback.diagonal f.op ≫ (pullbackIsoOpPushout f.op f.op).hom

Tactic:
by
  rw [← Iso.comp_inv_eq]
  ext <;> simp [← op_comp]

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 : C
inst✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ IsPullback (f ≫ pushout.inl f g).op (pushout.map (i ≫ f) (i ≫ g) f g (𝟙 X) (𝟙 Y) i ⋯ ⋯).op (pushout.codiagonal i).op
    (pushout.map i i (i ≫ f) (i ≫ g) f g (𝟙 S) ⋯ ⋯).op

Tactic:
simp only [op_pushoutMap, Quiver.Hom.unop_op, op_comp, unop_comp, op_id, pushout.op_codiagonal]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ IsPullback ((pushout.inl f g).op ≫ f.op)
    ((pullbackIsoOpPushout f.op g.op).inv ≫
      pullback.map f.op g.op (f.op ≫ i.op) (g.op ≫ i.op) (𝟙 (Opposite.op X)) (𝟙 (Opposite.op Y)) i.op ⋯ ⋯ ≫
        (pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)).hom)
    (pullback.diagonal i.op ≫ (pullbackIsoOpPushout i.op i.op).hom)
    ((pullbackIsoOpPushout (f.op ≫ i.op) (g.op ≫ i.op)).inv ≫
      pullback.map (f.op ≫ i.op) (g.op ≫ i.op) i.op i.op f.op g.op (𝟙 (Opposite.op S)) ⋯ ⋯ ≫
        (pullbackIsoOpPushout i.op i.op).hom)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case refine_1
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
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ ((Cone.postcompose (pairComp A B F).hom).obj (F.mapCone (BinaryFan.mk (fst A B) (snd A B)))).π.app
      { as := WalkingPair.left } =
    (Iso.refl ((Cone.postcompose (pairComp A B F).hom).obj (F.mapCone (BinaryFan.mk (fst A B) (snd A B)))).pt).hom ≫
      (Cone.extend (BinaryFan.mk (fst (F.obj A) (F.obj B)) (snd (F.obj A) (F.obj B))) (prodComparison F A B)).π.app
        { as := WalkingPair.left }

Tactic:
simp [pairComp]

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

Goal state before:
pp: case refine_2
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
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ ((Cone.postcompose (pairComp A B F).hom).obj (F.mapCone (BinaryFan.mk (fst A B) (snd A B)))).π.app
      { as := WalkingPair.right } =
    (Iso.refl ((Cone.postcompose (pairComp A B F).hom).obj (F.mapCone (BinaryFan.mk (fst A B) (snd A B)))).pt).hom ≫
      (Cone.extend (BinaryFan.mk (fst (F.obj A) (F.obj B)) (snd (F.obj A) (F.obj B))) (prodComparison F A B)).π.app
        { as := WalkingPair.right }

Tactic:
simp [pairComp]

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 ≫ F.obj X ◁ F.map (toUnit Y) ≫ fst (F.obj X) (F.obj (𝟙_ C)) = F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom

Tactic:
δ_natural_right_assoc

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.map (X ◁ toUnit Y) ≫ δ F X (𝟙_ C) ≫ fst (F.obj X) (F.obj (𝟙_ C)) = F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom
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, (antipode R) (repr.left i) * repr.right i = (algebraMap R A) (counit a)

Tactic:
by
  simpa [← repr.eq, map_sum] using congr($(mul_antipode_rTensor_comul (R := R)) a)

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
⊢ toConv (antipode R) * toConv id = 1

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

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : Y ⟶ (ihom X).obj Z
⊢ (((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).ofNatIsoLeft
              (Functor.Monoidal.commTensorLeft F X).compInverseIso).homEquiv
          Y Z).symm
      f =
    (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
      (adj.toEquivalence.symm.toAdjunction.homEquiv ((F ⋙ tensorLeft (F.obj X)).obj Y) Z).symm
        (uncurry ((adj.homEquiv Y ((ihom (F.obj X)).obj (adj.toEquivalence.symm.inverse.obj Z))).symm f))

Tactic:
Adjunction.homEquiv_ofNatIsoLeft_symm_apply

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : Y ⟶ (ihom X).obj Z
⊢ (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
      ((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).homEquiv Y Z).symm f =
    (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
      (adj.toEquivalence.symm.toAdjunction.homEquiv ((F ⋙ tensorLeft (F.obj X)).obj Y) Z).symm
        (uncurry ((adj.homEquiv Y ((ihom (F.obj X)).obj (adj.toEquivalence.symm.inverse.obj Z))).symm f))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : Closed X
f : X ⟶ Y
⊢ X ◁ curry' f ≫ (ihom.ev X).app Y = (ρ_ X).hom ≫ f

Tactic:
by
  dsimp [curry']
  simp only [whiskerLeft_curry_ihom_ev_app]

Goal state after:
Module: Mathlib.Logic.Equiv.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
s : Multiset α
⊢ (fun n ↦ Multiset.map (ofNat α) ↑(raise (ofNat (List ℕ) n) 0))
      ((fun s ↦ encode (lower ((Multiset.map encode s).sort fun a b ↦ a ≤ b) 0)) s) =
    s

Tactic:
have :=
        raise_lower (List.pairwise_cons.2 ⟨fun n _ => Nat.zero_le n,
        (s.map encode).pairwise_sort _⟩).sortedLE

Goal state after:
α : Type u_1
inst✝ : Denumerable α
s : Multiset α
this : raise (lower ((Multiset.map encode s).sort LE.le) 0) 0 = (Multiset.map encode s).sort LE.le
⊢ (fun n ↦ Multiset.map (ofNat α) ↑(raise (ofNat (List ℕ) n) 0))
      ((fun s ↦ encode (lower ((Multiset.map encode s).sort fun a b ↦ a ≤ b) 0)) s) =
    s
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ 𝟙 ((Y₂ ⊗ Y₁) ⊗ 𝟙_ C) ⊗≫
      Y₂ ◁ (Y₁ ◁ η_ X₁ Y₁ ⊗≫ ε_ X₁ Y₁ ▷ Y₁) ⊗≫ (Y₂ ◁ η_ X₂ Y₂ ⊗≫ ε_ X₂ Y₂ ▷ Y₂) ▷ Y₁ ⊗≫ 𝟙 (𝟙_ C ⊗ Y₂ ⊗ Y₁) =
    (ρ_ (Y₂ ⊗ Y₁)).hom ≫ (λ_ (Y₂ ⊗ Y₁)).inv

Tactic:
by rw [coevaluation_evaluation'', coevaluation_evaluation'']; monoidal

Goal state after:
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
⊢ Injective ⇑(Dual.eval R M)

Tactic:
by
  intro m m' eq
  simp_rw [LinearMap.ext_iff, Dual.eval_apply] at eq
  exact b.ext_elem fun i ↦ eq (b.coord i)

Goal state after:
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
inst✝ : Finite ι
b : Basis ι R M
⊢ (Dual.eval R M).range = ⊤

Tactic:
cases nonempty_fintype ι
    rw [← b.toDual_toDual, range_comp, b.toDual_range, Submodule.map_top, toDual_range _]

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

Goal state before:
pp: case inr
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_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)
hLK : #↥L < #K
this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
⊢ False

Tactic:
have rep_e := bK.linearCombination_repr (bL ∘ e)

Goal state after:
case inr
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_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)
hLK : #↥L < #K
this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
rep_e : (Finsupp.linearCombination K ⇑bK) (bK.repr (⇑bL ∘ ⇑e)) = ⇑bL ∘ ⇑e
⊢ False
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 : ι
⊢ (ε i) (lc e l) = l i

Tactic:
rw [lc, map_finsuppSum, Finsupp.sum_eq_single i (g := fun a b ↦ (ε i) (b • e a))]
  · simp [h.eval_same, smul_eq_mul]
  · intro q _ q_ne
    simp [h.eval_of_ne q_ne.symm, smul_eq_mul]
  · simp

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

Goal state before:
pp: R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
⊢ ∃ t, s ⊆ t ∧ #↑t = Module.rank R M ∧ LinearIndepOn R _root_.id t

Tactic:
have hsec' : (Submodule.mkQ _) ∘ sec = _root_.id := funext hsec

Goal state after:
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
⊢ ∃ t, s ⊆ t ∧ #↑t = Module.rank R M ∧ LinearIndepOn R _root_.id t
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : HasRankNullity.{u, u_1} R
inst✝² : IsDomain R
inst✝¹ : StrongRankCondition R
inst✝ : IsTorsionFree R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy : LinearIndependent R (Fin.snoc ![x] y)
⊢ ∃ y, LinearIndependent R ![x, y]

Tactic:
have : Fin.snoc ![x] y = ![x, y] := by simp

Goal state after:
R : Type u_1
M : Type u
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : HasRankNullity.{u, u_1} R
inst✝² : IsDomain R
inst✝¹ : StrongRankCondition R
inst✝ : IsTorsionFree R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy : LinearIndependent R (Fin.snoc ![x] y)
this : Fin.snoc ![x] y = ![x, y]
⊢ ∃ y, LinearIndependent R ![x, y]
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
s t : Submodule R M
⊢ Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)

Tactic:
(equivSubtypeMap s (comap _ (s ⊓ t))).rank_eq,

Goal state after:
R : Type u_1
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : HasRankNullity.{u, u_1} R
s t : Submodule R M
⊢ Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(map s.subtype (comap s.subtype (s ⊓ t))) +
      Module.rank R ↥((s ⊔ t) ⊓ t)