mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: case a
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
| η ⊗ₘ η ≫ g

pp: case a
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
| (λ_ (𝟙_ C)).inv

Tactic:
one_hom

Goal state after:
case a
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
| η ⊗ₘ η

case a
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
| (λ_ (𝟙_ C)).inv
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M : C
inst✝² : MonObj M
inst✝¹ : BraidedCategory C
inst✝ : IsCommMonObj M
⊢ tensorμ M M M M ≫ (μ ⊗ₘ μ) ≫ μ = (μ ⊗ₘ μ) ≫ μ

Tactic:
by simp only [mon_tauto]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M : C
inst✝² : MonObj M
inst✝¹ : BraidedCategory C
inst✝ : IsCommMonObj M
⊢ tensorδ M M M M ≫ (μ ⊗ₘ μ) ≫ μ = (μ ⊗ₘ μ) ≫ μ

Tactic:
by simp only [mon_tauto]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ mk (a₁ * (IsLocalization.sec S x).1 • s₁) ((IsLocalization.sec S x).2 * (a₂ * s₂)) =
    mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂))

Tactic:
mul_smul_comm

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)) =
    mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂))
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
s : ↥S
⊢ Function.Bijective (⇑e ∘ ⇑((algebraMap R (End R M')) ↑s) ∘ ⇑e.symm)

Tactic:
EquivLike.comp_bijective,

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
s : ↥S
⊢ Function.Bijective (⇑((algebraMap R (End R M')) ↑s) ∘ ⇑e.symm)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
A : Type u_5
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M
S : Submonoid R
inst✝⁵ : Module A M
N : Type u_6
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module A N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
h : IsLocalizedModule (Algebra.algebraMapSubmonoid A S) f
s : ↥S
this : IsUnit ((algebraMap A (End A N)) ↑⟨(algebraMap R A) ↑s, ⋯⟩)
⊢ IsUnit ((algebraMap R (End R N)) ↑s)

Tactic:
simp only [← IsScalarTower.algebraMap_apply, Module.End.isUnit_iff] at this ⊢

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
A : Type u_5
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M
S : Submonoid R
inst✝⁵ : Module A M
N : Type u_6
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module A N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
h : IsLocalizedModule (Algebra.algebraMapSubmonoid A S) f
s : ↥S
this : Function.Bijective ⇑((algebraMap R (End A N)) ↑s)
⊢ Function.Bijective ⇑((algebraMap R (End R N)) ↑s)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
M : Type u_2
inst✝¹⁰ : AddCommMonoid M
A : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
inst✝⁷ : Module R M
S : Submonoid R
N : Type u_6
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Module A M
inst✝³ : Module A N
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R A N
f : M →ₗ[A] N
inst✝ : IsLocalizedModule S (↑R f)
x : R
hx : x ∈ ↑S
this : IsUnit ((algebraMap R (End R N)) ↑⟨x, hx⟩)
⊢ IsUnit ((algebraMap A (End A N)) ↑⟨(algebraMap R A) x, ⋯⟩)

Tactic:
simp only [← IsScalarTower.algebraMap_apply, Module.End.isUnit_iff] at this ⊢

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Type u_2
inst✝¹⁰ : AddCommMonoid M
A : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
inst✝⁷ : Module R M
S : Submonoid R
N : Type u_6
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Module A M
inst✝³ : Module A N
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R A N
f : M →ₗ[A] N
inst✝ : IsLocalizedModule S (↑R f)
x : R
hx : x ∈ ↑S
this : Function.Bijective ⇑((algebraMap R (End R N)) x)
⊢ Function.Bijective ⇑((algebraMap R (End A N)) x)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ f m = 1 • mk' f m 1

Tactic:
mk'_one,

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ f m = 1 • f m
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
j k : J
f : j ⟶ k
⊢ ((Functor.const J).obj (of (FreeCommRing PUnit.{u + 1}))).map f ≫
      ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv k) =
    ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j) ≫ F.map f

Tactic:
ext1; change FreeCommRing.lift (fun _ => inv k) = _
      ext; simp [map_inv f]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_6
M : Type u_8
M' : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝ : IsLocalizedModule S g
⊢ Subsingleton M' ↔ ⊤ ≤ g.ker

Tactic:
refine ⟨fun H m _ ↦ Subsingleton.elim _ _, fun H ↦ (subsingleton_iff_forall_eq 0).mpr fun x ↦ ?_⟩

Goal state after:
R : Type u_6
M : Type u_8
M' : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝ : IsLocalizedModule S g
H : ⊤ ≤ g.ker
x : M'
⊢ x = 0
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
⊢ IsLocalHom (Hom.hom (pullback.fst f g))

Tactic:
by
  refine Limits.π_isLocalHom _ (limit.isLimit _) left fun x hx i ↦ ?_
  rcases i with _ | _ | _
  · exact ⟨one, 𝟙 _, Hom.inl, inferInstance, by simp; rfl⟩
  · exact ⟨left, 𝟙 _, 𝟙 _, inferInstance, by simp⟩
  · refine ⟨one, Hom.inr, Hom.inl, ‹_›, ?_⟩
    exact DFunLike.congr_fun (congr(Hom.hom $(pullback.condition (f := f) (g := g)))) x |>.symm

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P Q : ObjectProperty C
h : P.op = Q.op
⊢ P.op.unop = Q

Tactic:
← Q.unop_op,

Goal state after:
C : Type u
inst✝ : CategoryStruct.{v, u} C
P Q : ObjectProperty C
h : P.op = Q.op
⊢ P.op.unop = Q.op.unop
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: ⊢ binaryProductFunctor ≅ prod.functor

Tactic:
refine NatIso.ofComponents (fun X => ?_) (fun _ => ?_)

Goal state after:
case refine_1
X : Type u
⊢ binaryProductFunctor.obj X ≅ prod.functor.obj X

case refine_2
X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ binaryProductFunctor.map x✝ ≫ Iso.hom ?refine_1 = Iso.hom ?refine_1 ≫ prod.functor.map x✝
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case refine_1.refine_2
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ (binaryProductFunctor.obj X).map x✝ ≫
      ((limit.isLimit (pair X Y✝)).conePointUniqueUpToIso (binaryProductLimit X Y✝)).symm.hom =
    ((limit.isLimit (pair X X✝)).conePointUniqueUpToIso (binaryProductLimit X X✝)).symm.hom ≫
      (prod.functor.obj X).map x✝

Tactic:
apply Limits.prod.hom_ext <;> simp

Goal state after:
case refine_1.refine_2.h₁
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ (↾fun x ↦ (x.1, (ConcreteCategory.hom x✝) x.2)) ≫ ↾_root_.Prod.fst = ↾_root_.Prod.fst

case h₂
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ (↾fun x ↦ (x.1, (ConcreteCategory.hom x✝) x.2)) ≫ ↾_root_.Prod.snd = ↾_root_.Prod.snd ≫ x✝
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case refine_2
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ (binaryProductFunctor.map x✝¹ ≫
          (NatIso.ofComponents
              (fun Y ↦ ((limit.isLimit (pair Y✝ Y)).conePointUniqueUpToIso (binaryProductLimit Y✝ Y)).symm) ⋯).hom).app
      x✝ =
    ((NatIso.ofComponents (fun Y ↦ ((limit.isLimit (pair X✝ Y)).conePointUniqueUpToIso (binaryProductLimit X✝ Y)).symm)
              ⋯).hom ≫
          prod.functor.map x✝¹).app
      x✝

Tactic:
apply Limits.prod.hom_ext <;> simp

Goal state after:
case refine_2.h₁
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ BinaryFan.IsLimit.lift (binaryProductLimit Y✝ x✝) (↾_root_.Prod.fst ≫ x✝¹) (↾_root_.Prod.snd) ≫ ↾_root_.Prod.fst =
    ↾_root_.Prod.fst ≫ x✝¹

case h₂
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ BinaryFan.IsLimit.lift (binaryProductLimit Y✝ x✝) (↾_root_.Prod.fst ≫ x✝¹) (↾_root_.Prod.snd) ≫ ↾_root_.Prod.snd =
    ↾_root_.Prod.snd
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Faithful
⊢ autoParam (∀ {X_1 Y : P.CostructuredArrow ⊤ F X}, Function.Injective (CostructuredArrow.toOver P F X).map)
    Functor.Faithful.map_injective._autoParam

Tactic:
intro A B f g hfg

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Faithful
A B : P.CostructuredArrow ⊤ F X
f g : A ⟶ B
hfg : (CostructuredArrow.toOver P F X).map f = (CostructuredArrow.toOver P F X).map g
⊢ f = g
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: case mk.mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
fst✝¹ : C
snd✝¹ : F.obj fst✝¹
fst✝ : C
snd✝ : F.obj fst✝
h₁ : ⟨fst✝¹, snd✝¹⟩.fst = ⟨fst✝, snd✝⟩.fst
h₂ : (ConcreteCategory.hom (F.map (eqToHom h₁))) ⟨fst✝¹, snd✝¹⟩.snd = ⟨fst✝, snd✝⟩.snd
⊢ ⟨fst✝¹, snd✝¹⟩ = ⟨fst✝, snd✝⟩

Tactic:
cases h₁

Goal state after:
case mk.mk.refl
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
fst✝ : C
snd✝¹ snd✝ : F.obj fst✝
h₂ : (ConcreteCategory.hom (F.map (eqToHom ⋯))) ⟨fst✝, snd✝¹⟩.snd = ⟨fst✝, snd✝⟩.snd
⊢ ⟨fst✝, snd✝¹⟩ = ⟨fst✝, snd✝⟩
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ (map α).op ⋙ toCostructuredArrow F₂ = toCostructuredArrow F₁ ⋙ CostructuredArrow.map α

Tactic:
fapply Functor.ext
  · intro X
    simp only [CostructuredArrow.map_mk, toCostructuredArrow_obj, Functor.op_obj,
      Functor.comp_obj]
    congr
    ext _ f
    exact (α.naturality_apply f.op (unop X).snd).symm
  · simp

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
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ (F.map e₁.inv).toFunctor.obj ((F.map e₁.hom).toFunctor.obj X.fiber) = X.fiber

Tactic:
rw [← Cat.Hom.comp_obj, ← F.map_comp,e₁.hom_inv_id,F.map_id,Cat.Hom.id_obj]

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
inst✝¹ : IsConnected J
F : J ⥤ C
inst✝ : HasLimit F
c : Cone F
hc : IsLimit c
⊢ IsIso (limMap c.π)

Tactic:
suffices limMap c.π = ((limit.isLimit _).conePointUniqueUpToIso (isLimitConstCone J c.pt) ≪≫
      hc.conePointUniqueUpToIso (limit.isLimit _)).hom by
    rw [this]; infer_instance
  ext j
  simp only [limMap_π, limit.cone_x, Iso.trans_hom, assoc,
    limit.conePointUniqueUpToIso_hom_comp]
  congr 1
  simp [← Iso.inv_comp_eq_id]

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.comp (RingHom.id A)).FinitePresentation

Tactic:
exact (id A).comp_surjective hf hker

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

Goal state before:
pp: case pos.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : P d
this : Nonempty (CostructuredArrow P.ι d)
j₁ j₂ : CostructuredArrow P.ι d
⊢ j₂ ⟶ CostructuredArrow.mk (𝟙 (P.ι.obj { obj := d, property := hd }))

Tactic:
· exact CostructuredArrow.homMk (InducedCategory.homMk j₂.hom)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ (pullbackAssoc f₁ f₂ f₃ f₄).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 _ _

Goal state after:
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.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯ ≫
      pullback.snd f₃ f₄

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₂)
⊢ pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯ ≫
      pullback.snd f₃ f₄ =
    pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : h ≫ m = h ≫ p
this : Epi g
⊢ (f ≫ h) ≫ m = (f ≫ h) ≫ p

Tactic:
simp only [Category.assoc, z]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P g → P (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
⊢ P g'

Tactic:
have : HasPullback f g := sq.flip.hasPullback
    let e := sq.flip.isoPullback
    rw [← P.cancel_left_of_respectsIso e.inv, sq.flip.isoPullback_inv_fst]
    exact hP₂ _ _ _ f g hg

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case refine_2
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)
x✝ : Discrete (Fin (n + 1))
j : Fin (n + 1)
i : Fin n
⊢ (↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 })
            (t₁.lift { pt := s.pt, π := Discrete.natTrans fun x ↦ s.π.app { as := x.as.succ } })) ≫
        c₂.snd) ≫
      c₁.π.app { as := i } =
    s.π.app { as := i.succ }

Tactic:
(BinaryFan.IsLimit.lift' t₂ _ _).2.2,

Goal state after:
case refine_2
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)
x✝ : Discrete (Fin (n + 1))
j : Fin (n + 1)
i : Fin n
⊢ t₁.lift { pt := s.pt, π := Discrete.natTrans fun x ↦ s.π.app { as := x.as.succ } } ≫ c₁.π.app { as := i } =
    s.π.app { as := i.succ }
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 : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ CommSq g (lift (𝟙 Y) g ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)

Tactic:
· constructor
    ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
f : X ⟶ Y
Z : C
⊢ f ▷ Z ≫ fst Y Z = fst X Z ≫ f

Tactic:
by
  simp [fst_def, ← whisker_exchange_assoc]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M : C
inst✝ : MonObj M
⊢ lift (fst M M) (snd M M) ≫ μ = μ

Tactic:
lift_fst_snd,

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M : C
inst✝ : MonObj M
⊢ 𝟙 (M ⊗ M) ≫ μ = μ
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M : C
inst✝ : MonObj M
⊢ μ = lift (fst M M) (snd M M) ≫ μ

Tactic:
lift_fst_snd,

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M : C
inst✝ : MonObj M
⊢ μ = 𝟙 (M ⊗ M) ≫ μ
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 id * toConv (antipode R) = 1

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

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
h₁ h₂ : GrpObj X
e : h₁.toMonObj = h₂.toMonObj
this : ι = ι
⊢ h₁ = h₂

Tactic:
cases h₁

Goal state after:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
h₂ : GrpObj X
toMonObj✝ : MonObj X
inv✝ : X ⟶ X
left_inv✝ : lift inv✝ (𝟙 X) ≫ μ = toUnit X ≫ η
right_inv✝ : lift (𝟙 X) inv✝ ≫ μ = toUnit X ≫ η
e : { toMonObj := toMonObj✝, inv := inv✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toMonObj = h₂.toMonObj
this : ι = ι
⊢ { toMonObj := toMonObj✝, inv := inv✝, left_inv := left_inv✝, right_inv := right_inv✝ } = h₂
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
eq : ∀ (x : Dual R M), x m = x m'
⊢ m = m'

Tactic:
exact b.ext_elem fun i ↦ eq (b.coord i)

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

Goal state before:
pp: case mpr.inl
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : I₁ a = 0
⊢ (B x) y = 0

Tactic:
rw [map_eq_zero I₁] at H
      trivial

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case h₀
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
i : ι
j : κ
i' : ι
j' b✝ : κ
a✝¹ : b✝ ∈ Finset.univ
a✝ : b✝ ≠ j
⊢ (Finsupp.single b✝ 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) b✝) = 0

Tactic:
simp [*] at *

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case h₁
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
i : ι
j : κ
i' : ι
j' : κ
a✝ : j ∉ Finset.univ
⊢ (Finsupp.single j 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) j) = 0

Tactic:
simp [*] at *

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case h₀
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
i : ι
j : κ
i' : ι
j' : κ
b✝ : ι
a✝¹ : b✝ ∈ Finset.univ
a✝ : b✝ ≠ i
⊢ ∑ x, (Finsupp.single x 1) j * (Finsupp.single b✝ 1) i * ((Finsupp.single i' 1) b✝ * (Finsupp.single j' 1) x) = 0

Tactic:
simp [*] at *

Goal state after: