mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
S : Cocone I.multispan
a : J.L
⊢ K.ι.app (WalkingMultispan.left a) ≫ desc S = S.ι.app (WalkingMultispan.left a)

pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
S : Cocone I.multispan
b : J.R
⊢ K.ι.app (WalkingMultispan.right b) ≫ desc S = S.ι.app (WalkingMultispan.right b)

Tactic:
· rw [← K.w (WalkingMultispan.Hom.fst a), ← S.w (WalkingMultispan.Hom.fst a),
          Category.assoc]
        congr 1
        apply fac

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
S : Cocone I.multispan
b : J.R
⊢ K.ι.app (WalkingMultispan.right b) ≫ desc S = S.ι.app (WalkingMultispan.right b)
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case one
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
hᵣ : StructuredArrow.mk right ∈ p
⊢ ∀ (j : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair), j ∈ p

Tactic:
rintro ⟨⟨⟨⟩⟩, (_ | _), ⟨_⟩⟩

Goal state after:
case one.zero.leftCompReflexion
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
hᵣ : StructuredArrow.mk right ∈ p
⊢ { left := { as := PUnit.unit }, right := zero, hom := leftCompReflexion } ∈ p

case one.zero.rightCompReflexion
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
hᵣ : StructuredArrow.mk right ∈ p
⊢ { left := { as := PUnit.unit }, right := zero, hom := rightCompReflexion } ∈ p

case one.zero.id
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
hᵣ : StructuredArrow.mk right ∈ p
⊢ { left := { as := PUnit.unit }, right := zero,
      hom := Hom.id ((Functor.fromPUnit WalkingReflexivePair.one).obj { as := PUnit.unit }) } ∈
    p

case one.one.left
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
hᵣ : StructuredArrow.mk right ∈ p
⊢ { left := { as := PUnit.unit }, right := one, hom := left } ∈ p

case one.one.right
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
hᵣ : StructuredArrow.mk right ∈ p
⊢ { left := { as := PUnit.unit }, right := one, hom := right } ∈ p
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Submodule R M
hS : S.IsPrimary
m : M
inst✝ : Decidable (m ∈ S)
hm : m ∉ S
⊢ (S.colon {m}).radical = (S.colon Set.univ).radical

Tactic:
exact hS.radical_colon_singleton_of_notMem hm

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
h : ∃ s_1, s_1 • t • i = s_1 • s • j
⊢ ∃ m, (m ∈ M' ∧ m ∈ M'') ∧ ∃ s, IsLocalizedModule.mk' f m s = x

Tactic:
obtain ⟨k, hk⟩ := h

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
⊢ ∃ m, (m ∈ M' ∧ m ∈ M'') ∧ ∃ s, IsLocalizedModule.mk' f m s = x
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : (Ideal.under R I).IsMaximal
⊢ Function.Surjective ⇑(Ideal.quotientMap I (algebraMap R S) H)

Tactic:
intro s
  obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective s
  obtain ⟨r, ⟨m, hm⟩, rfl⟩ := exists_mk'_eq M s
  by_cases hM : (Ideal.Quotient.mk (I.comap (algebraMap R S))) m = 0
  · have : I = ⊤ := by
      rw [Ideal.eq_top_iff_one]
      rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_comap] at hM
      convert! I.mul_mem_right (mk' S (1 : R) ⟨m, hm⟩) hM
      rw [← mk'_eq_mul_mk'_one, mk'_self]
    exact ⟨0, eq_comm.1 (by simp [Ideal.Quotient.eq_zero_iff_mem, this])⟩
  · rw [Ideal.Quotient.maximal_ideal_iff_isField_quotient] at hI
    obtain ⟨n, hn⟩ := hI.3 hM
    obtain ⟨rn, rfl⟩ := Ideal.Quotient.mk_surjective n
    refine ⟨(Ideal.Quotient.mk J) (r * rn), ?_⟩
    -- The rest of the proof is essentially just algebraic manipulations to prove the equality
    replace hn := congr_arg (Ideal.quotientMap I (algebraMap R S) le_rfl) hn
    rw [map_one, map_mul] at hn
    rw [Ideal.quotientMap_mk, ← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem, ←
      Ideal.Quotient.eq_zero_iff_mem, map_sub, sub_eq_zero, mk'_eq_mul_mk'_one]
    simp only [mul_eq_mul_left_iff, map_mul]
    refine
      Or.inl
        (mul_left_cancel₀ (M₀ := S ⧸ I)
          (fun hn =>
            hM
              (Ideal.Quotient.eq_zero_iff_mem.2
                (Ideal.mem_comap.2 (Ideal.Quotient.eq_zero_iff_mem.1 hn))))
          (_root_.trans hn ?_))
    rw [← map_mul, ← mk'_eq_mul_mk'_one, mk'_self, map_one]

Goal state after:
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
y : ↥(localizationLocalizationSubmodule M N)
⊢ IsUnit ((algebraMap R T) ↑y)

Tactic:
by
  obtain ⟨y', z, eq⟩ := mem_localizationLocalizationSubmodule.mp y.prop
  rw [IsScalarTower.algebraMap_apply R S T, eq, map_mul, IsUnit.mul_iff]
  exact ⟨IsLocalization.map_units T y', (IsLocalization.map_units _ z).map (algebraMap S T)⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
⊢ J = Ideal.comap (↑f.symm) (Ideal.comap f J)

Tactic:
← Ideal.comap_coe f,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
⊢ J = Ideal.comap (↑f.symm) (Ideal.comap (↑f) J)
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
⊢ (coeSubmodule S I).IsPrincipal ↔ Submodule.IsPrincipal I

Tactic:
constructor <;> rintro ⟨⟨x, hx⟩⟩

Goal state after:
case mp
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : S
hx : coeSubmodule S I = R ∙ x
⊢ Submodule.IsPrincipal I

case mpr
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
hx : I = R ∙ x
⊢ (coeSubmodule S I).IsPrincipal
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case hs
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
⊢ Set.EqOn ⇑(f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
    ⇑(g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S)) {x | ↑x ∈ finset R S}

Tactic:
rintro ⟨x, hx⟩ hx'; exact H x hx'

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ (∑ x ∈ s, A.cramer fun j ↦ f j x) i = A.cramer (fun j ↦ ∑ x ∈ s, f j x) i

Tactic:
sum_cramer,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ A.cramer (∑ x ∈ s, fun j ↦ f j x) i = A.cramer (fun j ↦ ∑ x ∈ s, f j x) i
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule R⁰ M) → M
hw : LinearIndependent R w
⊢ #↑(Set.range w) = Module.rank R M

Tactic:
apply Cardinal.lift_injective.{max uR uM}

Goal state after:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule R⁰ M) → M
hw : LinearIndependent R w
⊢ lift.{max uR uM, uM} #↑(Set.range w) = lift.{max uR uM, uM} (Module.rank R M)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
m : Type u_4
a : m
b : n
hb : b ≠ j
c : R
M : Matrix m n R
⊢ (M * transvection i j c) a b = M a b

Tactic:
by simp [transvection, Matrix.mul_add, hb]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case cons
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod = 1
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) (t :: L).reverse).prod * (List.map toMatrix (t :: L)).prod = 1

Tactic:
suffices
      (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod * (t.inv.toMatrix * t.toMatrix) *
          (L.map toMatrix).prod = 1
      by simpa [Matrix.mul_assoc]

Goal state after:
case cons
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod = 1
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (t.inv.toMatrix * t.toMatrix) *
      (List.map toMatrix L).prod =
    1
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.det ^ Fintype.card n = A'.det ^ (Fintype.card n - 1 + 1)

Tactic:
h_card

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.det ^ Fintype.card n = A'.det ^ Fintype.card n
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible A.det
⊢ (⅟A).det = ⅟A.det

Tactic:
let := detInvertibleOfInvertible A
  convert! (rfl : _ = ⅟A.det)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
⊢ (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))

Tactic:
simp only [n', listTransvecRow, hnr, dif_pos, List.getElem?_ofFn]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ ⅟(diagonal v).det * (v i * ∏ j ∈ univ.erase i, v j) = 1

Tactic:
mul_prod_erase _ _ (Finset.mem_univ _),

Goal state after:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ ⅟(diagonal v).det * ∏ x, v x = 1
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
⊢ k ∈ image b univ

Tactic:
apply max'_mem

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
⊢ A.det • b ᵥ* A⁻¹ = Aᵀ.cramer b

Tactic:
by
  rw [← A⁻¹.transpose_transpose, vecMul_transpose, transpose_nonsing_inv, ← det_transpose,
    Aᵀ.det_smul_inv_mulVec_eq_cramer _ (isUnit_det_transpose A h)]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) ^ (n + 2) = x ^ (n + 2) + ↑(n + 2) * x ^ (n + 2 - 1) * y + (x * z + (↑n + 1) * x ^ n + z * y) * y ^ 2

Tactic:
calc
      (x + y) ^ (n + 2) = (x + y) * (x + y) ^ (n + 1) := by ring
      _ = (x + y) * (x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2) := by rw [hz]
      _ = x ^ (n + 2) + ↑(n + 2) * x ^ (n + 1) * y + (x * z + (n + 1) * x ^ n + z * y) * y ^ 2 := by
        push_cast
        ring!

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ ¬IsNilpotent (-1)

Tactic:
intro h
  simpa [not_isNilpotent_one] using h.neg

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i j : n
h : i = j
⊢ (M.charmatrix i j).natDegree ≤ 1

Tactic:
simp [h, natDegree_X_le]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i j : n
h : ¬i = j
⊢ (M.charmatrix i j).natDegree ≤ 0

Tactic:
simp [h, natDegree_X_le]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case mpr
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
hr : ∃ s, s.Finite ∧ IsIntegral (↥(Subring.closure s)) r
⊢ IsIntegral R r

Tactic:
rcases hr with ⟨s, _, hsr⟩

Goal state after:
case mpr
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
s : Set R
left✝ : s.Finite
hsr : IsIntegral (↥(Subring.closure s)) r
⊢ IsIntegral R r
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case e'_3
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ 1 = eval 0 1

Tactic:
eval_one

Goal state after:
case e'_3
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ 1 = 1
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hl : (monomial n) s ∈ lifts f
h : s ≠ 0
⊢ ∃ q, map f q = (monomial n) s ∧ q.degree = ((monomial n) s).degree

Tactic:
obtain ⟨a, rfl⟩ := coeff_monomial_same n s ▸ (monomial n s).lifts_iff_coeff_lifts.mp hl n

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
hl : (monomial n) (f a) ∈ lifts f
h : f a ≠ 0
⊢ ∃ q, map f q = (monomial n) (f a) ∧ q.degree = ((monomial n) (f a)).degree
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
⊢ (∏ i, M.charmatrix (c i) i).coeff k ∈ I ^ (Fintype.card n - k)

Tactic:
have : ∑ x : n, 1 = Fintype.card n := by rw [Finset.sum_const, card_univ, smul_eq_mul, mul_one]

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x, 1 = Fintype.card n
⊢ (∏ i, M.charmatrix (c i) i).coeff k ∈ I ^ (Fintype.card n - k)
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.comp X = f

Tactic:
comp_X

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f = f
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
⊢ (∑ s, D (s.piecewise (fun i ↦ (X • M.map ⇑C) i) fun i ↦ 1 i)).coeff k =
    (∑ s, X ^ #s • D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i)).coeff k

Tactic:
by
        congr 2 with s
        have h_smul : s.piecewise (fun i ↦ ((X : R[X]) • M.map C) i)
            (fun i ↦ (1 : Matrix n n R[X]) i) =
            fun i => (if i ∈ s then (X : R[X]) else 1) •
              s.piecewise (fun i ↦ (M.map C) i) (fun i ↦ (1 : Matrix n n R[X]) i) i := by
          funext i j
          simp only [piecewise, Pi.smul_apply, smul_eq_mul, ite_mul, one_mul]
          split_ifs <;> rfl
        rw [h_smul, D.map_smul_univ]
        congr 1
        simp only [Finset.prod_ite_mem, Finset.univ_inter, Finset.prod_const]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
hp : ¬p = 0
⊢ ((taylor r) p).degree = p.degree

Tactic:
degree_eq_natDegree hp,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
hp : ¬p = 0
⊢ ((taylor r) p).degree = ↑p.natDegree