mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
α : R
hα : α ∉ p
hαx : α • x ∈ pS
β γ : R
hγ : γ ∈ p
hβ : β * α = 1 + γ
this : x + γ • x ∈ pS
⊢ x ∈ pS

Tactic:
refine (Submodule.add_mem_iff_left pS ?_).mp this

Goal state after:
S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
α : R
hα : α ∉ p
hαx : α • x ∈ pS
β γ : R
hγ : γ ∈ p
hβ : β * α = 1 + γ
this : x + γ • x ∈ pS
⊢ γ • x ∈ pS
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝ : InvolutiveStar α
A : Matrix n n α
⊢ Aᴴ.IsSymm ↔ A.IsSymm

Tactic:
by
  refine ⟨fun h ↦ ?_, (·.conjTranspose)⟩
  rw [← A.conjTranspose_conjTranspose]
  exact h.conjTranspose

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ p.coeff a = (∑ i ∈ p.coeff.support, Finsupp.single i (p.coeff i)) a

Tactic:
Finset.sum_apply',

Goal state after:
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ p.coeff a = ∑ k ∈ p.coeff.support, (Finsupp.single k (p.coeff k)) a
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case mul_T.succ
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
hn : Q (toLaurent f * T (-↑n))
⊢ Q (toLaurent f * T (-↑(n + 1)))

Tactic:
| succ n hn =>

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 α
⊢ A.adjugateᵀ = Aᵀ.adjugate

Tactic:
ext i j
  rw [transpose_apply, adjugate_apply, adjugate_apply, updateRow_transpose, det_transpose]
  rw [det_apply', det_apply']
  apply Finset.sum_congr rfl
  intro σ _
  congr 1
  by_cases h : i = σ j
  · -- Everything except `(i, j)` (= `(σ j, j)`) is given by A, and the rest is a single `1`.
    congr
    ext j'
    subst h
    have : σ j' = σ j ↔ j' = j := σ.injective.eq_iff
    rw [updateRow_apply, updateCol_apply]
    simp_rw [this]
    rw [← dite_eq_ite, ← dite_eq_ite]
    congr 1 with rfl
    rw [Pi.single_eq_same, Pi.single_eq_same]
  · -- Otherwise, we need to show that there is a `0` somewhere in the product.
    have : (∏ j' : n, updateCol A j (Pi.single i 1) (σ j') j') = 0 := by
      apply prod_eq_zero (mem_univ j)
      rw [updateCol_self, Pi.single_eq_of_ne' h]
    rw [this]
    apply prod_eq_zero (mem_univ (σ⁻¹ i))
    simp only [Perm.coe_inv, apply_symm_apply, updateRow_self]
    apply Pi.single_eq_of_ne
    intro h'
    exact h ((symm_apply_eq σ).mp h')

Goal state after:
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
b : m
c : R
M : Matrix n m R
⊢ (transvection i j c * M) i b = M i b + c * M j b

Tactic:
simp [transvection, Matrix.add_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : IsDomain R
inst✝ : StrongRankCondition R
h : IsEmpty (OreLocalization.OreSet R⁰)
this : ℵ₀ ≤ Module.rank R R
⊢ False

Tactic:
rw [rank_self] at this

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : IsDomain R
inst✝ : StrongRankCondition R
h : IsEmpty (OreLocalization.OreSet R⁰)
this : ℵ₀ ≤ 1
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 - U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A - U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A =
    1 + U * C * V * ⅟A - (U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A)

Tactic:
abel

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

Goal state before:
pp: n : Type u_3
R : Type u_6
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : AddCommMonoidWithOne R
⊢ trace 1 = ↑(Fintype.card n)

Tactic:
simp_rw [trace, diag_one, Pi.one_def, Finset.sum_const, nsmul_one, Finset.card_univ]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 + U * C * V * ⅟A - U * C * V * ⅟A = 1

Tactic:
abel

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V + ⅟A * U * C * V - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V =
    1 + ⅟A * U * C * V - (⅟A * U * ⅟(⅟C + V * ⅟A * U) * V + ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V)

Tactic:
abel

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 + ⅟A * U * C * V - ⅟A * U * C * V = 1

Tactic:
abel

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

Goal state before:
pp: case self
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
⊢ M (inl i) (inr ()) = if r ≤ ↑i then 0 else M (inl i) (inr ())

Tactic:
rw [if_neg]

Goal state after:
case self.hnc
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
⊢ ¬r ≤ ↑i
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✝ : StarRing α
⊢ star A.det⁻¹ʳ • A.adjugateᴴ = (star A.det)⁻¹ʳ • Aᴴ.adjugate

Tactic:
adjugate_conjTranspose,

Goal state after:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : StarRing α
⊢ star A.det⁻¹ʳ • Aᴴ.adjugate = (star A.det)⁻¹ʳ • Aᴴ.adjugate
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
α : Type v
inst✝³ : CommRing α
inst✝² : Subsingleton m
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
⊢ (diagonal fun x ↦ A.det⁻¹ʳ) = diagonal fun i ↦ (A i i)⁻¹ʳ

Tactic:
congr! with i

Goal state after:
m : Type u
α : Type v
inst✝³ : CommRing α
inst✝² : Subsingleton m
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
i : m
⊢ A.det = A i i
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
val✝¹ : Invertible A
val✝ : Invertible C
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

Tactic:
obtain ⟨iAC⟩ := hAC.nonempty_invertible

Goal state after:
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
val✝¹ : Invertible A
val✝ : Invertible C
iAC : Invertible (C⁻¹ + V * A⁻¹ * U)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
val✝¹ : Invertible A
val✝ : Invertible C
iAC : Invertible (C⁻¹ + V * A⁻¹ * U)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

Tactic:
simp only [← invOf_eq_nonsing_inv] at iAC

Goal state after:
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
val✝¹ : Invertible A
val✝ : Invertible C
iAC : Invertible (⅟C + V * ⅟A * U)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case H.inr
α : 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' ⋯
⊢ ∀ (i : m), b i = k → ∀ (j : m), ¬b j = k → M i j = 0

Tactic:
intro i hi j hj

Goal state after:
case H.inr
α : 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' ⋯
i : m
hi : b i = k
j : m
hj : ¬b j = k
⊢ M i j = 0
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (↑h.unit⁻¹ * N * ↑h.unit).trace = N.trace

Tactic:
trace_units_conj'

Goal state after:
m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ N.trace = N.trace
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval M (Polynomial.map (algebraMap R (Matrix n n R)) M.charpoly) = 0
⊢ (aeval M) M.charpoly = 0

Tactic:
eval_map

Goal state after:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval₂ (algebraMap R (Matrix n n R)) M M.charpoly = 0
⊢ (aeval M) M.charpoly = 0
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 : ℕ
inst✝ : CommRing R
x y : R
k : ℕ
⊢ { z // x ^ (k + 2) - y ^ (k + 2) = z * (x - y) }

Tactic:
obtain ⟨z, hz⟩ := @powSubPowFactor x y (k + 1)

Goal state after:
R : Type u
S : Type v
T : Type w
ι : Type x
k✝ : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
x y : R
k : ℕ
z : R
hz : x ^ (k + 1) - y ^ (k + 1) = z * (x - y)
⊢ { z // x ^ (k + 2) - y ^ (k + 2) = z * (x - y) }
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ toENat (⨅ s, #↑↑s) ≤ ⨅ s, ⨅ (_ : span R s = p), s.encard

Tactic:
refine le_iInf₂ (fun s hs ↦ ?_)

Goal state after:
case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
s : Set M
hs : span R s = p
⊢ toENat (⨅ s, #↑↑s) ≤ s.encard
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

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

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 ⟨p, hmp, hpr⟩
    refine ⟨_, Finset.finite_toSet _, p.restriction, monic_restriction.2 hmp, ?_⟩
    rw [← aeval_def, ← aeval_map_algebraMap R r p.restriction, map_restriction, aeval_def, hpr]

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
hr : ∃ s, s.Finite ∧ IsIntegral (↥(Subring.closure s)) r
⊢ IsIntegral R r
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic

Tactic:
rw [lifts_iff_coeff_lifts] at hlifts
  let g : ℕ → R := fun k ↦ (hlifts k).choose
  have hg k : f (g k) = p.coeff k := (hlifts k).choose_spec
  let q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
  have hq : map f q = p := by
    simp_rw [q, Polynomial.map_add, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_pow,
      map_X, map_C, hg, ← hp.as_sum]
  have h : q.Monic := monic_X_pow_add (by simp_rw [← Fin.sum_univ_eq_sum_range, degree_sum_fin_lt])
  exact ⟨q, hq, hq ▸ (h.degree_map f).symm, h⟩

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * (↑((n + k + 1).choose (k + 1)) * f.coeff (n + k + 1)) =
    ↑k ! * (↑((n + k + 1).choose (n + 1)) * (f.coeff (n + k + 1) * ↑(n + 1)))

Tactic:
← (cast_commute (n + 1) (f.coeff (n + k + 1))).eq

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k !) * (↑((n + k + 1).choose (k + 1)) * f.coeff (n + k + 1)) =
    ↑k ! * (↑((n + k + 1).choose (n + 1)) * (↑(n + 1) * f.coeff (n + k + 1)))
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ (taylor r) f = 0 ↔ f = 0

Tactic:
← leadingCoeff_eq_zero,

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ((taylor r) f).leadingCoeff = 0 ↔ f = 0
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ((taylor r) f).leadingCoeff = 0 ↔ f = 0

Tactic:
← leadingCoeff_eq_zero,

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ((taylor r) f).leadingCoeff = 0 ↔ f.leadingCoeff = 0
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p q : R[X]
r : R
inst✝ : NoZeroDivisors R
hpq : p ∣ q
⊢ p.scaleRoots r ∣ q.scaleRoots r

Tactic:
by
  obtain ⟨a, rfl⟩ := hpq
  rw [mul_scaleRoots_of_noZeroDivisors]
  exact dvd_mul_right (scaleRoots p r) (scaleRoots a r)

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

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective ⇑f
a : R
ha : IsUnit (f a)
p : R[X]
p_monic : p.Monic
hp : eval₂ f (↑ha.unit⁻¹) p = 0
⊢ IsUnit a

Tactic:
refine .of_mul_eq_one (-p.reverse.divX.eval a) ?_

Goal state after:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective ⇑f
a : R
ha : IsUnit (f a)
p : R[X]
p_monic : p.Monic
hp : eval₂ f (↑ha.unit⁻¹) p = 0
⊢ a * -eval a p.reverse.divX = 1
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
⊢ ∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)

Tactic:
have quotient_f : ∀ x ∈ I.comap f, (Ideal.Quotient.mk I).comp f x = 0 := by
    simp [Quotient.eq_zero_iff_mem]

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0
⊢ ∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Nontrivial N
⊢ Nontrivial (N ⊗[R] M)

Tactic:
obtain ⟨n, hn⟩ := nontrivial_iff_exists_ne (0 : N) |>.1 inferInstance
  let I := (Submodule.span R {n}).annihilator
  by_cases I_ne_top : I = ⊤
  · rw [Ideal.eq_top_iff_one, Submodule.mem_annihilator_span_singleton, one_smul] at I_ne_top
    contradiction
  let inc : R ⧸ I →ₗ[R] N := Submodule.liftQ _ ((LinearMap.lsmul R N).flip n) <| fun r hr => by
    simpa only [LinearMap.mem_ker, LinearMap.flip_apply, LinearMap.lsmul_apply,
      Submodule.mem_annihilator_span_singleton, I] using hr
  have injective_inc : Function.Injective inc := LinearMap.ker_eq_bot.1 <| eq_bot_iff.2 <| by
    intro r hr
    induction r using Quotient.inductionOn' with | h r =>
    simpa only [Submodule.Quotient.mk''_eq_mk, Submodule.mem_bot, Submodule.Quotient.mk_eq_zero,
      Submodule.mem_annihilator_span_singleton, LinearMap.mem_ker, Submodule.liftQ_apply,
      LinearMap.flip_apply, LinearMap.lsmul_apply, I, inc] using hr
  have ne_top := iff_flat_and_proper_ideal R M |>.1 fl |>.2 I I_ne_top
  refine subsingleton_or_nontrivial _ |>.resolve_left fun rid => ne_top ?_
  rw [← Submodule.Quotient.subsingleton_iff]
  exact (fl.toFlat.rTensor_preserves_injective_linearMap inc injective_inc).comp
    (quotTensorEquivQuotSMul M I).symm.injective |>.subsingleton

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
⊢ (∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x) →
    Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)

Tactic:
· refine fun H y ↦ Localization.ind (fun ⟨y, t, h⟩ ↦ ?_) y
    simp only
    obtain ⟨yx, ys, yc, hyc, hy, ey⟩ := H y
    obtain ⟨tx, ts, yt, hyt, ht, et⟩ := H t
    refine ⟨Localization.mk (yx * ts) ⟨ys * tx, Submonoid.mul_mem _ hy ?_⟩, ?_⟩
    · exact fun H ↦ mul_mem (P.primeCompl.mul_mem hyt ht) h (et ▸ Ideal.mul_mem_left _ yt H)
    · simp only [Localization.mk_eq_mk', Localization.localRingHom_mk', map_mul f,
        IsLocalization.mk'_eq_iff_eq, IsLocalization.eq_iff_exists P.primeCompl]
      refine ⟨⟨yc, hyc⟩ * ⟨yt, hyt⟩, ?_⟩
      simp only [Submonoid.coe_mul]
      convert! congr($(ey.symm) * $(et)) using 1 <;> ring

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalRing A
inst✝² : IsLocalRing B
inst✝¹ : Flat A B
inst✝ : IsLocalHom (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
⊢ Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)) ≠ ⊤

Tactic:
by_contra eqt

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalRing A
inst✝² : IsLocalRing B
inst✝¹ : Flat A B
inst✝ : IsLocalHom (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
eqt : Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)) = ⊤
⊢ False
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
I : Ideal R
inst✝ : I.IsPrime
x s : R
hs : s ∈ I.primeCompl
⊢ (IsLocalRing.residue (Localization.AtPrime I)) (IsLocalization.mk' (Localization.AtPrime I) x ⟨s, hs⟩) *
      (algebraMap (R ⧸ I) I.ResidueField) ↑((Ideal.Quotient.mk I) x, ⟨(Ideal.Quotient.mk I) s, ⋯⟩).2 =
    (algebraMap (R ⧸ I) I.ResidueField) ((Ideal.Quotient.mk I) x, ⟨(Ideal.Quotient.mk I) s, ⋯⟩).1

Tactic:
simp [IsScalarTower.algebraMap_eq R (Localization.AtPrime I) I.ResidueField, ← map_mul]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑(SemilatticeSup.sup aᶜ bᶜ)ᶜ).1 * (↑a).1 = (↑(SemilatticeSup.sup aᶜ bᶜ)ᶜ).1

Tactic:
(·ᶜ),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑(SemilatticeSup.sup ⟨((↑a).2, (↑a).1), ⋯⟩ ⟨((↑b).2, (↑b).1), ⋯⟩)).2 * (↑a).1 =
    (↑(SemilatticeSup.sup ⟨((↑a).2, (↑a).1), ⋯⟩ ⟨((↑b).2, (↑b).1), ⋯⟩)).2
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑(SemilatticeSup.sup aᶜ bᶜ)ᶜ).1 * (↑b).1 = (↑(SemilatticeSup.sup aᶜ bᶜ)ᶜ).1

Tactic:
(·ᶜ),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑(SemilatticeSup.sup ⟨((↑a).2, (↑a).1), ⋯⟩ ⟨((↑b).2, (↑b).1), ⋯⟩)).2 * (↑b).1 =
    (↑(SemilatticeSup.sup ⟨((↑a).2, (↑a).1), ⋯⟩ ⟨((↑b).2, (↑b).1), ⋯⟩)).2
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : a ≤ b
hac : a ≤ c
⊢ (↑a).1 * (↑(SemilatticeSup.sup bᶜ cᶜ)ᶜ).1 = (↑a).1

Tactic:
(·ᶜ),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : a ≤ b
hac : a ≤ c
⊢ (↑a).1 * (↑(SemilatticeSup.sup ⟨((↑b).2, (↑b).1), ⋯⟩ ⟨((↑c).2, (↑c).1), ⋯⟩)).2 = (↑a).1