mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : CommRing A
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module A N
inst✝⁵ : Algebra R A
inst✝⁴ : Module R N
inst✝³ : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
c : A
hc : IsRegular c
x y : N
hxy : (fun x ↦ c • x) x = (fun x ↦ c • x) y
hS₀ : 0 ∈ S
⊢ x = y

pp: case neg
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : CommRing A
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module A N
inst✝⁵ : Algebra R A
inst✝⁴ : Module R N
inst✝³ : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
c : A
hc : IsRegular c
x y : N
hxy : (fun x ↦ c • x) x = (fun x ↦ c • x) y
hS₀ : 0 ∉ S
⊢ x = y

Tactic:
· have : Subsingleton N := (IsLocalizedModule.subsingleton_iff S f).2 fun _ ↦ ⟨0, hS₀, by simp⟩
      exact Subsingleton.elim ..

Goal state after:
case neg
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : CommRing A
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module A N
inst✝⁵ : Algebra R A
inst✝⁴ : Module R N
inst✝³ : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
c : A
hc : IsRegular c
x y : N
hxy : (fun x ↦ c • x) x = (fun x ↦ c • x) y
hS₀ : 0 ∉ S
⊢ x = y
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: case sup
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
I₁ I₂ : Submodule R R
hN₁✝ : I₁.FG
hN₂✝ : I₂.FG
h₁ : I₁ ≤ J.radical → ∃ n, I₁ ^ n ≤ J
h₂ : I₂ ≤ J.radical → ∃ n, I₂ ^ n ≤ J
h' : I₁ ⊔ I₂ ≤ J.radical
n₁ : ℕ
hn₁ : I₁ ^ n₁ ≤ J
n₂ : ℕ
hn₂ : I₂ ^ n₂ ≤ J
⊢ ∃ n, (I₁ ⊔ I₂) ^ n ≤ J

Tactic:
use n₁ + n₂

Goal state after:
case h
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
I₁ I₂ : Submodule R R
hN₁✝ : I₁.FG
hN₂✝ : I₂.FG
h₁ : I₁ ≤ J.radical → ∃ n, I₁ ^ n ≤ J
h₂ : I₂ ≤ J.radical → ∃ n, I₂ ^ n ≤ J
h' : I₁ ⊔ I₂ ≤ J.radical
n₁ : ℕ
hn₁ : I₁ ^ n₁ ≤ J
n₂ : ℕ
hn₂ : I₂ ^ n₂ ≤ J
⊢ (I₁ ⊔ I₂) ^ (n₁ + n₂) ≤ J
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: A : Type u_1
inst✝⁵ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁴ : Category.{v_2, u_2} B
T : Type u_3
inst✝³ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝² : Q.IsMultiplicative
inst✝¹ : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
inst✝ : IsIso f
⊢ Hom.hom (𝟙 X) = 𝟙 X.toComma

Tactic:
id_hom

Goal state after:
A : Type u_1
inst✝⁵ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁴ : Category.{v_2, u_2} B
T : Type u_3
inst✝³ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝² : Q.IsMultiplicative
inst✝¹ : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
inst✝ : IsIso f
⊢ 𝟙 X.toComma = 𝟙 X.toComma
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_1
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
⊢ Surjective ⇑(MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))

Tactic:
rw [← AlgHom.range_eq_top, ← Algebra.adjoin_range_eq_range_aeval,
      Set.range_comp f MvPolynomial.X, eq_top_iff, ← @adjoin_adjoin_of_tower R A B,
      adjoin_image, adjoin_range_X, Algebra.map_top, (AlgHom.range_eq_top _).mpr hf]
    exact fun {x} => subset_adjoin ⟨⟩

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

Goal state before:
pp: case w_fiber
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
⊢ eqToHom ⋯ = eqToHom ⋯ ≫ eqToHom ⋯ ≫ eqToHom ⋯

Tactic:
conv_rhs => rw [eqToHom_trans, eqToHom_trans]

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
X : C
inst✝ : IsConnected J
s : Cocone ((Functor.const J).obj X)
j : J
⊢ (constCocone J X).ι.app j ≫ s.ι.app (Classical.arbitrary J) = s.ι.app j

Tactic:
dsimp
    rw [id_comp]
    exact constant_of_preserves_morphisms _
      (fun _ _ f ↦ by simpa using (s.w f).symm) _ _

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.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : CreatesLimit (F ⋙ G) H
c : Cone (G ⋙ H)
hc : IsLimit c
i : H.mapCone (liftLimit ((isLimitWhiskerEquiv F c).symm hc)) ≅ Cone.whisker F c :=
  liftedLimitMapsToOriginal ((isLimitWhiskerEquiv F c).symm hc)
⊢ H.mapCone (extendCone.obj (liftLimit ((isLimitWhiskerEquiv F c).symm hc))) ≅ c

Tactic:
refine ?_ ≪≫ ((extendCone (F := F)).mapIso i) ≪≫ ((conesEquiv F (G ⋙ H)).counitIso.app _)

Goal state after:
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
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : CreatesLimit (F ⋙ G) H
c : Cone (G ⋙ H)
hc : IsLimit c
i : H.mapCone (liftLimit ((isLimitWhiskerEquiv F c).symm hc)) ≅ Cone.whisker F c :=
  liftedLimitMapsToOriginal ((isLimitWhiskerEquiv F c).symm hc)
⊢ H.mapCone (extendCone.obj (liftLimit ((isLimitWhiskerEquiv F c).symm hc))) ≅
    extendCone.obj (H.mapCone (liftLimit ((isLimitWhiskerEquiv F c).symm hc)))
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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.Initial
inst✝ : G.Initial
⊢ (F ⋙ G).op.Final

Tactic:
exact final_comp F.op G.op

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : C
X Y : Cᵒᵖ
f : X ⟶ Y
hf : RegularMono f
⊢ hf.left.unop ≫ f.unop = hf.right.unop ≫ f.unop

Tactic:
simp [← unop_comp, hf.w]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : C
X Y : Cᵒᵖ
f : X ⟶ Y
hf : RegularEpi f
⊢ f.unop ≫ hf.left.unop = f.unop ≫ hf.right.unop

Tactic:
simp [← unop_comp, hf.w]

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₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝² : HasPushout g₁ g₂
inst✝¹ : HasPushout g₃ g₄
inst✝ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
⊢ g₁ ≫ pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄ =
    g₂ ≫
      pushout.inl g₃ g₄ ≫
        pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
          (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯

Tactic:
pushout.inl_desc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝² : HasPushout g₁ g₂
inst✝¹ : HasPushout g₃ g₄
inst✝ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
⊢ g₁ ≫ pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄ =
    g₂ ≫ pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom =
    pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)

Tactic:
by
  trans f₂ ≫ l₁
  · congr 1
    exact
      (pushoutPushoutLeftIsPushout g₁ g₂ g₃ g₄).comp_coconePointUniqueUpToIso_hom _
        WalkingCospan.left
  · exact pushout.inr_desc _ _ _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ ∀ {X Y Y' S : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X},
    IsPullback f' g' g f → P.pullbacks g → P.pullbacks g'

Tactic:
rintro _ _ _ _ _ _ _ _ h ⟨_, _, _, _, _, hp, hq⟩
    exact P.pullbacks_mk (h.paste_horiz hq) hp

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

Tactic:
← Category.comp_id (pullback.fst _ _),

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ fst (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ 𝟙 T = (pullbackDiagonalMapIdIso f g i).hom ≫ fst f g ≫ f
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
Q : ObjectProperty C
h : P ≤ Q
⊢ P.strictLimitsOfShape J ≤ Q.strictLimitsOfShape J

Tactic:
rintro _ ⟨F, hF⟩

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
Q : ObjectProperty C
h : P ≤ Q
F : J ⥤ C
inst✝ : HasLimit F
hF : ∀ (j : J), P (F.obj j)
⊢ Q.strictLimitsOfShape J (limit 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
Q : ObjectProperty C
h : P ≤ Q
⊢ P.strictColimitsOfShape J ≤ Q.strictColimitsOfShape J

Tactic:
rintro _ ⟨F, hF⟩

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
Q : ObjectProperty C
h : P ≤ Q
F : J ⥤ C
inst✝ : HasColimit F
hF : ∀ (j : J), P (F.obj j)
⊢ Q.strictColimitsOfShape J (colimit F)
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
A B A' : C
inst✝¹ : IsIso (prodComparison F A B)
f : A ⟶ A'
inst✝ : IsIso (prodComparison F A' B)
⊢ F.map (f ▷ B) ≫ prodComparison F A' B = prodComparison F A B ≫ F.map f ▷ F.obj B

Tactic:
prodComparison_natural_whiskerRight

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
A B A' : C
inst✝¹ : IsIso (prodComparison F A B)
f : A ⟶ A'
inst✝ : IsIso (prodComparison F A' B)
⊢ prodComparison F A B ≫ F.map f ▷ F.obj B = prodComparison F A B ≫ F.map f ▷ F.obj B
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
D : Type u₁
inst✝⁶ : Category.{v₁, u₁} D
inst✝⁵ : CartesianMonoidalCategory D
F : C ⥤ D
E✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} E✝
inst✝³ : CartesianMonoidalCategory E✝
G✝ : D ⥤ E✝
A✝ B A' B' : C
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
A : C
inst✝ : ∀ (B : C), IsIso (prodComparison F A B)
⊢ IsIso (prodComparisonNatTrans F A)

Tactic:
let : ∀ X, IsIso ((prodComparisonNatTrans F A).app X) := by assumption

Goal state after:
C✝ : Type u
inst✝⁹ : Category.{v, u} C✝
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
E✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} E✝
inst✝³ : CartesianMonoidalCategory E✝
G✝ : D ⥤ E✝
A✝ B A' B' : C
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
A : C
inst✝ : ∀ (B : C), IsIso (prodComparison F A B)
this : ∀ (X : C), IsIso ((prodComparisonNatTrans F A).app X) := inst✝
⊢ IsIso (prodComparisonNatTrans F A)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case η
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F : C ⥤ D
G : D ⥤ E
X Y Z : C
inst✝¹ : F.OplaxMonoidal
inst✝ : PreservesFiniteProducts F
a b : F.OplaxMonoidal
⊢ η F = η F

pp: case δ
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F : C ⥤ D
G : D ⥤ E
X Y Z : C
inst✝¹ : F.OplaxMonoidal
inst✝ : PreservesFiniteProducts F
a b : F.OplaxMonoidal
⊢ δ F = δ F

Tactic:
· exact toUnit_unique _ _

Goal state after:
case δ
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F : C ⥤ D
G : D ⥤ E
X Y Z : C
inst✝¹ : F.OplaxMonoidal
inst✝ : PreservesFiniteProducts F
a b : F.OplaxMonoidal
⊢ δ F = δ F
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
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : CartesianMonoidalCategory E
F : C ⥤ D
G : D ⥤ E
inst✝² : F.Monoidal
inst✝¹ : G.Monoidal
inst✝ : (F ⋙ G).Monoidal
X Y : C
⊢ μ (F ⋙ G) X Y = μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)

Tactic:
by
  rw [← cancel_mono (μIso _ _ _).inv]; ext <;> simp [← Functor.comp_obj, ← Functor.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ lift (ι ≫ ι) ι ≫ μ = ι ≫ toUnit A ≫ η

Tactic:
← left_inv,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ lift (ι ≫ ι) ι ≫ μ = ι ≫ lift ι (𝟙 A) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
G : C
inst✝ : GrpObj G
⊢ μ ≫ ι = (ι ⊗ₘ ι) ≫ (β_ G G).hom ≫ μ

Tactic:
simp [tensorHom_inv_inv_mul]

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 Y : C
g : A ⊗ Y ⟶ X
⊢ B ◁ curry g ≫ f ▷ (ihom A).obj X ≫ (ihom.ev A).app X = f ▷ Y ≫ g

Tactic:
whisker_exchange_assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B : C
inst✝¹ : Closed A
inst✝ : Closed B
f : B ⟶ A
X Y : C
g : A ⊗ Y ⟶ X
⊢ f ▷ Y ≫ A ◁ curry g ≫ (ihom.ev A).app X = f ▷ Y ≫ g
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
A₁ A₂ A₃ : C
inst✝² : Closed A₁
inst✝¹ : Closed A₂
inst✝ : Closed A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ (conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁)) ((tensoringLeft C).map (f ≫ g)) =
    (conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₂)) ((tensoringLeft C).map g) ≫
      (conjugateEquiv (ihom.adjunction A₂) (ihom.adjunction A₁)) ((tensoringLeft C).map f)

Tactic:
conjugateEquiv_comp,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
A₁ A₂ A₃ : C
inst✝² : Closed A₁
inst✝¹ : Closed A₂
inst✝ : Closed A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ (conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁)) ((tensoringLeft C).map (f ≫ g)) =
    (conjugateEquiv (ihom.adjunction A₃) (ihom.adjunction A₁)) ((tensoringLeft C).map f ≫ (tensoringLeft C).map g)
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
inst✝ : Closed y
⊢ (ρ_ (x ⊗ (ihom x).obj y)).inv ≫ (x ⊗ (ihom x).obj y) ◁ id y ≫ (ihom.ev x).app y ▷ (ihom y).obj y ≫ (ihom.ev y).app y =
    uncurry (𝟙 ((ihom x).obj y))

Tactic:
whisker_exchange_assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ρ_ (x ⊗ (ihom x).obj y)).inv ≫ (ihom.ev x).app y ▷ 𝟙_ C ≫ (𝟭 C).obj y ◁ id y ≫ (ihom.ev y).app y =
    uncurry (𝟙 ((ihom x).obj y))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
w x y z : C
inst✝² : Closed w
inst✝¹ : Closed x
inst✝ : Closed y
⊢ w ◁ (α_ ((ihom w).obj x) ((ihom x).obj y) ((ihom y).obj z)).inv ≫
      (α_ w ((ihom w).obj x ⊗ (ihom x).obj y) ((ihom y).obj z)).inv ≫
        ((α_ w ((ihom w).obj x) ((ihom x).obj y)).inv ≫ (ihom.ev w).app x ▷ (ihom x).obj y ≫ (ihom.ev x).app y) ▷
            (ihom y).obj z ≫
          (ihom.ev y).app z =
    (α_ w ((ihom w).obj x) ((ihom x).obj y ⊗ (ihom y).obj z)).inv ≫
      (w ⊗ (ihom w).obj x) ◁
          curry
            ((α_ x ((ihom x).obj y) ((ihom y).obj z)).inv ≫ (ihom.ev x).app y ▷ (ihom y).obj z ≫ (ihom.ev y).app z) ≫
        (ihom.ev w).app x ▷ (ihom x).obj z ≫ (ihom.ev x).app z

Tactic:
whisker_exchange_assoc,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
w x y z : C
inst✝² : Closed w
inst✝¹ : Closed x
inst✝ : Closed y
⊢ w ◁ (α_ ((ihom w).obj x) ((ihom x).obj y) ((ihom y).obj z)).inv ≫
      (α_ w ((ihom w).obj x ⊗ (ihom x).obj y) ((ihom y).obj z)).inv ≫
        ((α_ w ((ihom w).obj x) ((ihom x).obj y)).inv ≫ (ihom.ev w).app x ▷ (ihom x).obj y ≫ (ihom.ev x).app y) ▷
            (ihom y).obj z ≫
          (ihom.ev y).app z =
    (α_ w ((ihom w).obj x) ((ihom x).obj y ⊗ (ihom y).obj z)).inv ≫
      (ihom.ev w).app x ▷ ((ihom x).obj y ⊗ (ihom y).obj z) ≫
        x ◁
            curry
              ((α_ x ((ihom x).obj y) ((ihom y).obj z)).inv ≫ (ihom.ev x).app y ▷ (ihom y).obj z ≫ (ihom.ev y).app z) ≫
          (ihom.ev x).app z
Module: Mathlib.Data.W.Basic

Goal state before:
pp: case succ.zero
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          n =
        (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          m →
      n = m
h :
  (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      (n + 1) =
    (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      0
⊢ n + 1 = 0

pp: case succ.succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          n =
        (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      (n + 1) =
    (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      (m + 1)
⊢ n + 1 = m + 1

Tactic:
· simp_all

Goal state after:
case succ.succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          n =
        (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      (n + 1) =
    (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      (m + 1)
⊢ n + 1 = m + 1
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
b : Basis ι R M
inst✝ : Fintype ι
f : Dual R M
m : M
⊢ ∑ x, (b.coord x) m • f (b x) = f m

Tactic:
← f.map_smul,

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Fintype ι
f : Dual R M
m : M
⊢ ∑ x, f ((b.coord x) m • b x) = f m
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:

Tactic:
_ = η_ X₁ Y₁ ▷ (X₁ ⊗ X₂) ⊗≫
          (X₁ ◁ η_ X₂ Y₂) ▷ (Y₁ ⊗ X₁ ⊗ X₂) ⊗≫
          (X₁ ⊗ X₂) ◁ (Y₂ ◁ ε_ X₁ Y₁ ▷ X₂) ⊗≫
          (X₁ ⊗ X₂) ◁ ε_ X₂ Y₂ := by monoidal
      -- Group η₂ and ε₁ so they compose with ≫:
      --
      --   ╭── Y₁ ────────────╮       X₁   X₂
      --   │    ╭── Y₂ ───╮   │       │    │
      --   │    │         │   │       │    │
      --   │    │         │   ╰──ε₁───╯    │
      --   │    │         │                │
      --   │    │         ╰──────── ε₂ ────╯
      --   X₁   X₂
      --
      _ = η_ X₁ Y₁ ▷ (X₁ ⊗ X₂) ⊗≫
          X₁ ◁ (η_ X₂ Y₂ ▷ (Y₁ ⊗ X₁) ≫ (X₂ ⊗ Y₂) ◁ ε_ X₁ Y₁) ▷ X₂ ⊗≫
          (X₁ ⊗ X₂) ◁ ε_ X₂ Y₂ := by monoidal
      -- Slide the ε₁ cap past the η₂ cup (← whisker_exchange), separating the
      -- two zigzags into independent snakes:
      --
      --                 X₁   X₂
      --   ╭──Y₁──╮      │    │
      --   │      │      │    │
      --   │      ╰──────╯    │       ← snake for (X₁, Y₁)
      --   │                  │
      --   │   ╭──Y₂──╮       │
      --   │   │      │       │
      --   │   │      ╰───────╯       ← snake for (X₂, Y₂)
      --   X₁  X₂
      --
      _ = η_ X₁ Y₁ ▷ (X₁ ⊗ X₂) ⊗≫
          X₁ ◁ ((𝟙_ C) ◁ ε_ X₁ Y₁ ≫ η_ X₂ Y₂ ▷ (𝟙_ C)) ▷ X₂ ⊗≫
          (X₁ ⊗ X₂) ◁ ε_ X₂ Y₂ := by
        rw [← whisker_exchange]
      -- Separate into two snakes and cancel each.
      _ = 𝟙 _ ⊗≫ (η_ X₁ Y₁ ▷ X₁ ⊗≫ X₁ ◁ ε_ X₁ Y₁) ▷ X₂ ⊗≫
          X₁ ◁ (η_ X₂ Y₂ ▷ X₂ ⊗≫ X₂ ◁ ε_ X₂ Y₂) ⊗≫ 𝟙 _ := by monoidal
      _ = _ := by rw [evaluation_coevaluation'', evaluation_coevaluation'']; monoidal

Goal state after: