mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
x : R
hx : x ∈ span s
⊢ x ∈ span t

Tactic:
rw [mem_span_iff] at hx ⊢

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
x : R
hx : ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → x ∈ I
⊢ ∀ (I : TwoSidedIdeal R), t ⊆ ↑I → x ∈ I
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : IsLocalization M S
x : R
e : IsUnit x
inst✝ : Away x S
⊢ {x} ⊆ ↑(IsUnit.submonoid R)

Tactic:
Set.singleton_subset_iff

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : IsLocalization M S
x : R
e : IsUnit x
inst✝ : Away x S
⊢ x ∈ ↑(IsUnit.submonoid R)
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_1
S : Type u_4
T : Type u_5
inst✝² : CommRing S
inst✝¹ : CommRing T
inst✝ : Algebra S T
h₁ : Function.Surjective ⇑(algebraMap S T)
r : S
hr : IsUnit ((algebraMap S T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap S T) ≤ ⊥
t : T
⊢ ∃ n a, t * (algebraMap S T) r ^ n = (algebraMap S T) a

pp: case refine_2
S : Type u_4
T : Type u_5
inst✝² : CommRing S
inst✝¹ : CommRing T
inst✝ : Algebra S T
h₁ : Function.Surjective ⇑(algebraMap S T)
r : S
hr : IsUnit ((algebraMap S T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap S T) ≤ ⊥
x y : S
h : (algebraMap S T) x = (algebraMap S T) y
⊢ r ^ n * x = r ^ n * y

Tactic:
· obtain ⟨s, rfl⟩ := h₁ t
    exact ⟨0, by simp⟩

Goal state after:
case refine_2
S : Type u_4
T : Type u_5
inst✝² : CommRing S
inst✝¹ : CommRing T
inst✝ : Algebra S T
h₁ : Function.Surjective ⇑(algebraMap S T)
r : S
hr : IsUnit ((algebraMap S T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap S T) ≤ ⊥
x y : S
h : (algebraMap S T) x = (algebraMap S T) y
⊢ r ^ n * x = r ^ n * y
Module: Mathlib.RingTheory.Localization.Module

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
N : Type ?u.31
N' : Type ?u.33
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : AddCommMonoid N'
inst✝⁹ : Module R N
inst✝⁸ : Module R N'
g : N →ₗ[R] N'
inst✝⁷ : IsLocalizedModule S g
Rₛ : Type ?u.52
inst✝⁶ : CommSemiring Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : Module Rₛ N'
inst✝² : IsScalarTower R Rₛ M'
inst✝¹ : IsScalarTower R Rₛ N'
inst✝ : IsLocalization S Rₛ
e : M ≃ₗ[R] N
⊢ ↑R ((mapExtendScalars S f g Rₛ) ↑e ∘ₗ (mapExtendScalars S g f Rₛ) ↑e.symm) = ↑R LinearMap.id

Tactic:
apply IsLocalizedModule.linearMap_ext S g g

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
N : Type ?u.31
N' : Type ?u.33
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : AddCommMonoid N'
inst✝⁹ : Module R N
inst✝⁸ : Module R N'
g : N →ₗ[R] N'
inst✝⁷ : IsLocalizedModule S g
Rₛ : Type ?u.52
inst✝⁶ : CommSemiring Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : Module Rₛ N'
inst✝² : IsScalarTower R Rₛ M'
inst✝¹ : IsScalarTower R Rₛ N'
inst✝ : IsLocalization S Rₛ
e : M ≃ₗ[R] N
⊢ ↑R ((mapExtendScalars S f g Rₛ) ↑e ∘ₗ (mapExtendScalars S g f Rₛ) ↑e.symm) ∘ₗ g = ↑R LinearMap.id ∘ₗ g
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
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝³ : F.Monoidal
hF : F.FullyFaithful
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : F.obj X ⟶ F.obj Y
inst✝ : IsMonHom f
⊢ F.map (μ ≫ hF.preimage f) = F.map ((hF.preimage f ⊗ₘ hF.preimage f) ≫ μ)

Tactic:
by
    simp [← obj.μ_def_assoc, ← obj.μ_def, ← μ_natural_assoc, ← cancel_epi (LaxMonoidal.μ F ..)]

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

Goal state before:
pp: α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
h : α ≃ β
x : f α
⊢ ⇑h.symm <$> ⇑h <$> x = x

Tactic:
by simp [map_map]

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

Goal state before:
pp: α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
h : α ≃ β
x : f β
⊢ ⇑h <$> ⇑h.symm <$> x = x

Tactic:
by simp [map_map]

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
H :
  ∀ ⦃X Y Z : C⦄ (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    ∃ P inl inr, IsPushout f g inl inr ∧ IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
h✝ : HasColimit (span f g)
P : C
fst : X ⟶ P
snd : Y ⟶ P
h : IsPushout f g fst snd
h' : IsPushout (F.map f) (F.map g) (F.map fst) (F.map snd)
⊢ PreservesColimit (span f g) F

Tactic:
h.preservesColimit_span_iff

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
H :
  ∀ ⦃X Y Z : C⦄ (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    ∃ P inl inr, IsPushout f g inl inr ∧ IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
h✝ : HasColimit (span f g)
P : C
fst : X ⟶ P
snd : Y ⟶ P
h : IsPushout f g fst snd
h' : IsPushout (F.map f) (F.map g) (F.map fst) (F.map snd)
⊢ IsPushout (F.map f) (F.map g) (F.map fst) (F.map snd)
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_1
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) 1 = ↑n

Tactic:
use 1
      rw [map_one]
      norm_cast

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Quiver.IsThin C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : Nonempty (IsLimit (BinaryFan.mk fst snd))
⊢ IsPullback fst snd f g

Tactic:
exact ⟨⟨by subsingleton⟩,
      ⟨PullbackCone.IsLimit.mk _ (fun s ↦ BinaryFan.IsLimit.lift h.some s.fst s.snd)
      (by subsingleton) (by subsingleton) (by subsingleton)⟩⟩

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
inst✝ : Subsingleton α
x y : FreeRing α
⊢ x * y = (subsingletonEquivFreeCommRing α).symm ((subsingletonEquivFreeCommRing α) (y * x))

Tactic:
(subsingletonEquivFreeCommRing α).map_mul,

Goal state after:
α : Type u
inst✝ : Subsingleton α
x y : FreeRing α
⊢ x * y =
    (subsingletonEquivFreeCommRing α).symm ((subsingletonEquivFreeCommRing α) y * (subsingletonEquivFreeCommRing α) 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
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 : M''
⊢ ∃ x_1, x_1.2 • x = (↑e ∘ₗ f) x_1.1

Tactic:
obtain ⟨p, h⟩ := hf.surj (e.symm x)

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 : M''
p : M × ↥S
h : p.2 • e.symm x = f p.1
⊢ ∃ x_1, x_1.2 • x = (↑e ∘ₗ f) x_1.1
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
eq1 : (fromLocalizedModule S f) x = (fromLocalizedModule S f) y
⊢ x = y

Tactic:
by
  induction x with | _ a b
  induction y with | _ a' b'
  simp only [fromLocalizedModule_mk] at eq1
  rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← map_smul,
    Module.End.algebraMap_isUnit_inv_apply_eq_iff'] at eq1
  rw [LocalizedModule.mk_eq, ← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def,
    Submonoid.smul_def, f.map_smul, f.map_smul, eq1]

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''
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
x : M
⊢ (linearEquiv S f g) (f x) = g x

Tactic:
simp [linearEquiv]

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''
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
x : M
⊢ (linearEquiv S f g).symm (g x) = f x

Tactic:
simp [linearEquiv]

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
m : M
s₁ s₂ : ↥S
⊢ mk' f (s₂ • m) (s₁ * s₂) = mk' f m s₁

Tactic:
delta mk'
  rw [LocalizedModule.mk_cancel_common_right]

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

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ ((const J).obj { left := c₁.pt, right := c₂.pt, hom := (isLimitOfPreserves R t₂).lift (limitAuxiliaryCone F c₁) }).map
        t ≫
      { left := c₁.π.app j₂, right := c₂.π.app j₂, w := ⋯ } =
    { left := c₁.π.app j₁, right := c₂.π.app j₁, w := ⋯ } ≫ F.map t

Tactic:
by
        ext
        · simp [← c₁.w t]
        · simp [← c₂.w t]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst✝¹ : Algebra ↑R ↑A := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑B := (Hom.hom g).toAlgebra
e : ↑(of (↑A ⊗[↑R] ↑B)) ≃+* ↑X := (IsPushout.isoIsPushout A B ⋯ H).commRingCatIsoToRingEquiv
⊢ Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (Set.range ⇑((Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv).comp (ConcreteCategory.hom a)) ∪
        Set.range ⇑((Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv).comp (ConcreteCategory.hom b)))

Tactic:
rw [← hom_comp, ← hom_comp, IsPushout.inl_isoIsPushout_inv, IsPushout.inr_isoIsPushout_inv,
    hom_ofHom, hom_ofHom]

Goal state after:
R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst✝¹ : Algebra ↑R ↑A := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑B := (Hom.hom g).toAlgebra
e : ↑(of (↑A ⊗[↑R] ↑B)) ≃+* ↑X := (IsPushout.isoIsPushout A B ⋯ H).commRingCatIsoToRingEquiv
⊢ Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (Set.range ⇑Algebra.TensorProduct.includeLeftRingHom ∪ Set.range ⇑↑Algebra.TensorProduct.includeRight)
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F : J ⥤ Comma L R
inst✝ : PreservesColimit (F ⋙ fst L R) L
c₁ : Cocone (F ⋙ fst L R)
t₁ : IsColimit c₁
c₂ : Cocone (F ⋙ snd L R)
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ F.map t ≫ { left := c₁.ι.app j₂, right := c₂.ι.app j₂, w := ⋯ } =
    { left := c₁.ι.app j₁, right := c₂.ι.app j₁, w := ⋯ } ≫
      ((const J).obj
            { left := c₁.pt, right := c₂.pt,
              hom := (isColimitOfPreserves L t₁).desc (colimitAuxiliaryCocone F c₂) }).map
        t

Tactic:
by
        ext
        · simp [← c₁.w t]
        · simp [← c₂.w t]

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

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
inst✝ : HasColimitsOfShape J T
⊢ PreservesColimitsOfShape J leftFunc

Tactic:
apply Comma.preservesColimitsOfShape_fst

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
x : R
hJK : R ∙ x ≤ I.radical
n : ℕ
hn : x ^ n ∈ I
⊢ {x ^ n} ⊆ ↑I

Tactic:
Set.singleton_subset_iff

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
x : R
hJK : R ∙ x ≤ I.radical
n : ℕ
hn : x ^ n ∈ I
⊢ x ^ n ∈ ↑I
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: 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✝ : FinitePresentation R A
e : A ≃ₐ[R] B
⊢ FinitePresentation R B

Tactic:
by
  obtain ⟨n, f, hf⟩ := FinitePresentation.out (R := R) (A := A)
  use n, AlgHom.comp (↑e) f
  constructor
  · rw [AlgHom.coe_comp]
    exact Function.Surjective.comp e.surjective hf.1
  suffices (RingHom.ker (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom) = RingHom.ker f.toRingHom by
    rw [this]
    exact hf.2
  have hco : (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom = RingHom.comp (e.toRingEquiv : A ≃+* B)
    f.toRingHom := by
    have h : (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom =
      e.toAlgHom.toRingHom.comp f.toRingHom := rfl
    have h1 : ↑e.toRingEquiv = e.toAlgHom.toRingHom := rfl
    rw [h, h1]
  rw [RingHom.ker_eq_comap_bot, hco, ← Ideal.comap_comap, ← RingHom.ker_eq_comap_bot,
    RingHom.ker_coe_equiv (AlgEquiv.toRingEquiv e), RingHom.ker_eq_comap_bot]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
⊢ EssentiallySmall.{w, v, u} C ↔ ObjectProperty.EssentiallySmall.{w, v, u} ⊤

Tactic:
by
  rw [← exists_equivalence_iff_of_locallySmall]
  exact ⟨fun _ ↦ ⟨_, _, ⟨equivSmallModel.{w} C⟩⟩,
    fun ⟨C₀, _, ⟨e⟩⟩ ↦ ⟨C₀, inferInstance, ⟨e⟩⟩⟩

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

Goal state before:
pp: case h.some
J : Type v₁
p : Set (WidePushoutShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
val✝ : J
⊢ some val✝ ∈ p

Tactic:
· rwa [← t (WidePushoutShape.Hom.init _)]

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hg : (g.comp f).FinitePresentation
hf : f.FiniteType
⊢ g.FinitePresentation

Tactic:
algebraize [f, g, g.comp f]
  exact Algebra.FinitePresentation.of_restrict_scalars_finitePresentation A B C

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 : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
⊢ (F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber ⟶
    ((pre F G).obj { base := c, fiber := (F.map g).toFunctor.obj f }).fiber

Tactic:
by exact 𝟙 _

Goal state after:
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
⊢ (map α).Final

Tactic:
let α' : F' ⟶ G' := whiskerLeft _ (whiskerRight α _)

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)
⊢ (map α).Final
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: 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
⊢ CostructuredArrow P.ι d

Tactic:
by exact CostructuredArrow.mk (Y := ⟨d, hd⟩) (𝟙 _)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
Z : C
l' : Z ⟶ (IsPullback.cone h).pt
e : (l' ≫ (IsPullback.cone h).fst) ≫ f = (l' ≫ (IsPullback.cone h).snd) ≫ f
⊢ l' ≫ (IsPullback.cone h).fst = l' ≫ (IsPullback.cone h).snd

Tactic:
rw [IsPullback.cone_fst, h₂]

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.IsStableUnderBaseChange → P.pullbacks ≤ P

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.pullbacks ≤ P → P.IsStableUnderBaseChange

Tactic:
· intro h _ _ _ ⟨_, _, _, _, _, h₁, h₂⟩
    exact of_isPullback h₂ h₁

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.pullbacks ≤ P → P.IsStableUnderBaseChange
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
inst✝ : HasPullback i₁ i₂
⊢ (fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f =
    map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯ ≫
      map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯

Tactic:
ext <;> simp [condition_assoc]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
P Q : ObjectProperty C
inst✝² : P.ContainsZero
inst✝¹ : Q.ContainsZero
inst✝ : Q.IsClosedUnderIsomorphisms
⊢ ∃ Z, IsZero Z ∧ (P ⊓ Q) Z

Tactic:
by
    obtain ⟨Z, hZ, hP⟩ := P.exists_prop_of_containsZero
    exact ⟨Z, hZ, hP, Q.prop_of_isZero hZ⟩

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₃
⊢ lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯ ≫ fst (fst f' g') i₁ =
    lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯ ≫ fst (snd f' g') i₂

Tactic:
by rw [lift_fst, lift_fst]

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

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

Tactic:
have : HasColimit X₂ := ⟨c₂, hc₂⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasCoproduct X₁] [inst_1 : HasCoproduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Sigma.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j ↦ f.app { as := j }
this✝ : HasColimit X₁
this : HasColimit X₂
⊢ W α
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_4.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
m : c.pt ⟶ pullback (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ (m ≫ snd (fst f g) (fst f h)) ≫ fst f h =
    (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ snd (fst f g) (fst f h)) ≫ fst f h

Tactic:
simp [← hsnd, pullback.condition, ← hfst]

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

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
m : c.pt ⟶ pullback (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ (m ≫ snd (fst f g) (fst f h)) ≫ snd f h =
    (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ snd (fst f g) (fst f h)) ≫ snd f h

Tactic:
simp [← hsnd, pullback.condition, ← hfst]

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
inst✝ : BraidedCategory C
M N : Mon C
⊢ { hom := snd M.X N.X, isMonHom_hom := ⋯ }.hom =
    ((IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from M ▷ N ≫ (λ_ N).hom).hom

Tactic:
simp [snd_def]

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
inst✝ : BraidedCategory C
M N : Mon C
⊢ isTerminalTensorUnit.from M.X ▷ N.X =
    ((IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from M).hom ▷ N.X
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X : C
⊢ (λ_ X).hom = snd (𝟙_ C) X

Tactic:
simp [snd_def]

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 : C
⊢ (λ_ X).inv ≫ snd (𝟙_ C) X = 𝟙 X

Tactic:
simp [snd_def]

Goal state after: