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

Goal state before:
pp: case h.h
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
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : (fromLocalizedModule S f) (LocalizedModule.mk a b) = (fromLocalizedModule S f) (LocalizedModule.mk a' b')
⊢ LocalizedModule.mk a b = LocalizedModule.mk a' b'

Tactic:
simp only [fromLocalizedModule_mk] at eq1

Goal state after:
case h.h
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
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : ↑⋯.unit⁻¹ (f a) = ↑⋯.unit⁻¹ (f a')
⊢ LocalizedModule.mk a b = LocalizedModule.mk a' b'
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ ↑(Algebra.TensorProduct.liftEquiv.symm { hom' := m }.hom.toIntAlgHom) =
    ↑(Algebra.TensorProduct.liftEquiv.symm
        (Hom.hom
            (ofHom
              (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                  ⋯).toRingHom)).toIntAlgHom)

Tactic:
rw [Algebra.TensorProduct.liftEquiv_symm_apply_coe, Prod.mk.injEq]

Goal state after:
A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ { hom' := m }.hom.toIntAlgHom.comp Algebra.TensorProduct.includeLeft =
      (Algebra.TensorProduct.liftEquiv.symm
            (Hom.hom
                (ofHom
                  (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                      ⋯).toRingHom)).toIntAlgHom).1.1 ∧
    (AlgHom.restrictScalars ℤ { hom' := m }.hom.toIntAlgHom).comp Algebra.TensorProduct.includeRight =
      (Algebra.TensorProduct.liftEquiv.symm
            (Hom.hom
                (ofHom
                  (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                      ⋯).toRingHom)).toIntAlgHom).1.2
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case left
A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
a : ↑A
⊢ ({ hom' := m }.hom.toIntAlgHom.comp Algebra.TensorProduct.includeLeft) a =
    (Algebra.TensorProduct.liftEquiv.symm
            (Hom.hom
                (ofHom
                  (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                      ⋯).toRingHom)).toIntAlgHom).1.1
      a

Tactic:
simp [map_one, mul_one, ← hm (Discrete.mk WalkingPair.left)]

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
M₁ : Type u_6
M₂ : Type u_7
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
y : M₂
y' : M
s : ↥S₂
e : (y', s).2 • y = f₂ (y', s).1
⊢ (f₁ y', s).2 • y = (liftOfLE S₁ S₂ h f₁ f₂) (f₁ y', s).1

Tactic:
simpa

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
N : Type u_6
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
h_inj : Function.Injective ⇑h
x : M
s : ↥S
y : M
t : ↥S
c : R
hc : c ∈ S
e : c • s • h y = c • t • h x
⊢ h (c • s • y) = h (c • t • x)

Tactic:
simpa

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

Goal state before:
pp: case map_units.left
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
⊢ Function.Injective ⇑((algebraMap R (End R S')) ↑x)

pp: case map_units.right
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
⊢ Function.Surjective ⇑((algebraMap R (End R S')) ↑x)

Tactic:
· rintro a b (e : x • a = x • b)
      simp_rw [Submonoid.smul_def, Algebra.smul_def] at e
      exact (h₁ x x.2).mul_left_cancel e

Goal state after:
case map_units.right
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
⊢ Function.Surjective ⇑((algebraMap R (End R S')) ↑x)
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
inst✝ : Subsingleton M
⊢ Subsingleton M'

Tactic:
rw [subsingleton_iff S g]
  intro m
  use 1
  simp [one_mem, Subsingleton.elim m 0]

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
⊢ (R ∙ x) ^ n ≤ I

Tactic:
← span,

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
⊢ span {x} ^ n ≤ I
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ (ιOfLE ⋯).IsEquivalence

Tactic:
rw [isEquivalence_ιOfLE_iff]

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
⊢ ObjectProperty.Small.{w, v, u} P.op

Tactic:
simpa

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
⊢ ObjectProperty.Small.{w, v, u} P.unop

Tactic:
simpa

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.EssentiallySmall.{w, v, u} P
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.op

Tactic:
simpa

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.EssentiallySmall.{w, v, u} P
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.unop

Tactic:
simpa

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝ : LocallySmall.{w, v_1, u_1} C
H₁ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} F.essImage
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v_1, u_1} fun x ↦ Nonempty (F.obj x ≅ Y)
⊢ ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v_1, u_1} (⊤ ⊓ fun x ↦ Nonempty (F.obj x ≅ Y))

Tactic:
simpa

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
h : X = Y
⊢ (F.map (eqToHom h).base).toFunctor.obj X.fiber = Y.fiber

Tactic:
by subst h; simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x✝ : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
⊢ (G.map { base := f, fiber := g } ≫ colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) ≫ c.ι.app Y.base =
    (G.map ((Grothendieck.ιNatTrans f).app X.fiber ≫ (Grothendieck.ι F Y.base).map g) ≫
        colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) ≫
      c.ι.app Y.base

Tactic:
congr <;> 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 ⥤ Type w
⊢ ∀ {X Y : Grothendieck (G ⋙ typeToCat)} (f : X ⟶ Y),
    (𝟭 (Grothendieck (G ⋙ typeToCat))).map f ≫
        (casesOn Y fun base fiber ↦
            Discrete.casesOn fiber fun as ↦
              Iso.refl ((𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base, fiber := { as := as } })).hom =
      (casesOn X fun base fiber ↦
            Discrete.casesOn fiber fun as ↦
              Iso.refl ((𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base, fiber := { as := as } })).hom ≫
        (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).map f

Tactic:
rintro ⟨_, ⟨⟩⟩ ⟨_, ⟨⟩⟩ ⟨base, ⟨⟨f⟩⟩⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
base✝¹ : C
as✝¹ : G.obj base✝¹
base✝ : C
as✝ : G.obj base✝
base : { base := base✝¹, fiber := { as := as✝¹ } }.base ⟶ { base := base✝, fiber := { as := as✝ } }.base
f :
  (((G ⋙ typeToCat).map base).toFunctor.obj { base := base✝¹, fiber := { as := as✝¹ } }.fiber).as =
    { base := base✝, fiber := { as := as✝ } }.fiber.as
⊢ (𝟭 (Grothendieck (G ⋙ typeToCat))).map { base := base, fiber := { down := { down := f } } } ≫
      (casesOn { base := base✝, fiber := { as := as✝ } } fun base fiber ↦
          Discrete.casesOn fiber fun as ↦
            Iso.refl ((𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base, fiber := { as := as } })).hom =
    (casesOn { base := base✝¹, fiber := { as := as✝¹ } } fun base fiber ↦
          Discrete.casesOn fiber fun as ↦
            Iso.refl ((𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base, fiber := { as := as } })).hom ≫
      (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).map
        { base := base, fiber := { down := { down := f } } }
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case of.star.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (starTerminal.from (incl.obj x)) ≫ hG.hom = h.hom.app x ≫ M x
X : C
⊢ G.map PUnit.unit ≫
      (match star with
        | of x => h.app x
        | star => hG).hom =
    (match of X with
        | of x => h.app x
        | star => hG).hom ≫
      (lift F M hM).map PUnit.unit

Tactic:
exact hh _

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_1
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i - (MvPolynomial.aeval h) (g i) + (MvPolynomial.aeval h) (g i) ∈
    aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid

Tactic:
add_comm

Goal state after:
case refine_1
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
i : Fin n
⊢ (MvPolynomial.aeval h) (g i) + (MvPolynomial.X i - (MvPolynomial.aeval h) (g i)) ∈
    aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin 0) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ Ideal.comap (↑(MvPolynomial.isEmptyRingEquiv R (Fin 0)).symm) (ker g') =
    Ideal.map (↑(MvPolynomial.isEmptyRingEquiv R (Fin 0))) (ker g')

Tactic:
exact Ideal.comap_symm (MvPolynomial.isEmptyRingEquiv R (Fin 0))

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
⊢ IsLimit (PullbackCone.mk a b ⋯)

Tactic:
by
      refine PullbackCone.isLimitAux _
        (fun s => small_k.lift s.fst s.snd (by rw [← cancel_mono f₂, assoc, s.condition, assoc]))
        (by simp) (by simp) ?_
      intro s m hm
      apply small_k.isLimit.hom_ext
      apply PullbackCone.equalizer_ext small_k.cone _ _
      · exact (hm WalkingCospan.left).trans (by simp)
      · exact (hm WalkingCospan.right).trans (by simp)

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
t : (PullbackCone.mk r.left r.right ⋯).pt ⟶ (IsPullback.cone k).pt :=
  (IsPullback.isLimit k).lift (PullbackCone.mk r.left r.right ⋯)
ht : t ≫ a = r.left
kt : t ≫ b = r.right
s : Cofork a b
m : (Cofork.ofπ f ⋯).pt ⟶ s.pt
w : (Cofork.ofπ f ⋯).π ≫ m = s.π
⊢ m = Cofork.IsColimit.desc r.isColimit s.π ⋯

Tactic:
apply Cofork.IsColimit.hom_ext r.isColimit

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
t : (PullbackCone.mk r.left r.right ⋯).pt ⟶ (IsPullback.cone k).pt := ⋯
ht : t ≫ a = r.left
kt : t ≫ b = r.right
s : Cofork a b
m : (Cofork.ofπ f ⋯).pt ⟶ s.pt
w : (Cofork.ofπ f ⋯).π ≫ m = s.π
⊢ (Cofork.ofπ f ⋯).π ≫ m = (Cofork.ofπ f ⋯).π ≫ Cofork.IsColimit.desc r.isColimit s.π ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: 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)
⊢ pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯ ≫ pullback.fst f g =
    pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯ ≫ pullback.fst f g

Tactic:
pullback.lift_fst,

Goal state after:
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)
⊢ pullback.fst f (a₁ ≫ g) ≫ 𝟙 X = pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯ ≫ pullback.fst f g
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ X Y : C
f : X ⟶ Y
inst✝ : IsRegularEpi f
⊢ IsRegularMono f.op

Tactic:
simpa

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : IsRegularEpi f
⊢ IsRegularMono f.unop

Tactic:
simpa

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ X Y : C
f : X ⟶ Y
inst✝ : IsRegularMono f
⊢ IsRegularEpi f.op

Tactic:
simpa

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : IsRegularMono f
⊢ IsRegularEpi f.unop

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
e : R' →+* S' := (↑e₂).comp ((IsLocalization.map (Localization.Away (f r)) f ⋯).comp ↑e₁)
⊢ e = IsLocalization.Away.map R' S' f r

Tactic:
apply IsLocalization.ringHom_ext (Submonoid.powers r) _

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := ⋯
e₂ : Localization.Away (f r) ≃+* S' := ⋯
e : R' →+* S' := ⋯
⊢ e.comp (algebraMap R R') = (IsLocalization.Away.map R' S' f r).comp (algebraMap R R')
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Q (algebraMap R S) → P (algebraMap S (S ⊗[R] T)) → P (algebraMap R T)
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
e : R' ⊗[R] S ≃ₐ[R'] S' := ⋯
this : (↑e.symm).comp (algebraMap R' S') = algebraMap R' (R' ⊗[R] S)
⊢ P (algebraMap R' (R' ⊗[R] S))

Tactic:
← this

Goal state after:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Q (algebraMap R S) → P (algebraMap S (S ⊗[R] T)) → P (algebraMap R T)
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
e : R' ⊗[R] S ≃ₐ[R'] S' := Algebra.IsPushout.equiv R R' S S'
this : (↑e.symm).comp (algebraMap R' S') = algebraMap R' (R' ⊗[R] S)
⊢ P ((↑e.symm).comp (algebraMap R' S'))
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
Q : ObjectProperty C
h : P ≤ Q
F : J ⥤ C
inst✝ : HasLimit F
hF : ∀ (j : J), P (F.obj j)
⊢ Q.strictLimitsOfShape J (limit F)

Tactic:
exact ⟨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
X✝ Y✝ Z : 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:
pullback.lift_fst,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : 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₂ = lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯ ≫ fst (snd f' g') i₂