mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.π F i ≫ eqToHom ⋯ = 𝟙 (limit F) ≫ limit.π F i

Tactic:
id_comp,

Goal state after:
case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.π F i ≫ eqToHom ⋯ = limit.π F i
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: 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
e : M ≅ X
⊢ IsMonHom e.hom

Tactic:
let := MonObj.ofIso e

Goal state after:
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
e : M ≅ X
this : MonObj X := MonObj.ofIso e
⊢ IsMonHom e.hom
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| ((λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η) ⊗ₘ η) ≫ (α_ M N P).hom

Tactic:
rw [← Category.id_comp (η : 𝟙_ C ⟶ P), ← tensorHom_comp_tensorHom]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| (((λ_ (𝟙_ C)).inv ⊗ₘ 𝟙 (𝟙_ C)) ≫ ((η ⊗ₘ η) ⊗ₘ η)) ≫ (α_ M N P).hom
Module: Mathlib.CategoryTheory.Monoidal.Mon

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

Tactic:
simp only [comp_whiskerRight_assoc, whiskerLeft_comp_assoc]
  slice_lhs 2 3 => rw [tensorμ_natural_left]
  slice_lhs 3 4 => rw [tensorHom_comp_tensorHom, mul_assoc, mul_assoc, ← tensorHom_comp_tensorHom,
    ← tensorHom_comp_tensorHom]
  slice_lhs 1 3 => rw [tensor_associativity]
  slice_lhs 3 4 => rw [← tensorμ_natural_right]
  simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
⊢ (α_ X Y (X ⊗ Y)).hom ≫
      X ◁ (α_ Y X Y).inv ≫
        X ◁ (β_ Y X).hom ▷ Y ≫
          X ◁ (β_ X Y).hom ▷ Y ≫
            (α_ X (Y ⊗ X) Y).inv ≫
              (α_ X Y X).inv ▷ Y ≫
                (β_ X Y).hom ▷ X ▷ Y ≫
                  (α_ (Y ⊗ X) X Y).hom ≫
                    (α_ Y X (X ⊗ Y)).hom ≫
                      Y ◁ X ◁ (β_ X Y).hom ≫
                        Y ◁ (α_ X Y X).inv ≫
                          Y ◁ (β_ X Y).hom ▷ X ≫ Y ◁ (α_ Y X X).hom ≫ (α_ Y Y (X ⊗ X)).inv ≫ (μ ⊗ₘ μ) =
    ((β_ X Y).hom ⊗ₘ (β_ X Y).hom) ≫
      (α_ Y X (Y ⊗ X)).hom ≫
        Y ◁ (α_ X Y X).inv ≫ Y ◁ (β_ X Y).hom ▷ X ≫ Y ◁ (α_ Y X X).hom ≫ (α_ Y Y (X ⊗ X)).inv ≫ (μ ⊗ₘ μ)

Tactic:
slice_lhs 3 4 =>
    -- We use symmetry here:
    rw [← whiskerLeft_comp, ← comp_whiskerRight, SymmetricCategory.symmetry]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
⊢ (α_ X Y (X ⊗ Y)).hom ≫
      X ◁ (α_ Y X Y).inv ≫
        ((((((((((X ◁ 𝟙 (Y ⊗ X) ▷ Y ≫ (α_ X (Y ⊗ X) Y).inv) ≫ (α_ X Y X).inv ▷ Y) ≫ (β_ X Y).hom ▷ X ▷ Y) ≫
                        (α_ (Y ⊗ X) X Y).hom) ≫
                      (α_ Y X (X ⊗ Y)).hom) ≫
                    Y ◁ X ◁ (β_ X Y).hom) ≫
                  Y ◁ (α_ X Y X).inv) ≫
                Y ◁ (β_ X Y).hom ▷ X) ≫
              Y ◁ (α_ Y X X).hom) ≫
            (α_ Y Y (X ⊗ X)).inv) ≫
          (μ ⊗ₘ μ) =
    ((β_ X Y).hom ⊗ₘ (β_ X Y).hom) ≫
      (α_ Y X (Y ⊗ X)).hom ≫
        Y ◁ (α_ X Y X).inv ≫ Y ◁ (β_ X Y).hom ▷ X ≫ Y ◁ (α_ Y X X).hom ≫ (α_ Y Y (X ⊗ X)).inv ≫ (μ ⊗ₘ μ)
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_1
inst✝¹⁸ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁷ : CommSemiring A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : IsLocalization S A
M : Type u_3
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
M' : Type u_4
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : Module A M'
inst✝⁹ : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst✝⁸ : CommSemiring T
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R T B
inst✝¹ : IsScalarTower R A B
α : Type u_7
inst✝ : IsLocalizedModule S f
e : Localization S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LocalizedModule.equivTensorProduct S M).symm ≪≫ₗ IsLocalizedModule.iso S f
e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  finsuppRight R R (Localization S) M α ≪≫ₗ Finsupp.mapRange.linearEquiv e
a : α
m : M
b : α
this : (if a = b then f m else 0) = e (1 ⊗ₜ[R] if a = b then m else 0)
⊢ e
      (((finsuppRight R R (Localization S) M α) (((↑e'.symm ∘ₗ Finsupp.mapRange.linearMap f) ∘ₗ Finsupp.lsingle a) m))
        b) =
    e (((finsuppRight R R (Localization S) M α) (((mk R (Localization S) (α →₀ M)) 1 ∘ₗ Finsupp.lsingle a) m)) b)

Tactic:
by
    simpa [e', Finsupp.single_apply, -EmbeddingLike.apply_eq_iff_eq, apply_ite]

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
x : Localization M
⊢ (tensorLeftAlgEquiv M S) (1 ⊗ₜ[R] x) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M))) x

Tactic:
by
  let Rₘ := Localization M
  let Sₘ := Localization (Algebra.algebraMapSubmonoid S M)
  obtain ⟨x, y, rfl⟩ := IsLocalization.exists_mk'_eq M x
  let : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
  have h1 : (1 : S) ⊗ₜ[R] IsLocalization.mk' Rₘ x y = algebraMap _ _ (IsLocalization.mk' Rₘ x y) :=
    rfl
  rw [h1, tensorLeftAlgEquiv, algEquiv_symm_apply,
    IsLocalization.algebraMap_mk' S, IsLocalization.map_mk', IsLocalization.mk'_eq_iff_eq_mul]
  simp_rw [RingHom.id_apply]
  have h x : algebraMap S Sₘ ((algebraMap R S) x) = algebraMap Rₘ Sₘ ((algebraMap R Rₘ) x) := by
    rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]
  rw [h, h, ← map_mul, IsLocalization.mk'_spec]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ IsPullback (F.map f) (F.map g) (F.map h) (F.map i)

Tactic:
refine
    IsPullback.of_isLimit' (F.map_commSq s.toCommSq)
      (IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext ?_ ?_ ?_)
        (isLimitOfPreserves F s.isLimit))
  · rfl
  · simp
  · simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Quiver.IsThin C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : Quiver.IsThin D
F : C ⥤ D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
hfg : HasPullback f g
⊢ Nonempty (IsLimit (BinaryFan.mk (pullback.fst f g) (pullback.snd f g)))

Tactic:
rw [← CategoryTheory.isPullback_iff_isLimit_binaryFan_of_isThin (f := f) (g := g)]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Quiver.IsThin C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : Quiver.IsThin D
F : C ⥤ D
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
hfg : HasPullback f g
⊢ IsPullback (pullback.fst f g) (pullback.snd f g) f g
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_s
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ (IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t) =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)

Tactic:
· rw [mul_mul_mul_comm]

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

Goal state before:
pp: 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
a : R
s : ↥S
⊢ (algebraMap T (LocalizedModule S A)) (IsLocalization.mk' T a s) = mk ((algebraMap R A) a) s

Tactic:
with_unfolding_all
  rw [Algebra.algebraMap_eq_smul_one]
  change _ • mk _ _ = _
  rw [mk'_smul_mk, Algebra.algebraMap_eq_smul_one, mul_one]

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 ⥤ D
X : Cᵒᵖ
t : (F.op ⋙ (cones J D).obj K).obj X
j j' : J
f : j ⟶ j'
⊢ (unop ((const J).op.obj X)).map f ≫ (adj.homEquiv (unop X) (K.obj j')) (t.app j') =
    (adj.homEquiv (unop X) (K.obj j)) (t.app j) ≫ (K ⋙ G).map f

Tactic:
← adj.homEquiv_naturality_right,

Goal state after:
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 ⥤ D
X : Cᵒᵖ
t : (F.op ⋙ (cones J D).obj K).obj X
j j' : J
f : j ⟶ j'
⊢ (unop ((const J).op.obj X)).map f ≫ (adj.homEquiv (unop X) (K.obj j')) (t.app j') =
    (adj.homEquiv ((unop ((const J).op.obj X)).obj j) (K.obj j')) (t.app j ≫ K.map f)
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
x₁✝ x₂✝ : M''
h : (f ∘ₗ ↑e) x₁✝ = (f ∘ₗ ↑e) x₂✝
⊢ ∃ c, c • x₁✝ = c • x₂✝

Tactic:
simp_rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply] at h

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
x₁✝ x₂✝ : M''
h : f (e x₁✝) = f (e x₂✝)
⊢ ∃ c, c • x₁✝ = c • x₂✝
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPushoutsAlong f
x : Under X
y : Under Y
u : (pushout f).obj x ⟶ y
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ y.hom

Tactic:
← Under.w u

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPushoutsAlong f
x : Under X
y : Under Y
u : (pushout f).obj x ⟶ y
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ ((pushout f).obj x).hom ≫ Hom.right u
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ ofHom
        ((RingHom.fst ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) ≫
      f =
    ofHom
        ((RingHom.snd ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) ≫
      g

Tactic:
by
      ext ⟨x, e⟩
      simpa [CommRingCat.ofHom] using e

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
⊢ (∀ ⦃x : M⦄, True → ∃ r ∈ S, r • x = 0) ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0

Tactic:
true_implies

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ F.map₂ (λ_ f).inv = (λ_ (F.map f)).inv ≫ (F.mapId a✝).inv ▷ F.map f ≫ (F.mapComp (𝟙 a✝) f).inv

Tactic:
by
    rw [← F.map₂Iso_inv, eq_inv_comp, comp_inv_eq]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ F.map₂ (ρ_ f).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b✝).inv ≫ (F.mapComp f (𝟙 b✝)).inv

Tactic:
by
    rw [← F.map₂Iso_inv, eq_inv_comp, comp_inv_eq]
    simp

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
inst✝¹ : CommRing R
ι : Type u_1
inst✝ : Finite ι
⊢ ∃ n f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

Tactic:
by
    cases nonempty_fintype ι
    let eqv := (MvPolynomial.renameEquiv R <| Fintype.equivFin ι).symm
    exact
      ⟨Fintype.card ι, eqv, eqv.surjective,
        ((RingHom.injective_iff_ker_eq_bot _).1 eqv.injective).symm ▸ Submodule.fg_bot⟩

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case intro.refine_1
R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ⇑f
hf_ker : (RingHom.ker f.toRingHom).FG
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A := (MvPolynomial.mapAlgHom f).comp ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ (RingHom.ker ↑↑(MvPolynomial.sumAlgEquiv R ι ι')).FG

Tactic:
rw [AlgEquiv.toAlgHom_toRingHom, AlgHom.ker_coe_equiv]

Goal state after:
case intro.refine_1
R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ⇑f
hf_ker : (RingHom.ker f.toRingHom).FG
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A := (MvPolynomial.mapAlgHom f).comp ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ ⊥.FG
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f g : X ⟶ Y
h : f = g
⊢ f.fiber = eqToHom ⋯ ≫ g.fiber

Tactic:
subst h
  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
G : C ⥤ Cat
H : C ⥤ Cat
X✝ Y✝ Z✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { base := (x✝¹ ≫ x✝).base, fiber := AsSmall.down.map (x✝¹ ≫ x✝).fiber } =
    { base := x✝¹.base, fiber := AsSmall.down.map x✝¹.fiber } ≫ { base := x✝.base, fiber := AsSmall.down.map x✝.fiber }

Tactic:
apply Grothendieck.ext <;> simp [down_comp]

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
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X Y : C
f : X ⟶ Y
x✝² x✝¹ : ↑(F.obj X)
x✝ : x✝² ⟶ x✝¹
⊢ { base := 𝟙 X, fiber := eqToHom ⋯ ≫ x✝ } ≫ { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x✝¹) } =
    { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x✝²) } ≫
      { base := 𝟙 Y, fiber := eqToHom ⋯ ≫ (F.map f).toFunctor.map x✝ }

Tactic:
exact Grothendieck.ext _ _ (by simp) (by simp [eqToHom_map])

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

Goal state before:
pp: case h.zero
p : Set WalkingParallelPair
a✝ : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ WalkingParallelPair.zero ∈ p

pp: case h.one
p : Set WalkingParallelPair
a✝ : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ WalkingParallelPair.one ∈ p

Tactic:
· rwa [t WalkingParallelPairHom.left]

Goal state after:
case h.one
p : Set WalkingParallelPair
a✝ : WalkingParallelPair.one ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ WalkingParallelPair.one ∈ p
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
inst✝ : HasColimit G
X : C
⊢ colimit.ι (F ⋙ G) X ≫ (colimitIso F G).hom = colimit.ι G (F.obj X)

Tactic:
by
  simp [colimitIso]

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
inst✝ : HasColimit G
X : C
⊢ colimit.ι G (F.obj X) ≫ (colimitIso F G).inv = colimit.ι (F ⋙ G) X

Tactic:
by
  simp [colimitIso]

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsColimit (Cofork.ofπ f.unop ⋯)
⊢ (Iso.refl (Opposite.op (Opposite.unop Y))).hom ≫ pushout.inl f f =
    (pullback.fst f.unop f.unop).op ≫ (pushoutIsoOpPullback f f).symm.hom

pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsColimit (Cofork.ofπ f.unop ⋯)
⊢ (Iso.refl (Opposite.op (Opposite.unop Y))).hom ≫ pushout.inr f f =
    (pullback.snd f.unop f.unop).op ≫ (pushoutIsoOpPullback f f).symm.hom

Tactic:
· rw [Iso.symm_hom, ← Quiver.Hom.op_unop (pushoutIsoOpPullback f f).inv, ← op_comp,
        pushoutIsoOpPullback_inv_fst, Quiver.Hom.op_unop, Iso.refl_hom, Category.id_comp]

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsColimit (Cofork.ofπ f.unop ⋯)
⊢ (Iso.refl (Opposite.op (Opposite.unop Y))).hom ≫ pushout.inr f f =
    (pullback.snd f.unop f.unop).op ≫ (pushoutIsoOpPullback f f).symm.hom
Module: Mathlib.CategoryTheory.Limits.Final

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

Tactic:
have : ∀ X, Final (α'.app X).toFunctor := fun X =>
    inferInstanceAs (AsSmall.equiv.inverse ⋙ _ ⋙ AsSmall.equiv.functor).Final

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

Goal state before:
pp: case refine_4
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
      (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯)
          ⋯).snd =
    s.snd

pp: case refine_5
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
m : s.pt ⟶ pullback f (a₁ ≫ g)
hm :
  ∀ (j : WalkingCospan),
    m ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
                (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).π.app
          j =
      s.π.app j
⊢ m = pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯

Tactic:
· ext
    · simp [s.condition]
    · simp

Goal state after:
case refine_5
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
m : s.pt ⟶ pullback f (a₁ ≫ g)
hm :
  ∀ (j : WalkingCospan),
    m ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
                (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).π.app
          j =
      s.π.app j
⊢ m = pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯
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
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i =
    snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯ ≫ snd f f

Tactic:
pullback.lift_snd

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i =
    snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₂ ≫ fst f i
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
J : Type u_2
inst✝ : Category.{v_2, u_2} J
⊢ W₁.limitsOfShape J ≤ W₂.limitsOfShape J

Tactic:
rintro _ _ _ ⟨_, _, _, _, h₁, _, f, hf⟩
  exact ⟨_, _, _, _, h₁, _, f, fun j ↦ h _ (hf j)⟩

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 S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ map f g f' g' i₁ i₂ i₃ e₁ e₂ =
    (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv ≫
      snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ fst (snd f' g') i₂

Tactic:
simp only [pullbackFstFstIso_inv, lift_snd_assoc, lift_fst]

Goal state after: