mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ ∑ i, ∑ j, (↑↑(sign i) * ∏ i_1, A (i i_1) i_1) * (↑↑(sign j) * ∏ i, D (j i) i) =
    ∑ x ∈ (↑(sumCongrHom m n).range).toFinset, ↑↑(sign x) * ∏ i, fromBlocks A B 0 D (x i) i

Tactic:
← sum_product',

Goal state after:
case e'_3
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ ∑ x ∈ univ ×ˢ univ, (↑↑(sign x.1) * ∏ i, A (x.1 i) i) * (↑↑(sign x.2) * ∏ i, D (x.2 i) i) =
    ∑ x ∈ (↑(sumCongrHom m n).range).toFinset, ↑↑(sign x) * ∏ i, fromBlocks A B 0 D (x i) i
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁶ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f f' : MultilinearMap R M₁ M₂
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
m : Fin n → A
i : Fin n
x y : A
⊢ (List.ofFn (update m i (x + y))).prod = (List.ofFn (update m i x)).prod + (List.ofFn (update m i y)).prod

Tactic:
simp [List.ofFn_eq_map, (List.nodup_finRange n).map_update, List.prod_set, add_mul,
        mul_add, add_mul]

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
t : IsLimit c
x : ↑F.sections
j : J
| ↑x j

Tactic:
rw [← (isLimitEquivSections t).right_inv x]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
t : IsLimit c
x : ↑F.sections
j : J
| ↑((isLimitEquivSections t).toFun ((isLimitEquivSections t).invFun x)) j
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommGroup (M₁ i)
inst✝⁴ : AddCommGroup M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x h h' : (i : ι) → M₁ i
⊢ f (x + h) - f (x + h') - (f.linearDeriv x) (h - h') = ∑ s with 2 ≤ #s, (f (s.piecewise h x) - f (s.piecewise h' x))

Tactic:
simp_rw [map_add_eq_map_add_linearDeriv_add, add_assoc, add_sub_add_comm, sub_self, zero_add,
    ← map_sub, add_sub_cancel_left, sum_sub_distrib]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Finite J
val✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
⊢ ∑ j, ((tensorRight X).mapBicone b).π j ≫ ((tensorRight X).mapBicone b).ι j = 𝟙 ((tensorRight X).mapBicone b).pt

Tactic:
dsimp
            simp_rw [← tensorHom_id]
            simp only [tensorHom_comp_tensorHom, Category.comp_id, ← sum_tensor, ← id_tensorHom_id,
               IsBilimit.total i]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Coherence.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
f₁ f₂ f₃ f₄ : C
α α' : f₁ ⟶ f₂
η η' : f₂ ⟶ f₃
ηs ηs' : f₃ ⟶ f₄
e_α : α = α'
e_η : η = η'
e_ηs : ηs = ηs'
⊢ α ≫ η ≫ ηs = α' ≫ η' ≫ ηs'

Tactic:
simp [e_α, e_η, e_ηs]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : HasWidePullbacks Cᵒᵖ
ι : Type w
⊢ HasColimitsOfShape (WidePushoutShape ι) C

Tactic:
← hasLimitsOfShape_opposite_opposite_iff

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : HasWidePullbacks Cᵒᵖ
ι : Type w
⊢ HasLimitsOfShape (WidePushoutShape ι)ᵒᵖ Cᵒᵖ
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : HasFiniteWidePullbacks Cᵒᵖ
J : Type
x✝ : Finite J
⊢ HasColimitsOfShape (WidePushoutShape J) C

Tactic:
← hasLimitsOfShape_opposite_opposite_iff

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : HasFiniteWidePullbacks Cᵒᵖ
J : Type
x✝ : Finite J
⊢ HasLimitsOfShape (WidePushoutShape J)ᵒᵖ Cᵒᵖ
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case leftAdjoint_μ
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
this : G.LaxMonoidal := ⋯
⊢ autoParam
    (∀ (X Y : D),
      μ G X Y =
        adj.unit.app (G.obj X ⊗ G.obj Y) ≫ G.map (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y)))
    IsMonoidal.leftAdjoint_μ._autoParam

Tactic:
intro _ _

Goal state after:
case leftAdjoint_μ
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
this : G.LaxMonoidal := adj.rightAdjointLaxMonoidal
X✝ Y✝ : D
⊢ μ G X✝ Y✝ =
    adj.unit.app (G.obj X✝ ⊗ G.obj Y✝) ≫ G.map (δ F (G.obj X✝) (G.obj Y✝) ≫ (adj.counit.app X✝ ⊗ₘ adj.counit.app Y✝))
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
e : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
⊢ e.functor.map (ε e.inverse) ≫ e.counitIso.hom.app (𝟙_ D) ≫ e.counitIso.inv.app (𝟙_ D) ≫ e.functor.map (η e.inverse) =
    𝟙 (e.functor.obj (𝟙_ C))

Tactic:
Iso.hom_inv_id_app_assoc,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
e : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
⊢ e.functor.map (ε e.inverse) ≫ e.functor.map (η e.inverse) = 𝟙 (e.functor.obj (𝟙_ C))
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
e : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
⊢ e.functor.map (ε e.inverse) ≫ e.counitIso.hom.app (𝟙_ D) ≫ e.counitInv.app (𝟙_ D) ≫ e.functor.map (η e.inverse) =
    𝟙 (e.functor.obj (𝟙_ C))

Tactic:
Iso.hom_inv_id_app_assoc,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
e : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
⊢ e.functor.map (ε e.inverse) ≫ e.functor.map (η e.inverse) = 𝟙 (e.functor.obj (𝟙_ C))
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ : C
⊢ tensorδ X₁ X₂ Y₁ Y₂ ≫ tensorμ X₁ X₂ Y₁ Y₂ = 𝟙 ((X₁ ⊗ Y₁) ⊗ X₂ ⊗ Y₂)

Tactic:
by
  simp only [tensorδ, ← whiskerLeft_comp_assoc, tensorμ, assoc, Iso.inv_hom_id_assoc,
    Iso.hom_inv_id_assoc, inv_hom_whiskerRight_assoc, Iso.inv_hom_id, whiskerLeft_id, id_comp,
    Iso.hom_inv_id]

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
i j : J
f : i ⟶ j
⊢ AddCommGrpCat.ofHom ↑(Hom.hom (F.map f)) ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) i ≫ AddCommGrpCat.ofHom ↑LinearMap.id

Tactic:
erw [colimit.w (F ⋙ forget₂ _ AddCommGrpCat), comp_id]

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

Goal state before:
pp: R✝ : Type w
inst✝⁴ : Ring R✝
J : Type u
inst✝³ : Category.{v, u} J
F : J ⥤ ModuleCat R✝
R : Type w
inst✝² : CommRing R
M ι : Type u
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ (s : Cocone (Discrete.functor fun x ↦ of R M)) (j : Discrete ι),
    (finsuppCocone R M ι).ι.app j ≫ ↟((Finsupp.lsum R) fun i ↦ Hom.hom (s.ι.app { as := i })) = s.ι.app j

Tactic:
by aesop (add simp finsuppCocone)

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
⊢ (Hom.hom (hc.desc (toCocone F f))).comp (desc F c) = f

Tactic:
by
  refine Quot.addMonoidHom_ext F (fun j x ↦ ?_)
  rw [AddMonoidHom.comp_apply, ι_desc]
  change (c.ι.app j ≫ hc.desc (toCocone F f)) _ = _
  rw [hc.fac]
  simp

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 := ⋯
⊢ ∀ (x : ↑((restrictScalars f).obj (of S S))) (y : ↑M),
    (Hom.hom ((restrictScalars f).map α)) (x ⊗ₜ[R] y) = (Hom.hom ((restrictScalars f).map β)) (x ⊗ₜ[R] y)

Tactic:
intro (s : 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
⊢ (Hom.hom ((restrictScalars f).map α)) (s ⊗ₜ[R] m) = (Hom.hom ((restrictScalars f).map β)) (s ⊗ₜ[R] m)
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a - b = a + b

Tactic:
rw [sub_eq_add_neg, add_right_inj, neg_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ (adj1.leftAdjointUniq adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x

Tactic:
← leftAdjointUniq_hom_counit adj1 adj2

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ (adj1.leftAdjointUniq adj2).hom.app (G.obj x) ≫ adj2.counit.app x =
    (G.whiskerLeft (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit).app x
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ ∀ (y x : R), y ∈ univ * s * univ → y * x ∈ univ * s * univ

Tactic:
rintro - x ⟨y, hy, r, -, rfl⟩

Goal state after:
case refine_2
R : Type u_1
inst✝ : Ring R
s : Set R
z x y : R
hy : y ∈ univ * s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) y r * x ∈ univ * s * univ
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h : j = i
⊢ ((Functor.const J).obj (F.1 i)).obj j = F.obj j

Tactic:
cases h; rfl

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
n m : ℕ
h : m ≤ n
⊢ selfZPow x B (↑n - ↑m) = mk' B (x ^ n) (Submonoid.pow x m)

Tactic:
IsLocalization.eq_mk'_iff_mul_eq,

Goal state after:
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
n m : ℕ
h : m ≤ n
⊢ selfZPow x B (↑n - ↑m) * (algebraMap R B) ↑(Submonoid.pow x m) = (algebraMap R B) (x ^ n)
Module: Mathlib.RingTheory.Localization.Module

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
N : Type u_5
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
M' : Type u_3
N' : Type u_4
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g₁
inst✝ : IsLocalizedModule S g₂
l : M →ₗ[R] N
⊢ ((↑(IsLocalizedModule.iso S g₂) ∘ₗ ↑R ((map S) l)) ∘ₗ ↑(IsLocalizedModule.iso S g₁).symm) ∘ₗ g₁ =
    (IsLocalizedModule.map S g₁ g₂) l ∘ₗ g₁

Tactic:
rw [LinearMap.comp_assoc, IsLocalizedModule.iso_symm_comp]

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_5
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
M' : Type u_3
N' : Type u_4
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g₁
inst✝ : IsLocalizedModule S g₂
l : M →ₗ[R] N
⊢ (↑(IsLocalizedModule.iso S g₂) ∘ₗ ↑R ((map S) l)) ∘ₗ mkLinearMap S M = (IsLocalizedModule.map S g₁ g₂) l ∘ₗ g₁
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

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

Tactic:
by rw [s.condition, Category.assoc]

Goal state after:
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 = mk' (S ⊗[R] A) ((algebraMap R S) x * s) ⟨(algebraMap R S) ↑y, ⋯⟩

Tactic:
IsLocalization.eq_mk'_iff_mul_eq,

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] mk' A x y * (algebraMap S (S ⊗[R] A)) ↑⟨(algebraMap R S) ↑y, ⋯⟩ =
    (algebraMap S (S ⊗[R] A)) ((algebraMap R S) x * s)
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
a : α
m : Multiset α
⊢ FreeAbelianGroup.of (Multiplicative.ofAdd (a ::ₘ m)) = of a * FreeAbelianGroup.of (Multiplicative.ofAdd m)

Tactic:
dsimp [FreeCommRing]

Goal state after:
α : Type u
a : α
m : Multiset α
⊢ FreeAbelianGroup.of (Multiplicative.ofAdd (a ::ₘ m)) = of a * FreeAbelianGroup.of (Multiplicative.ofAdd m)
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
i✝ : ℤ
s : Set α
i : ℕ
hi : (↑↑i).IsSupported s
⊢ (↑↑i + ↑1).IsSupported s

Tactic:
Int.cast_one

Goal state after:
α : Type u
i✝ : ℤ
s : Set α
i : ℕ
hi : (↑↑i).IsSupported s
⊢ (↑↑i + 1).IsSupported s
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
i✝ : ℤ
s : Set α
i : ℕ
hi : (↑(-↑i)).IsSupported s
⊢ (↑(-↑i) - ↑1).IsSupported s

Tactic:
Int.cast_one

Goal state after:
α : Type u
i✝ : ℤ
s : Set α
i : ℕ
hi : (↑(-↑i)).IsSupported s
⊢ (↑(-↑i) - 1).IsSupported s
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case h
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ -1 = -↑1

Tactic:
Int.cast_one

Goal state after:
case h
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ -1 = -1
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case right
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Quiver.IsThin C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : Quiver.IsThin D
F : C ⥤ D
inst✝ : PreservesColimitsOfShape (Discrete WalkingPair) F
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
hfg : HasPushout f g
⊢ IsPushout (F.map f) (F.map g) (F.map (pushout.inl f g)) (F.map (pushout.inr f g))

Tactic:
rw [isPushout_iff_isColimit_binaryCofan_of_isThin]

Goal state after:
case right
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Quiver.IsThin C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : Quiver.IsThin D
F : C ⥤ D
inst✝ : PreservesColimitsOfShape (Discrete WalkingPair) F
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
hfg : HasPushout f g
⊢ Nonempty (IsColimit (BinaryCofan.mk (F.map (pushout.inl f g)) (F.map (pushout.inr f g))))
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.μ
⊢ T.map (T.η.app X) = T.η.app (T.obj X)

Tactic:
by
  simp [← cancel_mono (T.μ.app _)]

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
m : M
⊢ (↑(iso S f).symm ∘ₗ f) m = (LocalizedModule.mkLinearMap S M) m

Tactic:
rw [LinearMap.comp_apply, LocalizedModule.mkLinearMap_apply, LinearEquiv.coe_coe, iso_symm_apply']

Goal state after:
case eq1
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
⊢ 1 • f m = f m
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst✝¹ : Algebra ↑R ↑A := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑B := (Hom.hom g).toAlgebra
e : ↑(of (↑A ⊗[↑R] ↑B)) ≃+* ↑X := (IsPushout.isoIsPushout A B ⋯ H).commRingCatIsoToRingEquiv
⊢ Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (Set.range ⇑((Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv).comp (ConcreteCategory.hom a)) ∪
        Set.range ⇑((Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv).comp (ConcreteCategory.hom b)))

Tactic:
← hom_comp,

Goal state after:
R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst✝¹ : Algebra ↑R ↑A := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑B := (Hom.hom g).toAlgebra
e : ↑(of (↑A ⊗[↑R] ↑B)) ≃+* ↑X := (IsPushout.isoIsPushout A B ⋯ H).commRingCatIsoToRingEquiv
⊢ Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (Set.range ⇑(Hom.hom (a ≫ (IsPushout.isoIsPushout A B ⋯ H).inv)) ∪
        Set.range ⇑((Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv).comp (ConcreteCategory.hom b)))
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst✝¹ : Algebra ↑R ↑A := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑B := (Hom.hom g).toAlgebra
e : ↑(of (↑A ⊗[↑R] ↑B)) ≃+* ↑X := (IsPushout.isoIsPushout A B ⋯ H).commRingCatIsoToRingEquiv
⊢ Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (Set.range ⇑(Hom.hom (a ≫ (IsPushout.isoIsPushout A B ⋯ H).inv)) ∪
        Set.range ⇑((Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv).comp (ConcreteCategory.hom b)))

Tactic:
← hom_comp,

Goal state after:
R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst✝¹ : Algebra ↑R ↑A := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑B := (Hom.hom g).toAlgebra
e : ↑(of (↑A ⊗[↑R] ↑B)) ≃+* ↑X := (IsPushout.isoIsPushout A B ⋯ H).commRingCatIsoToRingEquiv
⊢ Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (Set.range ⇑(Hom.hom (a ≫ (IsPushout.isoIsPushout A B ⋯ H).inv)) ∪
        Set.range ⇑(Hom.hom (b ≫ (IsPushout.isoIsPushout A B ⋯ H).inv)))
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cone F
inst✝ : PreservesLimit (F ⋙ snd L R) R
h₁ : IsLimit ((fst L R).mapCone c)
h₂ : IsLimit ((snd L R).mapCone c)
s : Cone F
x✝ : s.pt ⟶ c.pt
hm : ∀ (j : J), x✝ ≫ c.π.app j = s.π.app j
⊢ x✝.right = { left := h₁.lift ((fst L R).mapCone s), right := h₂.lift ((snd L R).mapCone s), w := ⋯ }.right

Tactic:
· exact h₂.uniq ((snd _ _).mapCone s) _ (by simp [← hm])

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I.FG
f : R →+* S
⊢ (Ideal.map f I).FG

Tactic:
by
  classical
    obtain ⟨s, hs⟩ := h
    refine ⟨s.image f, ?_⟩
    rw [Finset.coe_image, ← map_span, hs]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
⊢ ∃ n, I.radical ^ n ≤ I

Tactic:
suffices hJ : ∀ J : Ideal R, J.FG → J ≤ I.radical → ∃ n : ℕ, J ^ n ≤ I by
    simpa using hJ I.radical h
  intro J hJ hJK
  induction J, hJ using Submodule.fg_induction with
  | singleton x =>
    obtain ⟨n, hn⟩ := hJK (subset_span (Set.mem_singleton x))
    exact ⟨n, by rwa [← span, span_singleton_pow, span_le, Set.singleton_subset_iff]⟩
  | sup J K _ _ hJ hK =>
    obtain ⟨n, hn⟩ := hJ fun x hx => hJK <| mem_sup_left hx
    obtain ⟨m, hm⟩ := hK fun x hx => hJK <| mem_sup_right hx
    use n + m
    rw [← add_eq_sup, add_pow, sum_eq_sup, Finset.sup_le_iff]
    refine fun i _ => mul_le_left.trans ?_
    obtain h | h := le_or_gt n i
    · exact mul_le_left.trans ((pow_le_pow_right h).trans hn)
    · exact mul_le_right.trans ((pow_le_pow_right (by lia)).trans hm)

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

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
hIJ : I ≤ J.radical
hJ : J.radical.FG
⊢ ∃ k, I ^ k ≤ J

Tactic:
by
  obtain ⟨k, hk⟩ := J.exists_radical_pow_le_of_fg hJ
  exact ⟨k, (pow_right_mono hIJ k).trans hk⟩

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Under X
F : C ⥤ D
t✝ : Cocone K
t : Cocone (liftFromUnder.obj K)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ K.map f ≫ Under.homMk (t.ι.app (of x✝)) ⋯ =
    Under.homMk (t.ι.app (of x✝¹)) ⋯ ≫ ((Functor.const J).obj (Under.mk (t.ι.app star))).map f

Tactic:
ext; simpa using! t.ι.naturality (incl.map f)

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra R B
inst✝³ : IsScalarTower R A B
inst✝² : IsDomain A
inst✝¹ : Module.IsTorsionFree A B
inst✝ : Nontrivial B
x : σ → A
p : MvPolynomial σ R
⊢ (aeval x) p • 1 = 0 ↔ (aeval x) p = 0

Tactic:
smul_eq_zero,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra R B
inst✝³ : IsScalarTower R A B
inst✝² : IsDomain A
inst✝¹ : Module.IsTorsionFree A B
inst✝ : Nontrivial B
x : σ → A
p : MvPolynomial σ R
⊢ (aeval x) p = 0 ∨ 1 = 0 ↔ (aeval x) p = 0