mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: case e'_3
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry ((mk S (A ⊗[R] B) S).flip 1)) x) y =
    (TensorProduct.rid S (A ⊗[R] B)).symm
      ((TensorProduct.rid S A) (x ⊗ₜ[S] 1) ⊗ₜ[R] (TensorProduct.rid R B) (y ⊗ₜ[R] 1))

Tactic:
· dsimp
      simp only [one_smul]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
p x : R
hp : p = 0 ∨ Irreducible p
hnorm : normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
⊢ count p (normalizedFactors x) = n

Tactic:
rcases hp with (rfl | hp)
  · cases n
    · exact count_eq_zero.2 (zero_notMem_normalizedFactors _)
    · rw [zero_pow (Nat.succ_ne_zero _)] at hle hlt
      exact absurd hle hlt
  · exact count_normalizedFactors_eq hp hnorm hle hlt

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ ↑I
t : Set R
⊢ s * t ⊆ ↑I

Tactic:
by
  rintro - ⟨x, hx, r, -, rfl⟩
  exact mul_mem_right _ _ _ (h hx)

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
⊢ sInf {m | IsCoatom m} = sInf {I | I.IsMaximal}

Tactic:
Ideal.isMaximal_def

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ z ∈ span s ↔ z ∈ AddSubgroup.closure (univ * s * univ)

Tactic:
by
  trans z ∈ span (univ * s * univ)
  · refine ⟨(span_mono (fun x hx ↦ ?_) ·), fun hz ↦ ?_⟩
    · exact ⟨1 * x, ⟨1, mem_univ _, x, hx, rfl⟩, 1, mem_univ _, by simp⟩
    · exact mem_span_iff.mp hz (span s) <| subset_mul_set (set_mul_subset subset_span _) _
  · refine mem_span_iff_mem_addSubgroup_closure_absorbing ?_ ?_
    · intro x y hy
      rw [mul_assoc] at hy ⊢
      obtain ⟨r, -, y, hy, rfl⟩ := hy
      exact ⟨x * r, mem_univ _, y, hy, mul_assoc ..⟩
    · rintro - x ⟨y, hy, r, -, rfl⟩
      exact ⟨y, hy, r * x, mem_univ _, (mul_assoc ..).symm⟩

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: case e'_3
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N = Ring.jacobson R • Submodule.map N.subtype ⊤

Tactic:
Submodule.map_top,

Goal state after:
case e'_3
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N = Ring.jacobson R • N.subtype.range
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_2
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra S T
R : Type u_6
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
h₁ : Function.Surjective ⇑(algebraMap S T)
h₂ : Function.Surjective ⇑(algebraMap R S)
r : R
hr : IsUnit ((algebraMap R T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap R T) ≤ Ideal.comap (algebraMap R S) ⊥
⊢ Ideal.map (algebraMap R S) (r ^ n • RingHom.ker (algebraMap R T)) ≤ ⊥

Tactic:
← Ideal.map_le_iff_le_comap

Goal state after:
case refine_2
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra S T
R : Type u_6
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
h₁ : Function.Surjective ⇑(algebraMap S T)
h₂ : Function.Surjective ⇑(algebraMap R S)
r : R
hr : IsUnit ((algebraMap R T) r)
n : ℕ
hn : Ideal.map (algebraMap R S) (r ^ n • RingHom.ker (algebraMap R T)) ≤ ⊥
⊢ Ideal.map (algebraMap R S) (r ^ n • RingHom.ker (algebraMap R T)) ≤ ⊥
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: case e'_4
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ N = Submodule.map N.subtype ⊤

Tactic:
Submodule.map_top,

Goal state after:
case e'_4
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : Nontrivial ↥N
fg : Module.Finite R ↥N
⊢ N = N.subtype.range
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
⊢ sInf {J | map f I ≤ J ∧ J.IsMaximal} ≤ sInf (map f '' {J | I ≤ J ∧ J.IsMaximal})

Tactic:
· refine sInf_le_sInf_of_subset_insert_top fun j hj => hj.recOn fun J hJ => ?_
    rw [← hJ.2]
    rcases map_eq_top_or_isMaximal_of_surjective f hf hJ.left.right with htop | hmax
    · exact htop.symm ▸ Set.mem_insert ⊤ _
    · exact Set.mem_insert_of_mem ⊤ ⟨map_mono hJ.1.1, hmax⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case inl.inr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : m < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

Tactic:
have : n + m = n.natAbs - m.natAbs := by
      rw [Int.natAbs_of_nonneg hn, Int.ofNat_natAbs_of_nonpos hm.le, sub_neg_eq_add]

Goal state after:
case inl.inr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : m < 0
this : n + m = ↑n.natAbs - ↑m.natAbs
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: case refine_2.e_a
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ↑(sec M (f i)).2 * ↑(∏ j ∈ s.erase i, (sec M (f j)).2) = ∏ x ∈ s, M.subtype (sec M (f x)).2

Tactic:
Submonoid.coe_finsetProd,

Goal state after:
case refine_2.e_a
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ↑(sec M (f i)).2 * ∏ i ∈ s.erase i, ↑(sec M (f i)).2 = ∏ x ∈ s, M.subtype (sec M (f x)).2
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✝ : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsPullback f g h i

Tactic:
refine ⟨⟨e⟩, ⟨isLimitOfReflects F <| ?_⟩⟩

Goal state after:
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✝ : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsLimit (F.mapCone (PullbackCone.mk f g ⋯))
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
m : M
s : ↥S
⊢ 1 = IsLocalization.mk' T 1 1

Tactic:
rw [IsLocalization.mk'_one, map_one]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Comonad C
A B : G.Coalgebra
h : A.A ≅ B.A
w : A.a ≫ G.map h.hom = h.hom ≫ B.a
⊢ B.a ≫ G.map h.inv = h.inv ≫ A.a

Tactic:
by
        rw [h.eq_inv_comp, ← reassoc_of% w, ← Functor.map_comp]
        simp

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

Goal state before:
pp: A B : CommRingCat
s : BinaryCofan A B
x✝ : Discrete WalkingPair
j : WalkingPair
⊢ (A.coproductCocone B).ι.app { as := j } ≫
      ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom =
    s.ι.app { as := j }

Tactic:
by cases j <;> ext a <;> simp

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

Goal state before:
pp: A B : CommRingCat
f g : A ⟶ B
⊢ ofHom ((Hom.hom f).eqLocus (Hom.hom g)).subtype ≫ f = ofHom ((Hom.hom f).eqLocus (Hom.hom g)).subtype ≫ g

Tactic:
ext ⟨x, e⟩
      simpa using e

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

Goal state before:
pp: 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 : S
x✝ : ∃ m, m • x = 0
m : R
hm : m ∈ M
e : ⟨m, hm⟩ • x = 0
⊢ (algebraMap R S') m * f x = (algebraMap R S') m * 0

Tactic:
rw [← Algebra.smul_def]

Goal state after:
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 : S
x✝ : ∃ m, m • x = 0
m : R
hm : m ∈ M
e : ⟨m, hm⟩ • x = 0
⊢ m • f x = (algebraMap R S') m * 0
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 Q : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{w, v, u} P
inst✝ : ObjectProperty.Small.{w, v, u} Q
⊢ Function.Surjective fun x ↦
    match x with
    | Sum.inl x => ⟨↑x, ⋯⟩
    | Sum.inr x => ⟨↑x, ⋯⟩

Tactic:
rintro ⟨x, hx | hx⟩ <;> aesop

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

Goal state before:
pp: case refine_2
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 : ∃ a, ∃ (b : P' a), ↑(φ ⟨a, b⟩) = X
⊢ P X

Tactic:
obtain ⟨Y, hY, rfl⟩ := hX

Goal state after:
case refine_2
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'))
Y : C
hY : P' Y
⊢ P ↑(φ ⟨Y, hY⟩)
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_1.inr
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✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid

Tactic:
· apply AddSubmonoid.mem_sup_left
          exact ⟨X i, map_X _ _⟩

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

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

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

Goal state after:
case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ eqToHom ⋯ ≫
      eqToHom ⋯ ≫
        ((Cat.Hom.toNatIso (eqToIso ⋯) ≪≫ eqToIso ⋯).hom.app ((F.map f.base).toFunctor.obj X.fiber) ≫
            (𝟭 ↑(F.obj Y.base)).map f.fiber ≫ (Cat.Hom.toNatIso (eqToIso ⋯) ≪≫ eqToIso ⋯).inv.app Y.fiber) ≫
          eqToHom ⋯ =
    f.fiber
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b : Cat} (f : a ⟶ b), NatTrans.toCatHom₂ (map₂ (𝟙 f).toNatTrans) = 𝟙 (map f.toFunctor).toCatHom

Tactic:
intros
    ext X
    cases X <;> rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b : Cat} (f : a ⟶ b), NatTrans.toCatHom₂ (map₂ (𝟙 f).toNatTrans) = 𝟙 (map f.toFunctor).toCatHom

Tactic:
by
    intros
    ext X
    cases X <;> rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b : Cat} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
    NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans) =
      NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)

Tactic:
intros
    ext X
    cases X <;> rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b : Cat} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
    NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans) =
      NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)

Tactic:
by
    intros
    ext X
    cases X <;> rfl

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:
by
        rintro ⟨_, ⟨⟩⟩ ⟨_, ⟨⟩⟩ ⟨base, ⟨⟨f⟩⟩⟩
        dsimp at *
        simp
        rfl

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

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cone (F ⋙ G)
j : C
⊢ ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ F.obj j) (k₂ : F.obj X₂ ⟶ F.obj j) (f : X₁ ⟶ X₂),
    F.map f ≫ k₂ = k₁ → s.π.app X₁ ≫ G.map k₁ = s.π.app j → s.π.app X₂ ≫ G.map k₂ = s.π.app j

Tactic:
intro j₁ j₂ k₁ k₂ f w h
    rw [← s.w f]
    rw [← w] at h
    simpa using h

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.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesLimit G H
c : Cone (F ⋙ G)
hc : IsLimit c
⊢ Nonempty (IsLimit (H.mapCone c))

Tactic:
refine ⟨isLimitExtendConeEquiv (G := G ⋙ H) F (H.mapCone c) ?_⟩
    let hc' := isLimitOfPreserves H ((isLimitExtendConeEquiv F c).symm hc)
    exact IsLimit.ofIsoLimit hc' (Cone.ext (Iso.refl _) (by simp))

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Initial
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
G : D ⥤ E
inst✝ : HasLimit G
⊢ IsIso (limit.pre G F)

Tactic:
limit.pre_eq (limitConeComp F (getLimitCone G)) (getLimitCone G)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Initial
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
G : D ⥤ E
inst✝ : HasLimit G
⊢ IsIso
    ((limit.isoLimitCone (getLimitCone G)).hom ≫
      (limitConeComp F (getLimitCone G)).isLimit.lift (Cone.whisker F (getLimitCone G).cone) ≫
        (limit.isoLimitCone (limitConeComp F (getLimitCone G))).inv)
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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hF : F.Final
hG : G.Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
s₃ : E ≌ AsSmall E := AsSmall.equiv
⊢ (F ⋙ G).Final

Tactic:
let i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅
      (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ (s₂.inverse ⋙ G ⋙ s₃.functor) :=
    isoWhiskerLeft (s₁.inverse ⋙ F) (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hF : F.Final
hG : G.Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
s₃ : E ≌ AsSmall E := AsSmall.equiv
i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
⊢ (F ⋙ G).Final
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
f : A →ₐ[R] B
hf : Surjective ⇑f
inst✝¹ : FinitePresentation R A
inst✝ : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ⇑g
right✝ : (RingHom.ker g.toRingHom).FG
⊢ Ideal.comap ↑f ⊥ = Ideal.map (↑g) (Ideal.comap ((↑f).comp ↑g) ⊥)

Tactic:
rw [← Ideal.comap_comap, Ideal.map_comap_of_surjective (g : MvPolynomial (Fin n) R →+* A) hg]

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
comm : a ≫ f₁ = b ≫ f₁
big_k : IsKernelPair (f₁ ≫ f₂) a b
s : PullbackCone f₁ f₁
s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯
⊢ { l //
    l ≫ (PullbackCone.mk a b comm).fst = s.fst ∧
      l ≫ (PullbackCone.mk a b comm).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk a b comm).pt},
          m ≫ (PullbackCone.mk a b comm).fst = s.fst → m ≫ (PullbackCone.mk a b comm).snd = s.snd → m = l }

Tactic:
refine ⟨big_k.isLimit.lift s', big_k.isLimit.fac _ WalkingCospan.left,
          big_k.isLimit.fac _ WalkingCospan.right, fun m₁ m₂ => ?_⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
comm : a ≫ f₁ = b ≫ f₁
big_k : IsKernelPair (f₁ ≫ f₂) a b
s : PullbackCone f₁ f₁
s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯
m✝ : s.pt ⟶ (PullbackCone.mk a b comm).pt
m₁ : m✝ ≫ (PullbackCone.mk a b comm).fst = s.fst
m₂ : m✝ ≫ (PullbackCone.mk a b comm).snd = s.snd
⊢ m✝ = (IsPullback.isLimit big_k).lift s'
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : Mono g
hcomp : P (f ≫ g)
this : f = (asIso (pullback.fst (f ≫ g) g)).inv ≫ pullback.snd (f ≫ g) g
⊢ P ((asIso (pullback.fst (f ≫ g) g)).inv ≫ pullback.snd (f ≫ g) g)

Tactic:
cancel_left_of_respectsIso (P := P)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : Mono g
hcomp : P (f ≫ g)
this : f = (asIso (pullback.fst (f ≫ g) g)).inv ≫ pullback.snd (f ≫ g) g
⊢ P (pullback.snd (f ≫ g) g)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : P.IsStableUnderCobaseChange
S S' X Y : C
f : S ⟶ S'
v₂₂ : S ⟶ Y
g : Y ⟶ X
inst✝¹ : HasPushout v₂₂ f
H : P g
inst✝ : HasPushout (v₂₂ ≫ g) f
⊢ IsPushout (pushout.inl v₂₂ f) g (pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) f) ⋯)
    (pushout.inl (v₂₂ ≫ g) f)

Tactic:
refine IsPushout.of_top ?_ (by simp) (IsPushout.of_hasPushout v₂₂ f).flip

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : P.IsStableUnderCobaseChange
S S' X Y : C
f : S ⟶ S'
v₂₂ : S ⟶ Y
g : Y ⟶ X
inst✝¹ : HasPushout v₂₂ f
H : P g
inst✝ : HasPushout (v₂₂ ≫ g) f
⊢ IsPushout f (v₂₂ ≫ g) (pushout.inr v₂₂ f ≫ pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) f) ⋯)
    (pushout.inl (v₂₂ ≫ g) f)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : W.IsStableUnderLimitsOfShape J
⊢ W.limitsOfShape J ≤ W

Tactic:
← isStableUnderLimitsOfShape_iff_limitsOfShape_le

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : W.IsStableUnderLimitsOfShape J
⊢ W.IsStableUnderLimitsOfShape J
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
hPQ : P ≤ Q
X : C
h : P.LimitOfShape J X
⊢ Q.limitsOfShape J X

Tactic:
exact ⟨h.ofLE hPQ⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ W ≤ W.colimitsOfShape (Discrete PUnit.{w + 1})

Tactic:
intro X₁ X₂ f hf
  have h := initialIsInitial (C := Discrete (PUnit.{w + 1}))
  let c₁ := coconeOfDiagramInitial (F := Discrete.functor (fun _ ↦ X₁)) h
  let c₂ := coconeOfDiagramInitial (F := Discrete.functor (fun _ ↦ X₂)) h
  have hc₁ : IsColimit c₁ := colimitOfDiagramInitial h _
  have hc₂ : IsColimit c₂ := colimitOfDiagramInitial h _
  have : hc₁.desc (Cocone.mk _ (Discrete.natTrans (fun _ ↦ by exact f) ≫ c₂.ι)) = f :=
    hc₁.hom_ext (fun x ↦ by
      obtain rfl : x = ⊥_ _ := by ext
      rw [IsColimit.fac]
      simp [c₁, c₂])
  rw [← this]
  exact ⟨_, _, _, _, _, hc₂, _, fun _ ↦ hf⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} W
⊢ coproducts.{w, v, u} W ≤ W

Tactic:
by
  intro X Y f hf
  rw [coproducts_iff] at hf
  obtain ⟨J, hf⟩ := hf
  exact colimitsOfShape_le _ hf

Goal state after: