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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget P
hP' : StableUnderCompositionWithLocalizationAwaySource P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)
hs : Ideal.span (⇑f '' s) = ⊤
r : R
hr : r ∈ s
⊢ P ((IsLocalization.map (Localization.Away ↑⟨f r, ⋯⟩) f ?m.175).comp (algebraMap R (Localization.Away r)))

Tactic:
apply hP' _ r

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget P
hP' : StableUnderCompositionWithLocalizationAwaySource P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)
hs : Ideal.span (⇑f '' s) = ⊤
r : R
hr : r ∈ s
⊢ P (IsLocalization.map (Localization.Away ↑⟨f r, ⋯⟩) f ?m.175)
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
I : Ideal R
⊢ Submodule.localized' S p (Algebra.linearMap R S) I = map (algebraMap R S) I

Tactic:
rw [map, span, Submodule.localized'_eq_span, Algebra.coe_linearMap]

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

Goal state before:
pp: α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix n n α
h : A.IsSymm
f : n ≃ m
⊢ (A.submatrix ⇑f.symm ⇑f.symm).IsSymm

Tactic:
apply submatrix h

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

Goal state before:
pp: α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
⊢ (Matrix.fromBlocks A B C D)ᵀ = Matrix.fromBlocks A B C D

Tactic:
fromBlocks_transpose,

Goal state after:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
⊢ Matrix.fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ (C 1 * T n).degree = ↑n

Tactic:
exact degree_C_mul_T n 1 (one_ne_zero : (1 : R) ≠ 0)

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

Goal state before:
pp: case inl
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i : n
⊢ ((diagonal v).updateCol i (Pi.single i 1)).det = diagonal (fun i ↦ ∏ j ∈ univ.erase i, v j) i i

Tactic:
rw [diagonal_apply_eq, diagonal_updateCol_single, det_diagonal,
      prod_update_of_mem (Finset.mem_univ _), sdiff_singleton_eq_erase, one_mul]

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

Goal state before:
pp: case succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
IH : k ≤ r → (M * (List.take k (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
hk : k + 1 ≤ r
hkr : k < r
k' : Fin r := ⟨k, hkr⟩
⊢ (M * (List.take (k + 1) (listTransvecRow M)).prod) i (inr ()) = M i (inr ())

Tactic:
have :
      (listTransvecRow M)[k]? =
        ↑(transvection (inr Unit.unit) (inl k')
            (-M (inr Unit.unit) (inl k') / M (inr Unit.unit) (inr Unit.unit))) := by
      simp only [k', listTransvecRow, hkr, dif_pos, List.getElem?_ofFn]

Goal state after:
case succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
IH : k ≤ r → (M * (List.take k (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
hk : k + 1 ≤ r
hkr : k < r
k' : Fin r := ⟨k, hkr⟩
this : (listTransvecRow M)[k]? = some (transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
⊢ (M * (List.take (k + 1) (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
val✝ : Fintype n
x✝ : ∃ B, B * A = 1
y : n → R
B : Matrix n m R
hBA : B * A = 1
⊢ (fun v ↦ v ᵥ* A) (y ᵥ* B) = y

Tactic:
by simp [hBA]

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

Goal state before:
pp: case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
val✝ : Fintype n
h : Function.Surjective fun v ↦ v ᵥ* A
⊢ ∃ B, B * A = 1

Tactic:
choose rows hrows using (h <| Pi.single · 1)

Goal state after:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
val✝ : Fintype n
h : Function.Surjective fun v ↦ v ᵥ* A
rows : n → m → R
hrows : ∀ (x : n), (fun v ↦ v ᵥ* A) (rows x) = Pi.single x 1
⊢ ∃ B, B * A = 1
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
x✝ : ∃ B, A * B = 1
y : m → R
B : Matrix n m R
hBA : A * B = 1
⊢ A *ᵥ B *ᵥ y = y

Tactic:
by simp [hBA]

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

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
this : ∀ (hs : Finset α), image b univ = hs → M⁻¹.BlockTriangular b
⊢ M⁻¹.BlockTriangular b

Tactic:
by exact this _ rfl

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

Goal state before:
pp: case pos.inr
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), of (fun i j ↦ M (inl i) (inr j)) i j = 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), of (fun i j ↦ M (inr i) (inl j)) i j = 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
· let M' := M * transvection (inl i) (inr unit) 1
    have hM' : M' (inr unit) (inr unit) ≠ 0 := by simpa [M', hM]
    rcases exists_isTwoBlockDiagonal_of_ne_zero M' hM' with ⟨L, L', hLL'⟩
    refine ⟨L, ⟨inl i, inr unit, by simp, 1⟩::L', ?_⟩
    simp only [← Matrix.mul_assoc, toMatrix_mk, List.prod_cons, List.map]
    rw [Matrix.mul_assoc (L.map toMatrix).prod]
    exact hLL'

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : i = j
⊢ (M.charmatrix i j).coeff k = (X.coeff k - (C M).coeff k) i j

pp: case neg
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ (M.charmatrix i j).coeff k = (X.coeff k - (C M).coeff k) i j

Tactic:
· subst h
    rw [charmatrix_apply_eq, coeff_sub]
    simp only [coeff_X, coeff_C]
    split_ifs <;> simp

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ (M.charmatrix i j).coeff k = (X.coeff k - (C M).coeff k) i j
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M : Matrix n n R
e : n ≃ m
⊢ ((reindex e e) M).charmatrix = (reindex e e) M.charmatrix

Tactic:
ext i j x
  by_cases h : i = j
  all_goals simp [h]

Goal state after:
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
α : Type u_5
inst✝ : Preorder α
M : Matrix n n R
b : n → α
⊢ M.charmatrix.BlockTriangular b ↔ M.BlockTriangular b

Tactic:
rw [charmatrix, scalar_apply, RingHom.mapMatrix_apply, (blockTriangular_diagonal _).sub_iff_right]
  simp [BlockTriangular]

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝² : Field 𝕜
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
this :
  ∀ (cn : ℕ), Fintype.card n = cn → ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
⊢ ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
by exact this _ rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
i k : ℕ
hk : (p + C r) ^ k = 0
⊢ eval 0 p = 0

Tactic:
rwa [coeff_zero_eq_aeval_zero] at hp₀

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

Goal state before:
pp: R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : ∀ (i : ℕ), (C r + X * P).coeff (i + 1) = P.coeff i
⊢ (IsUnit ((C r + X * P).coeff 0) ∧ ∀ (i : ℕ), IsNilpotent (P.coeff i)) ↔ IsUnit r ∧ IsNilpotent P

Tactic:
simp only [coeff_add, coeff_C_zero, mul_coeff_zero, coeff_X_zero, zero_mul, add_zero,
    ← Polynomial.isNilpotent_iff]

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
a b : S
h : IsNilpotent (a - b)
⊢ IsNilpotent ((aeval a) P - (aeval b) P)

Tactic:
simp only [← eval_map_algebraMap]

Goal state after:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
a b : S
h : IsNilpotent (a - b)
⊢ IsNilpotent (eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P))
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : RankCondition R
s : Set M
hs : LinearIndepOn R id s
⊢ (span R s).spanRank = #↑s

Tactic:
simp [← spanRank_span_range_of_linearIndependent Subtype.val_injective hs]

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
hm : m ≠ 0
⊢ (R ∙ m).spanFinrank = 1

Tactic:
by
  apply le_antisymm ?_ ?_
  · exact le_trans (Submodule.spanFinrank_span_le_ncard_of_finite (by simp)) (by simp)
  · by_contra!
    simp [Submodule.spanFinrank_eq_zero_iff_eq_bot (fg_span_singleton m), hm] at this

Goal state after:
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
⊢ (Equiv.Perm.sign c • ∏ i, M.charmatrix (c i) i).coeff k ∈ I ^ (Fintype.card n - k)

Tactic:
coeff_smul,

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
⊢ Equiv.Perm.sign c • (∏ i, M.charmatrix (c i) i).coeff k ∈ I ^ (Fintype.card n - k)
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : ↥A' →ₐ[R] Module.End R ↥N :=
  AlgHom.ofLinearMap { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
this : Function.Injective ⇑f
⊢ IsIntegral R (A'.val ⟨x, hx⟩)

Tactic:
isIntegral_algHom_iff A'.val Subtype.val_injective,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : ↥A' →ₐ[R] Module.End R ↥N :=
  AlgHom.ofLinearMap { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
this : Function.Injective ⇑f
⊢ IsIntegral R ⟨x, hx⟩
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case inr.inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i : { a // a ∉ s }
j : ↥s
⊢ s.piecewise M 1 ↑i ↑j = 0

pp: case inr.inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i j : { a // a ∉ s }
⊢ s.piecewise M 1 ↑i ↑j = 1 i j

Tactic:
· simp only [Finset.piecewise, if_neg i.prop]
      exact Matrix.one_apply_ne (fun h => i.prop (h ▸ j.prop))

Goal state after:
case inr.inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i j : { a // a ∉ s }
⊢ s.piecewise M 1 ↑i ↑j = 1 i j
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case succ.e_a
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) = k ! * (n + k + 1).choose (n + 1) * (n + 1)

Tactic:
mul_comm (k + 1) _,

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
⊢ ↑((i - l).choose k * i.choose l) = ↑((k + l).choose k * i.choose (k + l))

Tactic:
have h1 : l ≤ i := le_of_add_le_right hikl

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
⊢ ↑((i - l).choose k * i.choose l) = ↑((k + l).choose k * i.choose (k + l))
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case e'_6
S : Type u_2
K : Type u_4
inst✝¹ : Semiring S
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ⇑f
r s : S
hr : eval₂ f (f r / f s) p = 0
hs : s ∈ nonZeroDivisors S
a✝ : Nontrivial S
⊢ f r = f r * f s / f s

Tactic:
mul_div_cancel_right₀

Goal state after:
case e'_6
S : Type u_2
K : Type u_4
inst✝¹ : Semiring S
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ⇑f
r s : S
hr : eval₂ f (f r / f s) p = 0
hs : s ∈ nonZeroDivisors S
a✝ : Nontrivial S
⊢ f r = f r

case e'_6.hb
S : Type u_2
K : Type u_4
inst✝¹ : Semiring S
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ⇑f
r s : S
hr : eval₂ f (f r / f s) p = 0
hs : s ∈ nonZeroDivisors S
a✝ : Nontrivial S
⊢ f s ≠ 0
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = ↑i
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = (p.scaleRoots p.leadingCoeff).coeff i

Tactic:
· simp only [coeff_scaleRoots]
    by_cases h' : i < p.degree
    · rw [mul_assoc, ← pow_succ, tsub_right_comm, tsub_add_cancel_of_le]
      rw [le_tsub_iff_left (coe_lt_degree.mp h').le, Nat.succ_le_iff]
      exact coe_lt_degree.mp h'
    · simp [coeff_eq_zero_of_degree_lt (lt_of_le_of_ne (le_of_not_gt h') h)]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
⊢ (ofSubring T p).coeff n = ↑(p.coeff n)

Tactic:
simp only [ofSubring, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, Classical.not_not, ite_eq_left_iff]

Goal state after:
R : Type u_1
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
⊢ p.coeff n = 0 → 0 = ↑(p.coeff n)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: case h
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
this : p ≠ 0
⊢ p.integralNormalization.Monic ∧ eval₂ f (f p.leadingCoeff * x) p.integralNormalization = 0

Tactic:
use monic_integralNormalization this

Goal state after:
case right
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
this : p ≠ 0
⊢ eval₂ f (f p.leadingCoeff * x) p.integralNormalization = 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case neg.refine_2
R : Type u_5
S : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬1 = 0
this : Nontrivial Rₘ
b : Rₘ
hb : (algebraMap R Rₘ) ↑⟨p.leadingCoeff, hM⟩ * b = 1
⊢ eval₂ (IsLocalization.map Sₘ f ⋯) ((algebraMap S Sₘ) x) (Polynomial.map (algebraMap R Rₘ) p) = 0

Tactic:
rw [eval₂_map, IsLocalization.map_comp, ← hom_eval₂ _ f (algebraMap S Sₘ) x]

Goal state after:
case neg.refine_2
R : Type u_5
S : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬1 = 0
this : Nontrivial Rₘ
b : Rₘ
hb : (algebraMap R Rₘ) ↑⟨p.leadingCoeff, hM⟩ * b = 1
⊢ (algebraMap S Sₘ) (eval₂ f x p) = 0
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsIntegralClosure A R B
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S B
inst✝² : IsScalarTower R S B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
x y : S
⊢ mk' A ((algebraMap S B) (x * y)) ⋯ = mk' A ((algebraMap S B) x) ⋯ * mk' A ((algebraMap S B) y) ⋯

Tactic:
simp_rw [← mk'_mul, map_mul]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsIntegralClosure A R B
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S B
inst✝² : IsScalarTower R S B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
x y : S
⊢ mk' A ((algebraMap S B) (x + y)) ⋯ = mk' A ((algebraMap S B) x) ⋯ + mk' A ((algebraMap S B) y) ⋯

Tactic:
← mk'_add,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsIntegralClosure A R B
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S B
inst✝² : IsScalarTower R S B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
x y : S
⊢ mk' A ((algebraMap S B) (x + y)) ⋯ = mk' A ((algebraMap S B) x + (algebraMap S B) y) ⋯
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case h
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
n : N
hn : n ≠ 0
I : Ideal R := (R ∙ n).annihilator
I_ne_top : ¬I = ⊤
inc : R ⧸ I →ₗ[R] N := Submodule.liftQ I ((LinearMap.lsmul R N).flip n) ⋯
r : R
hr : Quotient.mk'' r ∈ inc.ker
⊢ Quotient.mk'' r ∈ ⊥

Tactic:
| h r =>

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

Goal state before:
pp: case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
m : Ideal R
left✝ : m.IsMaximal
hm : I ≤ m
x✝ : Algebra R S := f.toAlgebra
⊢ ¬map f I = ⊤

Tactic:
have : Algebra.IsIntegral _ _ := ⟨hf₂⟩

Goal state after:
case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
m : Ideal R
left✝ : m.IsMaximal
hm : I ≤ m
x✝ : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
⊢ ¬map 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
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
⊢ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range = ⊤

Tactic:
LinearMap.range_eq_top

Goal state after:
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
⊢ Function.Surjective ⇑(TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id)