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
| ((f ⊗ₘ g) ⊗ₘ f ⊗ₘ g) ≫ tensorμ Y W Y W

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
| μ ⊗ₘ μ

Tactic:
rw [tensorμ_natural]

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
| tensorμ X Z X Z ≫ ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ 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
| μ ⊗ₘ μ
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : Epi g
W : C
fst' snd' : P ⟶ W
heq : inl ≫ fst' = inl ≫ snd'
⊢ inr ≫ fst' = inr ≫ snd'

Tactic:
simp [← cancel_epi g, ← h.w_assoc, heq]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M × ↥S
m : M
s : ↥S
⊢ 1 • (m, s).2 • (m, s).1 = 1 • (m, s).2 • (m, s).1

Tactic:
by rw [one_smul]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
β : LocalizedModule S M → LocalizedModule S M → Prop
h : ∀ (m m' : M) (s s' : ↥S), β (mk m s) (mk m' s')
⊢ ∀ (x y : LocalizedModule S M), β x y

Tactic:
rintro ⟨⟨m, s⟩⟩ ⟨⟨m', s'⟩⟩
  exact h m m' s s'

Goal state after:
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 : 1 ⊗ₜ[R] IsLocalization.mk' Rₘ x y = (algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)
⊢ (algebraMap S (Localization (Algebra.algebraMapSubmonoid S M))) ((RingHom.id S) ((algebraMap R S) x)) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
        (IsLocalization.mk' (Localization M) x y) *
      (algebraMap S (Localization (Algebra.algebraMapSubmonoid S M))) ((RingHom.id S) ((algebraMap R S) ↑y))

Tactic:
RingHom.id_apply

Goal state after:
R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 : 1 ⊗ₜ[R] IsLocalization.mk' Rₘ x y = (algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)
⊢ (algebraMap S (Localization (Algebra.algebraMapSubmonoid S M))) ((algebraMap R S) x) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
        (IsLocalization.mk' (Localization M) x y) *
      (algebraMap S (Localization (Algebra.algebraMapSubmonoid S M))) ((algebraMap R S) ↑y)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.h.mpr
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n) → ∃ a ∈ S, a • t • r • m = a • s • n

Tactic:
· rintro ⟨a, ha, eq1⟩
        refine ⟨a, ha, ?_⟩
        rw [← eq1, mul_comm, mul_smul, Submonoid.mk_smul, Submonoid.smul_def, Submonoid.mk_smul]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ C
Y : D
t : (G ⋙ (cocones J C).obj (op K)).obj Y
j j' : J
f : j ⟶ j'
⊢ (unop (op (unop (op (K ⋙ F))))).map f ≫ (adj.homEquiv (K.obj j') Y).symm (t.app j') =
    (adj.homEquiv (K.obj j) Y).symm (t.app j) ≫ ((const J).obj Y).map f

Tactic:
erw [← adj.homEquiv_naturality_left_symm, ← adj.homEquiv_naturality_right_symm, t.naturality]
    simp

Goal state after:
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_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a : M
⊢ ∀ (m' : M) (s s' : ↥S), lift' S g h (mk a s + mk m' s') = lift' S g h (mk a s) + lift' S g h (mk m' s')

Tactic:
a'

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
⊢ ∀ (s s' : ↥S), lift' S g h (mk a s + mk a' s') = lift' S g h (mk a s) + lift' S g h (mk 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✝ g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
r : R
x : LocalizedModule S M
⊢ lift' S g h (r • x) = lift' S g h ((RingHom.id R) r • x)

Tactic:
RingHom.id_apply

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✝ g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
r : R
x : LocalizedModule S M
⊢ lift' S g h (r • x) = lift' S g h (r • x)
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
y : N
⊢ ∃ x, x.2 • y = (↑R f) x.1

Tactic:
obtain ⟨⟨x, ⟨_, ⟨r, ⟨hr₁, rfl⟩⟩⟩⟩, hx⟩ := h.2 y

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
y : N
x : M
r : R
hr₁ : r ∈ ↑S
hx : (x, ⟨(algebraMap R A) r, ⋯⟩).2 • y = f (x, ⟨(algebraMap R A) r, ⋯⟩).1
⊢ ∃ x, x.2 • y = (↑R f) x.1
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
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
r : R
f : M →ₗ[A] N
h : IsLocalizedModule (Algebra.algebraMapSubmonoid A (Submonoid.powers r)) f
⊢ IsLocalizedModule (Submonoid.powers r) (↑R f)

Tactic:
exact IsLocalizedModule.restrictScalars _ f

Goal state after:
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
x y : LocalizedModule S M
a : M
⊢ ∀ (m' : M) (s s' : ↥S),
    fromLocalizedModule' S f (LocalizedModule.mk a s + LocalizedModule.mk m' s') =
      fromLocalizedModule' S f (LocalizedModule.mk a s) + fromLocalizedModule' S f (LocalizedModule.mk m' s')

Tactic:
a'

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
x y : LocalizedModule S M
a a' : M
⊢ ∀ (s s' : ↥S),
    fromLocalizedModule' S f (LocalizedModule.mk a s + LocalizedModule.mk a' s') =
      fromLocalizedModule' S f (LocalizedModule.mk a s) + fromLocalizedModule' S f (LocalizedModule.mk a' s')
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
X Y Z : Under R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom (f ≫ g))).toUnder =
    (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom f)).toUnder ≫
      (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom g)).toUnder

Tactic:
by simp [Algebra.TensorProduct.map_id_comp]

Goal state after:
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''
inst✝ : IsLocalizedModule S f
r : R
x : LocalizedModule S M
⊢ fromLocalizedModule' S f (r • x) = fromLocalizedModule' S f ((RingHom.id R) r • x)

Tactic:
RingHom.id_apply

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''
inst✝ : IsLocalizedModule S f
r : R
x : LocalizedModule S M
⊢ fromLocalizedModule' S f (r • x) = fromLocalizedModule' S f (r • x)
Module: Mathlib.CategoryTheory.Adjunction.Comma

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
⊢ (fun f ↦ (initial.to (StructuredArrow.mk f)).right) ((fun g ↦ (⊥_ StructuredArrow A G).hom ≫ G.map g) g) = g

Tactic:
let B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
⊢ (fun f ↦ (initial.to (StructuredArrow.mk f)).right) ((fun g ↦ (⊥_ StructuredArrow A G).hom ≫ G.map g) g) = g
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
s : BinaryCofan A B
x✝¹ : ↑((pair A B).obj { as := WalkingPair.left })
x✝ : ↑((pair A B).obj { as := WalkingPair.right })
⊢ Commute ((Hom.hom s.inl).toIntAlgHom x✝¹) ((Hom.hom s.inr).toIntAlgHom x✝)

Tactic:
by apply Commute.all

Goal state after:
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
j : J
hj :
  ∀ (x : ↑c.pt),
    IsUnit ((ConcreteCategory.hom (c.π.app j)) x) →
      ∀ (i : J),
        ∃ k f g,
          IsLocalHom (Hom.hom (F.map f)) ∧
            (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app i)) x) =
              (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (c.π.app j)) x)
x : ↑c.pt
hx : IsUnit ((Hom.hom (c.π.app j)) x)
⊢ IsUnit x

Tactic:
isUnit_iff_forall_isUnit F hc

Goal state after:
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
j : J
hj :
  ∀ (x : ↑c.pt),
    IsUnit ((ConcreteCategory.hom (c.π.app j)) x) →
      ∀ (i : J),
        ∃ k f g,
          IsLocalHom (Hom.hom (F.map f)) ∧
            (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app i)) x) =
              (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (c.π.app j)) x)
x : ↑c.pt
hx : IsUnit ((Hom.hom (c.π.app j)) x)
⊢ ∀ (j : J), IsUnit ((ConcreteCategory.hom (c.π.app j)) x)
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
hPQ : Q ≤ P.isoClosure
x✝ : Q.FullSubcategory
Y : C
hY : Q Y
⊢ (ιOfLE h).essImage { obj := Y, property := hY }

Tactic:
obtain ⟨X, hX, ⟨e⟩⟩ := hPQ _ hY
    exact ⟨⟨X, hX⟩, ⟨Q.ι.preimageIso e.symm⟩⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
F : C ⥤ D
⊢ Function.Surjective fun X ↦ ⟨F.obj ↑X, ⋯⟩

Tactic:
rintro ⟨_, ⟨X, hX⟩⟩
    exact ⟨⟨X, hX⟩, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ eqToHom ⋯ ≫ eqToHom ⋯ ≫ (F.map (𝟙 Y.base)).toFunctor.map f.fiber ≫ eqToHom ⋯ = f.fiber

Tactic:
← NatIso.naturality_2 ((Cat.Hom.toNatIso <| eqToIso (F.map_id Y.base)) ≪≫
        (eqToIso Cat.Hom.id_toFunctor)) f.fiber

Goal state after:
case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ eqToHom ⋯ ≫
      eqToHom ⋯ ≫
        ((Cat.Hom.toNatIso (eqToIso ⋯) ≪≫ eqToIso ⋯).hom.app ((F.map f.base).toFunctor.obj X.fiber) ≫
            (𝟭 ↑(F.obj Y.base)).map f.fiber ≫ (Cat.Hom.toNatIso (eqToIso ⋯) ≪≫ eqToIso ⋯).inv.app Y.fiber) ≫
          eqToHom ⋯ =
    f.fiber
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
⊢ 𝟙 X ≫ s.ι.app (Classical.arbitrary J) = s.ι.app j

Tactic:
rw [id_comp]

Goal state after:
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
⊢ s.ι.app (Classical.arbitrary J) = 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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit c
hc' : IsColimit (H.mapCocone (extendCocone.obj c)) := isColimitOfPreserves H ((isColimitExtendCoconeEquiv F c).symm hc)
⊢ IsColimit (extendCocone.obj (H.mapCocone c))

Tactic:
exact IsColimit.ofIsoColimit hc' (Cocone.ext (Iso.refl _) (by simp))

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.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)
hc' : IsColimit (extendCocone.obj (H.mapCocone c)) := (isColimitExtendCoconeEquiv F (H.mapCocone c)).symm hc
⊢ IsColimit (H.mapCocone (extendCocone.obj c))

Tactic:
exact IsColimit.ofIsoColimit hc' (Cocone.ext (Iso.refl _) (by simp))

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.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit c
hc' : IsColimit (H.mapCocone (Cocone.whisker F c)) := isColimitOfPreserves H ((isColimitWhiskerEquiv F c).symm hc)
⊢ IsColimit (Cocone.whisker F (H.mapCocone c))

Tactic:
exact IsColimit.ofIsoColimit hc' (Cocone.ext (Iso.refl _) (by simp))

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.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 (F ⋙ G) H
c : Cocone G
hc : IsColimit (H.mapCocone c)
hc' : IsColimit (Cocone.whisker F (H.mapCocone c)) := (isColimitWhiskerEquiv F (H.mapCocone c)).symm hc
⊢ IsColimit (H.mapCocone (Cocone.whisker F c))

Tactic:
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
X Y : C
f : Y ⟶ X
inst✝ : EffectiveEpi f
Z✝¹ : C
m₁ m₂ : X ⟶ Z✝¹
h✝ : f ≫ m₁ = f ≫ m₂
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ Y
h : x✝¹ ≫ f = x✝ ≫ f
⊢ x✝¹ ≫ f ≫ m₂ = x✝ ≫ f ≫ m₂

Tactic:
simp [← assoc, h]

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.op.ι = c.π.op

Tactic:
simp [Cofork.op, Fork.ι]

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
⊢ LocallySmall.{u, max u v, max (u + 1) (v + 1)} (FGAlgCat R)

Tactic:
refine ⟨fun A B ↦ ?_⟩

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
A B : FGAlgCat R
⊢ Small.{u, max u v} (A ⟶ B)
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
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
⊢ W.colimitsOfShape J φ

Tactic:
by
  obtain rfl : φ = h₁.desc (Cocone.mk _ (f ≫ c₂.ι)) := h₁.hom_ext (fun j ↦ by simp [hφ])
  exact ⟨_, _, _, _, _, h₂, _, hf⟩

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
⊢ ((h a).i ≫ r.r) ≫ r.i ≫ (h a).r = 𝟙 (Y ⟨↑a, ⋯⟩)

Tactic:
by simp [← reassoc_of% hri]

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

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

Tactic:
· 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.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f : X ⟶ M
⊢ lift (toUnit X) f ≫ (η ⊗ₘ 𝟙 M) ≫ μ = f ≫ 𝟙 M

Tactic:
tensorHom_id,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f : X ⟶ M
⊢ lift (toUnit X) f ≫ η ▷ M ≫ μ = f ≫ 𝟙 M
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H✝ H₁ H₂ G H : Grp C
⊢ homMk' (fst G.toMon H.toMon) = G ◁ (IsTerminal.ofUniqueHom (fun G ↦ homMk' (toUnit G.toMon)) ⋯).from H ≫ (ρ_ G).hom

Tactic:
ext; apply fst_def

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : HopfAlgebra R A
x : ↑(Opposite.unop (Opposite.op (of R A)))
⊢ (Algebra.TensorProduct.lmul' R) ((Algebra.TensorProduct.map (antipodeAlgHom R A) (AlgHom.id R A)) (comul x)) =
    (algebraMap R A) (counit x)

Tactic:
exact mul_antipode_rTensor_comul_apply (R := R) x

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
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
by
  obtain ⟨s, hs, hs'⟩ :=
    exists_finset_linearIndependent_of_le_finrank (R := R) (M := M ⧸ N) le_rfl
  obtain ⟨v, hv⟩ : s.Nonempty := by rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero,
    hs, finrank_quotient, tsub_eq_zero_iff_le, not_le]
  obtain ⟨v, rfl⟩ := N.mkQ_surjective v
  refine ⟨v, fun r hr ↦ mt ?_ hr⟩
  have := linearIndependent_iff.mp hs' (Finsupp.single ⟨_, hv⟩ r)
  rwa [Finsupp.linearCombination_single, Finsupp.single_eq_zero, ← map_smul,
    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at this

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

Goal state before:
pp: 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
hB : IsSymm B
x y : M
⊢ (RingHom.id R) ((B y) x) * (RingHom.id R) ((B y) x) = (RingHom.id R) ((B y) x) * (B y) x

Tactic:
RingHom.id_apply

Goal state after:
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
hB : IsSymm B
x y : M
⊢ (B y) x * (B y) x = (B y) x * (B y) x