mathlib-initiative/mathlib-tactics huggingface dataset:
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
a b : M × ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : ↑u * ↑b.2 = v * ↑a.2
⊢ (v * ↑a.2) • a.1 = (↑u * ↑a.2) • b.1

Tactic:
mul_comm,

Goal state after:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : ↑u * ↑b.2 = v * ↑a.2
⊢ (↑a.2 * v) • a.1 = (↑u * ↑a.2) • b.1
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
a b : M × ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : ↑u * ↑b.2 = v * ↑a.2
⊢ ↑a.2 • u • b.1 = (↑u * ↑a.2) • b.1

Tactic:
mul_comm,

Goal state after:
case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : ↑u * ↑b.2 = v * ↑a.2
⊢ ↑a.2 • u • b.1 = (↑a.2 * ↑u) • b.1
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
s : S
x : R
y : ↥M
⊢ s ⊗ₜ[R] (mk' A x y * (algebraMap R A) ↑y) = (algebraMap S (S ⊗[R] A)) ((algebraMap R S) x * s)

Tactic:
mul_comm,

Goal state after:
R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
s : S
x : R
y : ↥M
⊢ s ⊗ₜ[R] ((algebraMap R A) ↑y * mk' A x y) = (algebraMap S (S ⊗[R] A)) ((algebraMap R S) x * s)
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✝ : LocalizedModule S A
a : A
s : ↥S
⊢ 1 • s • ((1, 1).1 * (a, s).1) = 1 • ((a, s).2 * (1, 1).2) • a

Tactic:
by simp only [one_mul, mul_one, one_smul]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Y₃ Y₂ Y₁ X₃ : C
g₂ : Y₃ ⟶ Y₂
g₁ : Y₂ ⟶ Y₁
i₃ : Y₃ ⟶ X₃
t₁ : PushoutCocone g₂ i₃
i₂ : Y₂ ⟶ t₁.pt
t₂ : PushoutCocone g₁ «i₂»
hi₂ : «i₂» = t₁.inl
H₁ : IsColimit t₁
H₂ : IsColimit t₂
⊢ IsColimit (t₁.pasteVert t₂ hi₂)

Tactic:
apply PushoutCocone.isColimitOfFlip <| IsColimit.ofIsoColimit _ (t₁.pasteVertFlip t₂ hi₂).symm
  exact pasteHorizIsPushout hi₂ (PushoutCocone.flipIsColimit H₁) (PushoutCocone.flipIsColimit H₂)

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
r : R
m : M
s t : ↥S
⊢ r • m /ₒ (t * s) = mk (r • m) (s * t)

Tactic:
by rw [mul_comm]

Goal state after:
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
x : T
q : LocalizedModule S M
m : M
s : ↥S
⊢ x • (mk m s + q) = x • mk m s + x • q

Tactic:
induction q with | _ n t

Goal state after:
case h.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
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ x • (mk m s + mk n t) = x • mk m s + x • mk n t
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullbacksAlong g
P : C
p : P ⟶ X
e : Over.mk p ≅ Over.mk (pullback.fst f g)
⊢ IsPullback p (Over.Hom.left e.hom ≫ pullback.snd f g) f g

Tactic:
exact of_over_iso e

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

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

Tactic:
mul_comm,

Goal state after:
α : Type u
inst✝ : Subsingleton α
x y : FreeRing α
⊢ x * y =
    (subsingletonEquivFreeCommRing α).symm ((subsingletonEquivFreeCommRing α) x * (subsingletonEquivFreeCommRing α) y)
Module: Mathlib.RingTheory.FreeCommRing

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

Tactic:
← (subsingletonEquivFreeCommRing α).map_mul,

Goal state after:
α : Type u
inst✝ : Subsingleton α
x y : FreeRing α
⊢ x * y = (subsingletonEquivFreeCommRing α).symm ((subsingletonEquivFreeCommRing α) (x * y))
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.h.mpr
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • (⟨r, hr⟩ * t) • m = a • s • n
⊢ a • t • r • m = a • (⟨r, hr⟩ * t) • m

Tactic:
mul_comm,

Goal state after:
case h.h.mpr
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • (⟨r, hr⟩ * t) • m = a • s • n
⊢ a • t • r • m = a • (t * ⟨r, hr⟩) • m
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
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
r : R
a : A
s : ↥S
⊢ mk ((algebraMap R A) r * a) (1 * s) = mk (a * (algebraMap R A) r) (s * 1)

Tactic:
mul_comm,

Goal state after:
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
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
r : R
a : A
s : ↥S
⊢ mk ((algebraMap R A) r * a) (s * 1) = mk (a * (algebraMap R A) r) (s * 1)
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.μ
⊢ IsSplitMono (T.η.app X) ↔ IsIso (T.η.app X)

Tactic:
refine ⟨fun _ ↦ ⟨retraction (T.η.app X), by simp, ?_⟩, fun _ ↦ inferInstance⟩
  rw [← map_id, ← show T.η.app X ≫ retraction (T.η.app X) = 𝟙 X from IsSplitMono.id _,
    map_comp, T.map_unit_app X, ← T.unit_naturality]

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
f : A ⟶ B
inst✝ : IsIso f.f
⊢ B.a ≫ G.map (inv f.f) = inv f.f ≫ A.a

Tactic:
rw [IsIso.eq_inv_comp f.f, ← f.h_assoc]
          simp

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

Goal state before:
pp: case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ (↑b * ↑b') • g a' = ↑b' • g (b • a')

Tactic:
mul_comm,

Goal state after:
case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ (↑b' * ↑b) • g a' = ↑b' • g (b • a')
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_a
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
⊢ (↑b * ↑b') • f a' = ↑b' • b • f a'

Tactic:
mul_comm,

Goal state after:
case e_a
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
⊢ (↑b' * ↑b) • f a' = ↑b' • b • f a'
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M'
a : M
b : ↥S
eq1 : b • m = f a
⊢ (b * ⋯.choose.2) • m = ⋯.choose.2 • f a

Tactic:
mul_comm,

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
m : M'
a : M
b : ↥S
eq1 : b • m = f a
⊢ (⋯.choose.2 * b) • m = ⋯.choose.2 • f a
Module: Mathlib.CategoryTheory.Adjunction.Comma

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
⊢ (fun g ↦ (terminal.from (CostructuredArrow.mk g)).left) ((fun g ↦ G.map g ≫ (⊤_ CostructuredArrow G A).hom) g) = g

Tactic:
let B' : CostructuredArrow G A :=
      CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
⊢ (fun g ↦ (terminal.from (CostructuredArrow.mk g)).left) ((fun g ↦ G.map g ≫ (⊤_ CostructuredArrow G A).hom) g) = g
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case refine_2
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : ↑X
e : 0 * x = 1 * x
⊢ (Hom.hom (ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f)) x = (Hom.hom (𝟙 X)) x

Tactic:
one_mul,

Goal state after:
case refine_2
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : ↑X
e : 0 * x = x
⊢ (Hom.hom (ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f)) x = (Hom.hom (𝟙 X)) x
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
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
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
a b : M'
hab : g a = g b
x : M
m : ↥S
hxm : m • a = f x
y : M
n : ↥S
hym : n • b = f y
h : ↑n • f x = ↑m • f y
⊢ n • m • a = (n * m) • b

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
N : Type u_6
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
a b : M'
hab : g a = g b
x : M
m : ↥S
hxm : m • a = f x
y : M
n : ↥S
hym : n • b = f y
h : ↑n • f x = ↑m • f y
⊢ n • m • a = (m * n) • b
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ iso S (mkLinearMap S M) = LinearEquiv.refl R (LocalizedModule S M)

Tactic:
by
  let f := mkLinearMap S M
  obtain ⟨e, _, univ⟩ := is_universal S f f (map_units f)
  rw [← toLinearMap_inj, univ (iso S f) ((eq_toLinearMap_symm_comp f f).1 (iso_symm_comp S f).symm)]
  exact Eq.symm <| univ (refl R (LocalizedModule S M)) (by simp)

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

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing A
f : R →+* S
g : S →+* A
hf : (RingHom.ker f).FG
hg : (RingHom.ker g).FG
hsur : Function.Surjective ⇑f
this : Algebra R S := f.toAlgebra
⊢ (RingHom.ker (g.comp f)).FG

Tactic:
let : Algebra R A := RingHom.toAlgebra (g.comp f)

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing A
f : R →+* S
g : S →+* A
hf : (RingHom.ker f).FG
hg : (RingHom.ker g).FG
hsur : Function.Surjective ⇑f
this✝ : Algebra R S := f.toAlgebra
this : Algebra R A := (g.comp f).toAlgebra
⊢ (RingHom.ker (g.comp f)).FG
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
hPQ : Q ≤ P.isoClosure
x✝ : Q.FullSubcategory
Y : C
hY : Q Y
⊢ (ιOfLE h).essImage { obj := Y, property := hY }

Tactic:
· obtain ⟨X, hX, ⟨e⟩⟩ := hPQ _ hY
    exact ⟨⟨X, hX⟩, ⟨Q.ι.preimageIso e.symm⟩⟩

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case h.right
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
hco : ((↑e).comp f).toRingHom = (↑e.toRingEquiv).comp f.toRingHom
⊢ Ideal.comap f.toRingHom (Ideal.comap ↑e.toRingEquiv ⊥) = RingHom.ker f.toRingHom

Tactic:
← RingHom.ker_eq_comap_bot,

Goal state after:
case h.right
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
hco : ((↑e).comp f).toRingHom = (↑e.toRingEquiv).comp f.toRingHom
⊢ Ideal.comap f.toRingHom (RingHom.ker ↑e.toRingEquiv) = RingHom.ker f.toRingHom
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✝¹ : LocallySmall.{w, v, u} C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ EssentiallySmall.{w, v, u} P.FullSubcategory

Tactic:
by
  obtain ⟨Q, _, h₁, h₂⟩ := EssentiallySmall.exists_small_le P
  have := (isEquivalence_ιOfLE_iff h₁).2 h₂
  rw [← essentiallySmall_congr (ιOfLE h₁).asEquivalence]
  exact essentiallySmall_of_small_of_locallySmall _

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R A
inst✝ hfpB : FinitePresentation A B
n : ℕ
I : Ideal (MvPolynomial (Fin n) A)
e : (MvPolynomial (Fin n) A ⧸ I) ≃ₐ[A] B
hfg : I.FG
⊢ FinitePresentation R B

Tactic:
let : FinitePresentation R (MvPolynomial (Fin n) A ⧸ I) :=
    (mvPolynomial_of_finitePresentation _).quotient hfg

Goal state after:
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 A
inst✝ hfpB : FinitePresentation A B
n : ℕ
I : Ideal (MvPolynomial (Fin n) A)
e : (MvPolynomial (Fin n) A ⧸ I) ≃ₐ[A] B
hfg : I.FG
this : FinitePresentation R (MvPolynomial (Fin n) A ⧸ I) := FinitePresentation.quotient hfg
⊢ FinitePresentation R B
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
X : C
inst✝² : IsConnected J
F : J ⥤ C
inst✝¹ : HasLimit F
c : Cone F
inst✝ : IsIso (limMap c.π)
⊢ IsLimit c

Tactic:
refine IsLimit.ofIsoLimit (limit.isLimit _) (Cone.ext ((asIso (limMap c.π)).symm ≪≫
    (limit.isLimit _).conePointUniqueUpToIso (isLimitConstCone J c.pt)) ?_)
  intro j
  simp only [limit.cone_x, limit.cone_π, Iso.trans_hom, Iso.symm_hom,
    asIso_inv, assoc, IsIso.eq_inv_comp, limMap_π]
  congr 1
  simp [← Iso.inv_comp_eq_id]

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
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
⊢ ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ → G.map k₂ ≫ c.ι.app X₂ = G.map f ≫ c.ι.app Y → G.map k₁ ≫ c.ι.app X₁ = G.map f ≫ c.ι.app Y

Tactic:
· intro _ _ _ _ _ h₁ h₂
    simp [← h₂, ← h₁, ← Functor.comp_map, c.ι.naturality]

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

Goal state before:
pp: J : Type v₁
⊢ IsConnected (WidePushoutShape J)

Tactic:
apply IsConnected.of_induct
  · introv hp t
    cases j
    · exact hp
    · rwa [← t (WidePushoutShape.Hom.init _)]

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.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : CreatesColimit (F ⋙ G) H
c : Cocone (G ⋙ H)
hc : IsColimit c
i : H.mapCocone (liftColimit ((isColimitWhiskerEquiv F c).symm hc)) ≅ Cocone.whisker F c :=
  liftedColimitMapsToOriginal ((isColimitWhiskerEquiv F c).symm hc)
⊢ H.mapCocone (extendCocone.obj (liftColimit ((isColimitWhiskerEquiv F c).symm hc))) ≅
    extendCocone.obj (H.mapCocone (liftColimit ((isColimitWhiskerEquiv F c).symm hc)))

Tactic:
exact Cocone.ext (Iso.refl _)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork f g
⊢ c.unop.ι = c.π.unop

Tactic:
by simp [Cofork.unop, Fork.ι]

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

Goal state before:
pp: case refine_2
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
D : J ⥤ C
c : Cocone D
hc : IsColimit c
j : J
inst✝ : (Under.forget j).Final
this : Nonempty (Under j)
c'' : Cocone
  (Under.lift (Under.forget j ⋙ D)
    ((Functor.constComp (Under j) j D).inv ≫ Functor.whiskerRight (Under.forgetCone j).π D)) :=
  Under.liftCocone (Under.forget j ⋙ D)
    ((Functor.constComp (Under j) j D).inv ≫ Functor.whiskerRight (Under.forgetCone j).π D)
    (Cocone.whisker (Under.forget j) c) (c.ι.app j) ⋯
hc'' : IsColimit c'' :=
  Under.isColimitLiftCocone (Under.forget j ⋙ D)
    ((Functor.constComp (Under j) j D).inv ≫ Functor.whiskerRight (Under.forgetCone j).π D)
    (Cocone.whisker (Under.forget j) c) (c.ι.app j) ⋯ ((Functor.Final.isColimitWhiskerEquiv (Under.forget j) c).symm hc)
⊢ (Cocone.precompose
          (NatIso.ofComponents
              (fun k ↦
                Under.isoMk
                  (Iso.refl
                    ((Under.lift (Under.forget j ⋙ D)
                            ((Functor.constComp (Under j) j D).inv ≫ Functor.whiskerRight (Under.forgetCone j).π D)).obj
                        k).right)
                  ⋯)
              ⋯).inv).obj
      c'' ≅
    c.underPost j

Tactic:
exact Cocone.ext (Iso.refl _)

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ Y✝ Y'✝ S✝ : C
f✝ : X✝ ⟶ S✝
g✝ : Y✝ ⟶ S✝
f'✝ : Y'✝ ⟶ Y✝
g'✝ : Y'✝ ⟶ X✝
h₁ : IsPullback f'✝ g'✝ g✝ f✝
h₂ : P g✝
⊢ P g'✝

Tactic:
exact h _ ⟨_, _, _, _, _, h₂, h₁⟩

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ A'✝ B✝ B'✝ : C
f✝ : A✝ ⟶ A'✝
g✝ : A✝ ⟶ B✝
f'✝ : B✝ ⟶ B'✝
g'✝ : A'✝ ⟶ B'✝
h₁ : IsPushout g✝ f✝ f'✝ g'✝
h₂ : P f✝
⊢ P f'✝

Tactic:
exact h _ ⟨_, _, _, _, _, h₂, h₁⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
X₁ X₂ : J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), φ ≫ c₂.π.app j = c₁.π.app j ≫ f.app j
⊢ W.limitsOfShape J φ

Tactic:
by
  obtain rfl : φ = h₂.lift (Cone.mk _ (c₁.π ≫ f)) := h₂.hom_ext (fun j ↦ by simp [hφ])
  exact ⟨_, _, _, _, h₁, _, _, hf⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C✝ : Type u
inst✝⁹ : Category.{v, u} C✝
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CartesianMonoidalCategory C
D : Type u₁
inst✝⁶ : Category.{v₁, u₁} D
inst✝⁵ : CartesianMonoidalCategory D
F : C ⥤ D
E✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} E✝
inst✝³ : CartesianMonoidalCategory E✝
G✝ : D ⥤ E✝
A✝ B A' B' : C
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
A : C
inst✝ : ∀ (B : C), IsIso (prodComparison F A B)
⊢ IsIso (prodComparisonNatTrans F A)

Tactic:
by
  let : ∀ X, IsIso ((prodComparisonNatTrans F A).app X) := by assumption
  apply NatIso.isIso_of_isIso_app

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹⁴ : CommSemiring R
inst✝¹³ : NonUnitalNonAssocSemiring A
inst✝¹² : Module R A
inst✝¹¹ : SMulCommClass R A A
inst✝¹⁰ : IsScalarTower R A A
inst✝⁹ : AddCommMonoid C
inst✝⁸ : Module R C
inst✝⁷ : CoalgebraStruct R C
D : Type u_7
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R B
inst✝⁴ : CoalgebraStruct R B
inst✝³ : NonUnitalNonAssocSemiring D
inst✝² : Module R D
inst✝¹ : SMulCommClass R D D
inst✝ : IsScalarTower R D D
f h : WithConv (C →ₗ[R] A)
g k : WithConv (B →ₗ[R] D)
⊢ toConv
      ((mul' R A ⊗ₘ mul' R D) ∘ₗ
        (↑(tensorTensorTensorComm R A D A D) ∘ₗ ((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ (h.ofConv ⊗ₘ k.ofConv))) ∘ₗ
          ↑(AlgebraTensorModule.tensorTensorTensorComm R R R R C C B B) ∘ₗ (δ ⊗ₘ δ)) =
    toConv (mul' R A ∘ₗ (f.ofConv ⊗ₘ h.ofConv) ∘ₗ δ ⊗ₘ mul' R D ∘ₗ (g.ofConv ⊗ₘ k.ofConv) ∘ₗ δ)

Tactic:
← comp_assoc,

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹⁴ : CommSemiring R
inst✝¹³ : NonUnitalNonAssocSemiring A
inst✝¹² : Module R A
inst✝¹¹ : SMulCommClass R A A
inst✝¹⁰ : IsScalarTower R A A
inst✝⁹ : AddCommMonoid C
inst✝⁸ : Module R C
inst✝⁷ : CoalgebraStruct R C
D : Type u_7
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R B
inst✝⁴ : CoalgebraStruct R B
inst✝³ : NonUnitalNonAssocSemiring D
inst✝² : Module R D
inst✝¹ : SMulCommClass R D D
inst✝ : IsScalarTower R D D
f h : WithConv (C →ₗ[R] A)
g k : WithConv (B →ₗ[R] D)
⊢ toConv
      ((mul' R A ⊗ₘ mul' R D) ∘ₗ
        ((↑(tensorTensorTensorComm R A D A D) ∘ₗ ((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ (h.ofConv ⊗ₘ k.ofConv))) ∘ₗ
            ↑(AlgebraTensorModule.tensorTensorTensorComm R R R R C C B B)) ∘ₗ
          (δ ⊗ₘ δ)) =
    toConv (mul' R A ∘ₗ (f.ofConv ⊗ₘ h.ofConv) ∘ₗ δ ⊗ₘ mul' R D ∘ₗ (g.ofConv ⊗ₘ k.ofConv) ∘ₗ δ)