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

Goal state before:
pp: S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring R'
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra S R
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
⊢ { f // ∀ (x y : M), f x * f y = 0 } ≃
    { fg //
      (∀ (x y : M), fg.2 x * fg.2 y = 0) ∧
        (∀ (r : R') (x : M), fg.2 (r •> x) = fg.1 r * fg.2 x) ∧ ∀ (r : R') (x : M), fg.2 (x <• r) = fg.2 x * fg.1 r }

Tactic:
exact {
    toFun := fun f => ⟨(Algebra.ofId _ _, f.val), f.prop,
      fun r x => by simp [Algebra.smul_def, Algebra.ofId_apply],
      fun r x => by simp [Algebra.smul_def, Algebra.ofId_apply, Algebra.commutes]⟩
    invFun := fun fg => ⟨fg.val.2, fg.prop.1⟩ }

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
s : S
m : ↑M
⊢ (Hom.hom ((restrictScalars f).map α)) (s ⊗ₜ[R] m) = (Hom.hom ((restrictScalars f).map β)) (s ⊗ₜ[R] m)

Tactic:
change α (s ⊗ₜ m) = β (s ⊗ₜ m)

Goal state after:
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
s : S
m : ↑M
⊢ (ConcreteCategory.hom α) (s ⊗ₜ[R] m) = (ConcreteCategory.hom β) (s ⊗ₜ[R] m)
Module: Mathlib.CategoryTheory.Category.Pointed

Goal state before:
pp: X Y Z : Pointed
f : X.Hom Y
g : Y.Hom Z
⊢ g.toFun (f.toFun X.point) = Z.point

Tactic:
f.map_point,

Goal state after:
X Y Z : Pointed
f : X.Hom Y
g : Y.Hom Z
⊢ g.toFun Y.point = Z.point
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
⊢ ∀ (y : ↥(Submonoid.powers r)), IsUnit ((algebraMap R S) ↑y)

Tactic:
rintro ⟨-, n, rfl⟩

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
n : ℕ
⊢ IsUnit ((algebraMap R S) ↑⟨(fun x ↦ r ^ x) n, ⋯⟩)
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
⊢ t * s ⊆ ↑I

Tactic:
rintro - ⟨r, -, x, hx, rfl⟩

Goal state after:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ ↑I
t : Set R
r x : R
hx : x ∈ s
⊢ (fun x1 x2 ↦ x1 * x2) r x ∈ ↑I
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
h : ∃! P, P ≠ ⊥ ∧ P.IsPrime
⊢ ∃! I, I.IsMaximal

Tactic:
rcases h with ⟨P, ⟨hPnonzero, hPnot_top, _⟩, hPunique⟩

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
⊢ ∃! I, I.IsMaximal
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S)
tfae_2_to_4 : ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalHom f
tfae_1_to_5 : IsLocalHom f → Ideal.comap f (maximalIdeal S) = maximalIdeal R
⊢ [IsLocalHom f, ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S), Ideal.map f (maximalIdeal R) ≤ maximalIdeal S,
      maximalIdeal R ≤ Ideal.comap f (maximalIdeal S), Ideal.comap f (maximalIdeal S) = maximalIdeal R].TFAE

Tactic:
tfae_have 5 → 4 := fun h ↦ le_of_eq h.symm

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S)
tfae_2_to_4 : ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalHom f
tfae_1_to_5 : IsLocalHom f → Ideal.comap f (maximalIdeal S) = maximalIdeal R
tfae_5_to_4 : Ideal.comap f (maximalIdeal S) = maximalIdeal R → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ [IsLocalHom f, ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S), Ideal.map f (maximalIdeal R) ≤ maximalIdeal S,
      maximalIdeal R ≤ Ideal.comap f (maximalIdeal S), Ideal.comap f (maximalIdeal S) = maximalIdeal R].TFAE
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
I X : C
inst✝ : HasBinaryProduct I X
hI : IsInitial I
⊢ I ⨯ X ≅ I

Tactic:
have := hI.isIso_to (prod.fst : I ⨯ X ⟶ I)
  exact asIso prod.fst

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

Goal state before:
pp: case pos
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
d : ℤ
hd : d ≤ 0
⊢ selfZPow x B d * selfZPow x B (-d) = 1

pp: case neg
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
d : ℤ
hd : 0 < d
⊢ selfZPow x B d * selfZPow x B (-d) = 1

Tactic:
· rw [selfZPow_of_nonpos x B hd, selfZPow_of_nonneg, ← map_pow, Int.natAbs_neg,
      Submonoid.pow_apply, IsLocalization.mk'_spec, map_one]
    apply nonneg_of_neg_nonpos
    rwa [neg_neg]

Goal state after:
case neg
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
d : ℤ
hd : 0 < d
⊢ selfZPow x B d * selfZPow x B (-d) = 1
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
c : BinaryFan X Y
hc : IsLimit c
T : C
hT : IsTerminal T
s :
  PullbackCone (hT.from ((pair X Y).obj { as := WalkingPair.left }))
    (hT.from ((pair X Y).obj { as := WalkingPair.right }))
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
h₁ : m ≫ c.fst = s.fst
h₂ : m ≫ c.snd = s.snd
⊢ m = BinaryFan.IsLimit.lift hc s.fst s.snd

Tactic:
apply BinaryFan.IsLimit.hom_ext hc

Goal state after:
case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
c : BinaryFan X Y
hc : IsLimit c
T : C
hT : IsTerminal T
s :
  PullbackCone (hT.from ((pair X Y).obj { as := WalkingPair.left }))
    (hT.from ((pair X Y).obj { as := WalkingPair.right }))
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
h₁ : m ≫ c.fst = s.fst
h₂ : m ≫ c.snd = s.snd
⊢ m ≫ c.fst = BinaryFan.IsLimit.lift hc s.fst s.snd ≫ c.fst

case h₂
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
c : BinaryFan X Y
hc : IsLimit c
T : C
hT : IsTerminal T
s :
  PullbackCone (hT.from ((pair X Y).obj { as := WalkingPair.left }))
    (hT.from ((pair X Y).obj { as := WalkingPair.right }))
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
h₁ : m ≫ c.fst = s.fst
h₂ : m ≫ c.snd = s.snd
⊢ m ≫ c.snd = BinaryFan.IsLimit.lift hc s.fst s.snd ≫ c.snd
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 : 1 ⊗ₜ[R] IsLocalization.mk' Rₘ x y = (algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)
h : ∀ (x : R), (algebraMap S Sₘ) ((algebraMap R S) x) = (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x)
⊢ (algebraMap S (Localization (Algebra.algebraMapSubmonoid S M))) ((algebraMap R S) x) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
        (IsLocalization.mk' (Localization M) x y) *
      (algebraMap S (Localization (Algebra.algebraMapSubmonoid S M))) ((algebraMap R S) ↑y)

Tactic:
rw [h, h, ← map_mul, IsLocalization.mk'_spec]

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
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
⊢ ∀ (a b c : LocalizedModule S A), a * (b + c) = a * b + a * c

Tactic:
rintro ⟨a₁, s₁⟩ ⟨a₂, s₂⟩ ⟨a₃, s₃⟩
      change a₁ /ₒ s₁ * (a₂ /ₒ s₂ + a₃ /ₒ s₃) = a₁ /ₒ s₁ * (a₂ /ₒ s₂) + a₁ /ₒ s₁ * (a₃ /ₒ s₃)
      rw [← mk, ← mk, ← mk, mk_mul_mk, mk_mul_mk, mk_add_mk, mk_mul_mk, mk_add_mk]
      apply mk_eq.mpr _
      use 1
      simp only [← mul_assoc, mul_right_comm, mul_add, mul_smul_comm, smul_add, smul_smul, one_mul]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
g' : W ⟶ Y
inst✝¹ : HasPullback f g
inst✝ : HasPullback (pullback.snd f g) g'
⊢ (pullbackLeftPullbackSndIso f g g').inv ≫ pullback.fst (pullback.snd f g) g' ≫ pullback.snd f g =
    pullback.snd f (g' ≫ g) ≫ g'

Tactic:
rw [pullback.condition]
  exact pullbackLeftPullbackSndIso_inv_snd_snd_assoc f g g' g'

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x : FreeRing α
⊢ toFreeCommRing (-x) = -toFreeCommRing x

Tactic:
map_neg

Goal state after:
α : Type u
x : FreeRing α
⊢ -toFreeCommRing x = -toFreeCommRing x
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ (algebraMap (Localization S) (LocalizedModule S A)) (Localization.mk a s) = mk ((algebraMap R A) a) s

Tactic:
Localization.mk_eq_mk'

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ (algebraMap (Localization S) (LocalizedModule S A)) (IsLocalization.mk' (Localization S) a s) =
    mk ((algebraMap R A) a) s
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A : Under R
⊢ pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫ Under.Hom.right (tensorProdObjIsoPushoutObj S A).inv =
    ofHom Algebra.TensorProduct.includeRight.toRingHom

Tactic:
by
  simp [tensorProdObjIsoPushoutObj]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A : Under R
⊢ pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫ Under.Hom.right (tensorProdObjIsoPushoutObj S A).inv =
    ofHom Algebra.TensorProduct.includeLeftRingHom

Tactic:
by
  simp [tensorProdObjIsoPushoutObj]

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

Goal state before:
pp: R S : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
R' S' : Type u
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' := (⋯.isoPushout ≪≫ h.isoPushout.symm).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    (ConcreteCategory.hom ⋯.isoPushout.hom) (r ⊗ₜ[R] 1) =
      (ConcreteCategory.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) r
h3 :
  ∀ (x : R'),
    (Hom.hom h.isoPushout.inv) ((Hom.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) x) =
      (algebraMap R' S') x
r : R'
⊢ e.toFun ((algebraMap R' (R' ⊗[R] S)) r) = (algebraMap R' S') r

Tactic:
simp [Iso.commRingCatIsoToRingEquiv, h2, e, h3]

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

Goal state before:
pp: R S Rₘ Sₘ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing Rₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : CommRing S
inst✝³ : CommRing Sₘ
inst✝² : Algebra S Sₘ
f : R →+* S
fₘ : Rₘ →+* Sₘ
H : fₘ.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp f
M : Submonoid R
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
⊢ IsPushout (ofHom f) (ofHom (algebraMap R Rₘ)) (ofHom (algebraMap S Sₘ)) (ofHom fₘ)

Tactic:
algebraize [f, fₘ, fₘ.comp (algebraMap R Rₘ)]

Goal state after:
R S Rₘ Sₘ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing Rₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : CommRing S
inst✝³ : CommRing Sₘ
inst✝² : Algebra S Sₘ
f : R →+* S
fₘ : Rₘ →+* Sₘ
H : fₘ.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp f
M : Submonoid R
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra Rₘ Sₘ := fₘ.toAlgebra
algInst✝ : Algebra R Sₘ := (fₘ.comp (algebraMap R Rₘ)).toAlgebra
scalarTowerInst✝ : IsScalarTower R Rₘ Sₘ := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R Sₘ))
⊢ IsPushout (ofHom f) (ofHom (algebraMap R Rₘ)) (ofHom (algebraMap S Sₘ)) (ofHom fₘ)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : AddCommGroup M
inst✝³ : SubtractionCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ (fromLocalizedModule S f) (-LocalizedModule.mk m s) = -(fromLocalizedModule S f) (LocalizedModule.mk m s)

Tactic:
map_neg

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : AddCommGroup M
inst✝³ : SubtractionCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ -(fromLocalizedModule S f) (LocalizedModule.mk m s) = -(fromLocalizedModule S f) (LocalizedModule.mk m s)
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J) (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' : J
⊢ F j = F j'

Tactic:
by
  simpa using
    any_functor_const_on_obj
      { obj := Discrete.mk ∘ F
        map := fun f => eqToHom (by ext; exact h _ _ f) }
      j j'

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

Goal state before:
pp: 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 : Subtype P'
⊢ ↑(φ X) ∈ Set.range (Subtype.val ∘ φ)

Tactic:
by tauto

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F₁ F₂ : C ⥤ Type w
α : F₁ ⟶ F₂
t₁ t₂ : F₁.Elements
k : t₁ ⟶ t₂
⊢ (ConcreteCategory.hom (F₂.map ↑k)) ⟨t₁.fst, (ConcreteCategory.hom (α.app t₁.fst)) t₁.snd⟩.snd =
    ⟨t₂.fst, (ConcreteCategory.hom (α.app t₂.fst)) t₂.snd⟩.snd

Tactic:
by simpa [map_snd] using (NatTrans.naturality_apply α k.1 t₁.2).symm

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.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
⊢ G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j

Tactic:
rw [← s.w f] at h

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₁ ≫ (F ⋙ G).map f ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x : WidePullbackShape J
⊢ (fun x ↦
        match x with
        | of x => some x.as
        | star => none)
      ((fun x ↦
          match x with
          | some x => of { as := x }
          | none => star)
        x) =
    x

Tactic:
cases x <;> simp

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 : WithTerminal (Discrete J)
⊢ (fun x ↦
        match x with
        | some x => of { as := x }
        | none => star)
      ((fun x ↦
          match x with
          | of x => some x.as
          | star => none)
        x) =
    x

Tactic:
cases x <;> simp

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 j₁ j₂ : C
k₁ : F.obj j₁ ⟶ F.obj j
k₂ : F.obj j₂ ⟶ F.obj j
f : j₁ ⟶ j₂
w : F.map f ≫ k₂ = k₁
h : s.π.app j₂ ≫ G.map k₂ = s.π.app j
⊢ s.π.app j₁ ≫ G.map k₁ = s.π.app j

Tactic:
rw [← s.w f] at h

Goal state after:
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 j₁ j₂ : C
k₁ : F.obj j₁ ⟶ F.obj j
k₂ : F.obj j₂ ⟶ F.obj j
f : j₁ ⟶ j₂
w : F.map f ≫ k₂ = k₁
h : (s.π.app j₁ ≫ (F ⋙ G).map f) ≫ G.map k₂ = s.π.app j
⊢ s.π.app j₁ ≫ G.map k₁ = s.π.app j
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
n : ℕ
g' : MvPolynomial (Fin n) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
g : MvPolynomial (Fin n) R →ₐ[R] S
⊢ Q R S (g'.comp MvPolynomial.C)

Tactic:
clear g

Goal state after:
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
n : ℕ
g' : MvPolynomial (Fin n) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ Q R S (g'.comp MvPolynomial.C)
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
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
inst✝ : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₂
X✝ Y✝ : C
f : X✝ ⟶ Y✝
d : ↑(F.obj X✝)
this : (F.map f ≫ α.app Y✝).toFunctor.obj d = (α.app X✝ ≫ G.map f).toFunctor.obj d
⊢ H.map { base := f, fiber := eqToHom ⋯ } ≫
      colimit.ι (ι G Y✝ ⋙ H) ((α.app Y✝).toFunctor.obj ((F.map f).toFunctor.obj d)) =
    H.map { base := f, fiber := 𝟙 ((G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d)) } ≫
      colimit.ι (ι G Y✝ ⋙ H) ((G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d))

Tactic:
dsimp at this

Goal state after:
C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F✝ : D ⥤ Cat
G✝ : C✝ ⥤ D
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
inst✝ : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₂
X✝ Y✝ : C
f : X✝ ⟶ Y✝
d : ↑(F.obj X✝)
this : (α.app Y✝).toFunctor.obj ((F.map f).toFunctor.obj d) = (G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d)
⊢ H.map { base := f, fiber := eqToHom ⋯ } ≫
      colimit.ι (ι G Y✝ ⋙ H) ((α.app Y✝).toFunctor.obj ((F.map f).toFunctor.obj d)) =
    H.map { base := f, fiber := 𝟙 ((G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d)) } ≫
      colimit.ι (ι G Y✝ ⋙ H) ((G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d))