mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: 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
⊢ IsPullback fst snd f g ↔ Nonempty (IsLimit (BinaryFan.mk fst snd))

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
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 : IsPullback fst snd f g
⊢ Nonempty (IsLimit (BinaryFan.mk fst snd))

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
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
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
m : M
s : ↥S
⊢ IsLocalization.mk' T 1 1 • mk m s = mk m s

Tactic:
rw [mk'_smul_mk, one_smul, one_mul]

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
P X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
⊢ IsPushout f g inl inr ↔ Nonempty (IsColimit (BinaryCofan.mk inl inr))

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Quiver.IsThin C
P X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
⊢ Nonempty (IsColimit (BinaryCofan.mk inl inr))

case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Quiver.IsThin C
P X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : Nonempty (IsColimit (BinaryCofan.mk inl inr))
⊢ IsPushout f g inl inr
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z Z' : C
f : X ⟶ Z
g : Y ⟶ Z'
i : Z ⟶ Z'
inst✝ : IsIso i
h : HasPullback f (g ≫ inv i)
⊢ HasPullback (f ≫ i) g

Tactic:
by simpa using hasPullback_of_comp_mono f (g ≫ inv i) i

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
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
p : LocalizedModule S M
⊢ (x + y) • p = x • p + y • p

Tactic:
induction p with | _ m s
  rw [smul_def T x, smul_def T y, mk_add_mk, show (x + y) • _ = IsLocalization.mk' T _ _ • _ by
    rw [← IsLocalization.mk'_sec (M := S) T x, ← IsLocalization.mk'_sec (M := S) T y,
      ← IsLocalization.mk'_add, IsLocalization.mk'_cancel _ _ s], mk'_smul_mk, ← smul_assoc,
    ← smul_assoc, ← add_smul]
  congr 1
  · simp only [Submonoid.smul_def, Submonoid.coe_mul, smul_eq_mul]; ring_nf
  · rw [mul_mul_mul_comm, mul_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
x✝ : IsSplitMono (T.η.app X)
⊢ retraction (T.η.app X) ≫ T.η.app X = T.η.app (T.obj X) ≫ T.map (retraction (T.η.app X))

Tactic:
← T.unit_naturality

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
x✝ : IsSplitMono (T.η.app X)
⊢ retraction (T.η.app X) ≫ T.η.app X = retraction (T.η.app X) ≫ T.η.app X
Module: Mathlib.CategoryTheory.Monad.Algebra

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : Comonad C
A B : G.Coalgebra
f : A ⟶ B
inst✝ : IsIso f.f
⊢ B.a ≫ G.map (inv f.f) = inv f.f ≫ A.a

Tactic:
IsIso.eq_inv_comp f.f,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : Comonad C
A B : G.Coalgebra
f : A ⟶ B
inst✝ : IsIso f.f
⊢ f.f ≫ B.a ≫ G.map (inv f.f) = A.a
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

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

Tactic:
exact this

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

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

Tactic:
exact this

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 a' : M
b b' : ↥S
⊢ f (b' • a + b • a') = ↑⋯.unit⁻¹ (f (↑(b * b') • a)) + ↑⋯.unit⁻¹ (↑(b * b') • f a')

Tactic:
map_add

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
b b' : ↥S
⊢ f (b' • a) + f (b • a') = ↑⋯.unit⁻¹ (f (↑(b * b') • a)) + ↑⋯.unit⁻¹ (↑(b * b') • f a')
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ (η.inv ≫ η.hom) = 𝟙 (F.map g)

Tactic:
Iso.inv_hom_id,

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ (𝟙 g) = 𝟙 (F.map g)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case one
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x)

Tactic:
exact ⟨op one, 𝟙 _, 𝟙 _, inferInstance, by simp⟩

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

Goal state before:
pp: case exists_of_eq
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 y : S
⊢ f.toLinearMap x = f.toLinearMap y → ∃ c, c • x = c • y

Tactic:
dsimp only [AlgHom.toLinearMap_apply]

Goal state after:
case exists_of_eq
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 y : S
⊢ f x = f y → ∃ c, c • x = c • y
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
inst✝¹ : IsPreconnected J
inst✝ : IsPreconnected K
⊢ IsPreconnected (J × K)

Tactic:
refine .of_any_functor_const_on_obj (fun {a} F ⟨j, k⟩ ⟨j', k'⟩ => ?_)
  exact (any_functor_const_on_obj (Prod.sectL J k ⋙ F) j j').trans
    (any_functor_const_on_obj (Prod.sectR j' K ⋙ F) k k')

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: case tail
X : Type u_1
a b b✝ c✝ : Discrete X
a✝ : Relation.ReflTransGen Zag a b✝
h : Zag b✝ c✝
eq : a.as = b✝.as
⊢ a.as = c✝.as

Tactic:
| tail _ h eq =>

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNoetherianRing R
h : FiniteType R A
⊢ FinitePresentation R A

Tactic:
obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.1 h

Goal state after:
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
⊢ FinitePresentation R A
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
X Y : C
⊢ ObjectProperty.Small.{w, v, u} (pair X Y)

Tactic:
dsimp [pair]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
⊢ ObjectProperty.Small.{w, v, u} (ofObj (Sum.elim (fun x ↦ X) fun x ↦ Y))
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
X : C
hX : P X
Y : C
hY : Q Y
e : X ≅ Y
⊢ isoClosure (fun X ↦ X ∈ Set.range (Subtype.val ∘ φ)) X

Tactic:
let Z : Subtype P' := ⟨Y, hY, ⟨X, hX, ⟨e.symm⟩⟩⟩

Goal state after:
case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
X : C
hX : P X
Y : C
hY : Q Y
e : X ≅ Y
Z : Subtype P' := ⟨Y, ⋯⟩
⊢ isoClosure (fun X ↦ X ∈ Set.range (Subtype.val ∘ φ)) X
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
α : Type u_1
P : α → ObjectProperty C
inst✝¹ : ∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)
inst✝ : Small.{w, u_1} α
h : ∀ (a : α), ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), P a ≤ Q.isoClosure
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), ⨆ a, P a ≤ Q.isoClosure

Tactic:
choose Q _ hQ using h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty C
inst✝¹ : ∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)
inst✝ : Small.{w, u_1} α
Q : α → ObjectProperty C
x✝ : ∀ (a : α), ObjectProperty.Small.{w, v, u} (Q a)
hQ : ∀ (a : α), P a ≤ (Q a).isoClosure
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), ⨆ a, P a ≤ Q.isoClosure
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: A : Type u_1
inst✝³ : Category.{v_1, u_1} A
B : Type u_2
inst✝² : Category.{v_2, u_2} B
T : Type u_3
inst✝¹ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
W : MorphismProperty T
X✝ : T
inst✝ : W.RespectsIso
X Y : Comma L R
e : X ≅ Y
h : commaObj L R W X
⊢ W (L.map e.hom.left ≫ Y.hom)

Tactic:
e.hom.w,

Goal state after:
A : Type u_1
inst✝³ : Category.{v_1, u_1} A
B : Type u_2
inst✝² : Category.{v_2, u_2} B
T : Type u_3
inst✝¹ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
W : MorphismProperty T
X✝ : T
inst✝ : W.RespectsIso
X Y : Comma L R
e : X ≅ Y
h : commaObj L R W X
⊢ W (X.hom ≫ R.map e.hom.right)
Module: Mathlib.CategoryTheory.Elements

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

Tactic:
fapply Functor.ext

Goal state after:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ ∀ (X : F₁.Elementsᵒᵖ),
    ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X

case h_map
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ autoParam
    (∀ (X Y : F₁.Elementsᵒᵖ) (f : X ⟶ Y),
      ((map α).op ⋙ toCostructuredArrow F₂).map f =
        eqToHom ⋯ ≫ (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ (F.map (e₁.hom ≫ e₁.inv)).toFunctor.obj X.fiber = X.fiber

Tactic:
e₁.hom_inv_id,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ (F.map (𝟙 X.base)).toFunctor.obj X.fiber = X.fiber
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
⊢ map (𝟙 F) = 𝟭 (Grothendieck F)

Tactic:
fapply Functor.ext

Goal state after:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
⊢ ∀ (X : Grothendieck F), (map (𝟙 F)).obj X = (𝟭 (Grothendieck F)).obj X

case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
⊢ autoParam
    (∀ (X Y : Grothendieck F) (f : X ⟶ Y), (map (𝟙 F)).map f = eqToHom ⋯ ≫ (𝟭 (Grothendieck F)).map f ≫ eqToHom ⋯)
    ext._auto_1
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
⊢ map (α ≫ β) = map α ⋙ map β

Tactic:
fapply Functor.ext

Goal state after:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
⊢ ∀ (X : Grothendieck F), (map (α ≫ β)).obj X = (map α ⋙ map β).obj X

case h_map
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
⊢ autoParam (∀ (X Y : Grothendieck F) (f : X ⟶ Y), (map (α ≫ β)).map f = eqToHom ⋯ ≫ (map α ⋙ map β).map f ≫ eqToHom ⋯)
    ext._auto_1
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫
      limit.π (pair X c.pt) { as := WalkingPair.left } =
    s.π.app j ≫ prod.fst

Tactic:
limit.lift_π

Goal state after:
case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ (BinaryFan.mk (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s))).π.app { as := WalkingPair.left } =
    s.π.app j ≫ prod.fst
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ (BinaryFan.mk (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s))).π.app { as := WalkingPair.left } =
    s.π.app j ≫ prod.fst

Tactic:
exact (nat_trans_from_is_connected (s.π ≫ γ₁ X) j (Classical.arbitrary _)).symm

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝ y✝ : WidePullbackShape J
x y : J
f : widePullbackShapeEquivObj (some x) ⟶ widePullbackShapeEquivObj (some y)
⊢ WidePullbackShape.Hom (some y) (some y) = (some x ⟶ some y)

Tactic:
by
        have eq : x = y := PLift.down (ULift.down (down f))
        rw [eq]
        rfl

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

Goal state before:
pp: case h₂
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ ((prod.functor.obj X).mapCone c).π.app j = s.π.app j
⊢ m ≫ prod.snd = prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫ prod.snd

Tactic:
limit.lift_π

Goal state after:
case h₂
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ ((prod.functor.obj X).mapCone c).π.app j = s.π.app j
⊢ m ≫ prod.snd =
    (BinaryFan.mk (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s))).π.app
      { as := WalkingPair.right }
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_4
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)
p₂ : RXn
hy✝ : p₂ ∈ adjoin R (Set.range MvPolynomial.X)
h₂ : p₂ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
x₁ : RXm
y₁ : RXn
hy₁ : y₁ ∈ (Ideal.span s').toAddSubmonoid
hx✝ : aeval_h.toRingHom x₁ + y₁ ∈ adjoin R (Set.range MvPolynomial.X)
h₁ : aeval_h.toRingHom x₁ + y₁ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
⊢ (aeval_h.toRingHom x₁ + y₁) * p₂ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid

Tactic:
obtain ⟨_, ⟨x₂, rfl⟩, y₂, hy₂, rfl⟩ := AddSubmonoid.mem_sup.mp h₂

Goal state after:
case refine_4
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)
x₁ : RXm
y₁ : RXn
hy₁ : y₁ ∈ (Ideal.span s').toAddSubmonoid
hx✝ : aeval_h.toRingHom x₁ + y₁ ∈ adjoin R (Set.range MvPolynomial.X)
h₁ : aeval_h.toRingHom x₁ + y₁ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
x₂ : RXm
y₂ : RXn
hy₂ : y₂ ∈ (Ideal.span s').toAddSubmonoid
hy✝ : aeval_h.toRingHom x₂ + y₂ ∈ adjoin R (Set.range MvPolynomial.X)
h₂ : aeval_h.toRingHom x₂ + y₂ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
⊢ (aeval_h.toRingHom x₁ + y₁) * (aeval_h.toRingHom x₂ + y₂) ∈
    aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
⊢ { l // l ≫ (Fork.ofι g ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = l }

Tactic:
obtain ⟨p, _, hp₂⟩ := PullbackCone.IsLimit.lift' t _ _ hl

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left✝ : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
⊢ { l // l ≫ (Fork.ofι g ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = l }
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Surjective ⇑f
hker : (RingHom.ker f.toRingHom).FG
⊢ f.FinitePresentation

Tactic:
convert! RingHom.FinitePresentation.of_surjective f hf hker

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

Goal state before:
pp: case refine_1.refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ f ≫ i = (f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S) ≫ 𝟙 S

Tactic:
← condition,

Goal state after:
case refine_1.refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ f ≫ i = (f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S) ≫ i
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_1.refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ g ≫ i = (g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S) ≫ 𝟙 S

Tactic:
← condition,

Goal state after:
case refine_1.refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ g ≫ i = (g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S) ≫ i