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

Goal state before:
pp: 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✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
h : EssFiniteType R S
⊢ EssFiniteType T (T ⊗[R] S)

Tactic:
rw [essFiniteType_iff] at h ⊢
  obtain ⟨σ, hσ⟩ := h
  use σ.image Algebra.TensorProduct.includeRight
  intro s
  induction s using TensorProduct.induction_on with
  | zero => exact ⟨1, one_mem _, isUnit_one, by simp⟩
  | tmul x y =>
    obtain ⟨t, h₁, h₂, h₃⟩ := hσ y
    have H (x : S) (hx : x ∈ Algebra.adjoin R (σ : Set S)) :
        1 ⊗ₜ[R] x ∈ Algebra.adjoin T
          ((σ.image Algebra.TensorProduct.includeRight : Finset (T ⊗[R] S)) : Set (T ⊗[R] S)) := by
      have : Algebra.TensorProduct.includeRight x ∈
          (Algebra.adjoin R (σ : Set S)).map (Algebra.TensorProduct.includeRight (A := T)) :=
        Subalgebra.mem_map.mpr ⟨_, hx, rfl⟩
      rw [← Algebra.adjoin_adjoin_of_tower R]
      apply Algebra.subset_adjoin
      simpa [← Algebra.adjoin_image] using this
    refine ⟨Algebra.TensorProduct.includeRight t, H _ h₁, h₂.map _, ?_⟩
    simp only [Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul,
      mul_one]
    rw [← mul_one x, ← smul_eq_mul, ← TensorProduct.smul_tmul']
    apply Subalgebra.smul_mem
    exact H _ h₃
  | add x y hx hy =>
    obtain ⟨tx, hx₁, hx₂, hx₃⟩ := hx
    obtain ⟨ty, hy₁, hy₂, hy₃⟩ := hy
    refine ⟨_, mul_mem hx₁ hy₁, hx₂.mul hy₂, ?_⟩
    rw [add_mul, ← mul_assoc, mul_comm tx ty, ← mul_assoc]
    exact add_mem (mul_mem hx₃ hy₁) (mul_mem hy₃ hx₁)

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).EssFiniteType ↔ Algebra.EssFiniteType R S

Tactic:
rw [RingHom.EssFiniteType, toAlgebra_algebraMap]

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:
hD

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 B C D = Matrix.fromBlocks A B C D
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (∑ σ, sign σ • ∏ i, (X • A.map ⇑C + B.map ⇑C) (σ i) i).coeff 0 = B.det

Tactic:
finsetSum_coeff,

Goal state after:
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∑ b, (sign b • ∏ i, (X • A.map ⇑C + B.map ⇑C) (b i) i).coeff 0 = B.det
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
M : Type uM
N : Type uN
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
hp : p ≤ R⁰
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)

Tactic:
cases subsingleton_or_nontrivial R
  · simp only [rank_subsingleton, lift_one]
  apply le_antisymm <;>
    rw [Module.rank_def, lift_iSup bddAbove_of_small] <;>
    apply ciSup_le' <;>
    intro ⟨s, hs⟩
  exacts [(IsLocalizedModule.linearIndependent_lift p f hs).choose_spec.cardinal_lift_le_rank,
    hs.of_isLocalizedModule_of_isRegular p f (le_nonZeroDivisors_iff_isRegular.mp hp)
      |>.cardinal_lift_le_rank]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (p q : R[X]), trunc (toLaurent p) = p → trunc (toLaurent q) = q → trunc (toLaurent (p + q)) = p + q

Tactic:
intro f g hf hg
    simp only [hf, hg, map_add]

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 α
b : n → α
i : n
h : ∀ (j : n), b j = A j i
⊢ A.cramer b = Pi.single i A.det

Tactic:
rw [← transpose_transpose A, det_transpose]

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i : n
h : ∀ (j : n), b j = A j i
⊢ Aᵀᵀ.cramer b = Pi.single i Aᵀ.det
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
n : ℤ
hn : n < 0
⊢ (eval₂ f x) (T n) = ↑(x ^ n)

Tactic:
obtain ⟨m, rfl⟩ := Int.exists_eq_neg_ofNat hn.le

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
m : ℕ
hn : -↑m < 0
⊢ (eval₂ f x) (T (-↑m)) = ↑(x ^ (-↑m))
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
r : R
n : ℕ
⊢ (eval₂ f x) (C r * T (-↑n)) = f r * ↑x⁻¹ ^ n

Tactic:
rw [map_mul, eval₂_T_neg_n, eval₂_C]

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

Goal state before:
pp: case inr
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g✝ : M →ₗ[R] P
bc : IsBaseChange T g✝
this✝¹ : NoZeroDivisors R
h✝ : Nontrivial R
this✝ : IsDomain T
FR : Type uR := FractionRing R
FT : Type uT := FractionRing T
inj : Function.Injective ⇑(algebraMap R FT)
g : P →ₗ[T] FT ⊗[T] P := (TensorProduct.mk T FT P) 1
this : IsLocalizedModule R⁰ ((TensorProduct.mk R FR FT) 1)
x✝ : Algebra FT (FR ⊗[R] FT) := Algebra.TensorProduct.rightAlgebra
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

Tactic:
let _ := isLocalizedModule_iff_isLocalization.mp this |>.atUnits _ _ ?_ |>.symm.isField
    (Field.toIsField FT) |>.toField

Goal state after:
case inr.refine_2
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g✝ : M →ₗ[R] P
bc : IsBaseChange T g✝
this✝¹ : NoZeroDivisors R
h✝ : Nontrivial R
this✝ : IsDomain T
FR : Type uR := FractionRing R
FT : Type uT := FractionRing T
inj : Function.Injective ⇑(algebraMap R FT)
g : P →ₗ[T] FT ⊗[T] P := (TensorProduct.mk T FT P) 1
this : IsLocalizedModule R⁰ ((TensorProduct.mk R FR FT) 1)
x✝¹ : Algebra FT (FR ⊗[R] FT) := Algebra.TensorProduct.rightAlgebra
x✝ : Field (FR ⊗[R] FT) := ⋯.toField
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

case inr.refine_1
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g✝ : M →ₗ[R] P
bc : IsBaseChange T g✝
this✝¹ : NoZeroDivisors R
h✝ : Nontrivial R
this✝ : IsDomain T
FR : Type uR := FractionRing R
FT : Type uT := FractionRing T
inj : Function.Injective ⇑(algebraMap R FT)
g : P →ₗ[T] FT ⊗[T] P := (TensorProduct.mk T FT P) 1
this : IsLocalizedModule R⁰ ((TensorProduct.mk R FR FT) 1)
x✝ : Algebra FT (FR ⊗[R] FT) := Algebra.TensorProduct.rightAlgebra
⊢ Algebra.algebraMapSubmonoid FT R⁰ ≤ IsUnit.submonoid FT
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
⊢ (A.updateRow j (Pi.single i 1)).det = (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det

Tactic:
det_succ_row _ j,

Goal state after:
α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
⊢ ∑ j_1,
      (-1) ^ (↑j + ↑j_1) * A.updateRow j (Pi.single i 1) j j_1 *
        ((A.updateRow j (Pi.single i 1)).submatrix j.succAbove j_1.succAbove).det =
    (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det
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 α
k : ℕ
⊢ (A ^ k).adjugate = A.adjugate ^ k

Tactic:
by
  induction k with
  | zero => simp
  | succ k IH => rw [pow_succ', adjugate_mul_distrib, IH, pow_succ]

Goal state after:
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 α
A : Matrix n n α
B : Matrix m n α
h : IsUnit A.det
⊢ B * A * A⁻¹ = B

Tactic:
by
  simp [Matrix.mul_assoc, mul_nonsing_inv A h]

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

Goal state before:
pp: case succ.succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
⊢ A'.det • A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 1) • A'

Tactic:
det_smul_adjugate_adjugate

Goal state after:
case succ.succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
⊢ A'.det ^ (Fintype.card n - 1) • A' = A'.det ^ (Fintype.card n - 1) • A'
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : AddZeroClass R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
⊢ (M + N) i j = 0

Tactic:
Matrix.add_apply,

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : AddZeroClass R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
⊢ M i j + N i j = 0
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case pos.intro.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val✝¹ : Invertible (diagonal v)
val✝ : Invertible v
⊢ ⅟(diagonal v) = diagonal ⅟v

Tactic:
invOf_diagonal_eq

Goal state after:
case pos.intro.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val✝¹ : Invertible (diagonal v)
val✝ : Invertible v
⊢ diagonal ⅟v = diagonal ⅟v
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case right
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Unit
j : Fin r
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₂₁ i j = 0 i j

Tactic:
have : i = unit := by simp only

Goal state after:
case right
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Unit
j : Fin r
this : i = ()
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₂₁ i j = 0 i j
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case zero
𝕜 : Type u_3
inst✝² : Field 𝕜
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = 0
⊢ ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
refine ⟨List.nil, List.nil, fun _ => 1, ?_⟩
    ext i j
    rw [Fintype.card_eq_zero_iff] at hn
    exact hn.elim' i

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
h : (-1) ^ n = 0
⊢ False

Tactic:
exact not_isNilpotent_neg_one ⟨n, 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 : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ ((f.sum fun e a ↦ (RingHom.id R) a * x ^ e) - f.sum fun e a ↦ (RingHom.id R) a * y ^ e) =
    (f.sum fun i r ↦ r * ↑(powSubPowFactor x y i)) * (x - y)

Tactic:
simp only [sum, ← Finset.sum_sub_distrib, Finset.sum_mul]

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
f : R[X]
x y : R
⊢ ∑ x_1 ∈ f.support, ((RingHom.id R) (f.coeff x_1) * x ^ x_1 - (RingHom.id R) (f.coeff x_1) * y ^ x_1) =
    ∑ i ∈ f.support, f.coeff i * ↑(powSubPowFactor x y i) * (x - y)
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case inr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard = ⨅ s, ↑(↑s).card

Tactic:
simp_rw [← Set.encard_coe_eq_coe_finsetCard]

Goal state after:
case inr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard = ⨅ s, (↑↑s).encard
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case refine_1.h
R : Type u_1
M : Type u
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s // span R s = span R (Set.range v) }
this : #↑↑x = #↑(Subtype.val ⁻¹' ↑x)
⊢ Function.Injective ⇑(Module.Basis.span hs)

Tactic:
exact .of_comp (f := Subtype.val) (by convert! hv; ext; simp [Module.Basis.span_apply])

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
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ M.charpoly.coeff k = (∏ i, (X - C (M i i))).coeff k

Tactic:
apply eq_of_sub_eq_zero; rw [← coeff_sub]
  apply Polynomial.coeff_eq_zero_of_degree_lt
  apply lt_of_lt_of_le (charpoly_sub_diagonal_degree_lt M) ?_
  rw [Nat.cast_le]; apply h

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : eval₂ (algebraMap R A) x.1 p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : eval₂ (algebraMap R B) x.2 p₂ = 0
⊢ eval₂ (algebraMap R (A × B)) x (p₁ * p₂) = 0

Tactic:
← aeval_def

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : (aeval x.1) p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : (aeval x.2) p₂ = 0
⊢ (aeval x) (p₁ * p₂) = 0
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k) (g k)
hq : map f q = p
⊢ ∀ (a : ℕ), (∑ k ∈ p.support, (monomial k) (g k)).coeff a ≠ 0 ↔ p.coeff a ≠ 0

Tactic:
finsetSum_coeff,

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k) (g k)
hq : map f q = p
⊢ ∀ (a : ℕ), ∑ b ∈ p.support, ((monomial b) (g b)).coeff a ≠ 0 ↔ p.coeff a ≠ 0
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k) (g k)
hq : map f q = p
k : ℕ
h : g k = 0
⊢ p.coeff k = 0

Tactic:
rw [← hg, h, map_zero]

Goal state after:
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' := ⋯ }
⊢ ∀ (x y : ↥A'),
    (DistribSMul.toLinearMap R M (x + y)).restrict ⋯ =
      (DistribSMul.toLinearMap R M x).restrict ⋯ + (DistribSMul.toLinearMap R M y).restrict ⋯

Tactic:
intro x y; ext; exact add_smul _ _ _

Goal state after:
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
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Nontrivial S
⊢ ∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

Tactic:
obtain ⟨p', h₁, h₂, h₃⟩ := lifts_and_degree_eq_and_monic hlifts hp

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Nontrivial S
p' : R[X]
h₁ : map f p' = p
h₂ : p'.degree = p.degree
h₃ : p'.Monic
⊢ ∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
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
this : Module.Finite R ↥N
⊢ IsIntegral R (f ⟨x, hx⟩)

Tactic:
apply Algebra.IsIntegral.isIntegral

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

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

Tactic:
rw [← tsub_lt_iff_right hil] at hikl
      rw [choose_eq_zero_of_lt hikl, zero_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y : R
⊢ ∃ c, c * y ^ 2 + eval x (derivative p) * y + eval x p = eval (x + y) p

Tactic:
have this t :
      (taylor x p).eval t =
      ∑ i ∈ Finset.range ((taylor x p).natDegree + 2), (taylor x p).coeff i * t ^ i :=
    (taylor x p).eval_eq_sum_range' (n := (taylor x p).natDegree + 2) (by lia) t

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y : R
this :
  ∀ (t : R), eval t ((taylor x) p) = ∑ i ∈ Finset.range (((taylor x) p).natDegree + 2), ((taylor x) p).coeff i * t ^ i
⊢ ∃ c, c * y ^ 2 + eval x (derivative p) * y + eval x p = eval (x + y) p
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
⊢ p.integralNormalization.coeff i = if p.degree = ↑i then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)

Tactic:
have : p.coeff i = 0 → p.degree ≠ i := fun hc hd => coeff_ne_zero_of_eq_degree hd hc
  simp +contextual [sum_def, integralNormalization, coeff_monomial, this,
    mem_support_iff]

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n a b : ℕ
e : a + b = n
ha : a ≤ p.natDegree
hb : b ≤ q.natDegree
⊢ p.coeff a * q.coeff b * r ^ (p.natDegree + q.natDegree - n) =
    p.coeff a * r ^ (p.natDegree - a) * (q.coeff b * r ^ (q.natDegree - b))

Tactic:
simp only [← e, mul_assoc, mul_comm (r ^ (_ - a)), ← pow_add]
        rw [add_comm (_ - _), tsub_add_tsub_comm ha hb]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n A
h : ∀ (i j : n), IsIntegral R (M i j)
⊢ IsIntegral R M.det

Tactic:
by
  rw [Matrix.det_apply]
  exact IsIntegral.sum _ fun σ _hσ ↦ (IsIntegral.prod _ fun i _hi => h _ _).zsmul _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : ((X - C a) * (f * g)).natDegree = n + 1
ha : eval a ((X - C a) * (f * g)) = 0
⊢ X - C a ≠ 0

Tactic:
by aesop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : ((X - C a) * (f * g)).natDegree = n + 1
ha : eval a ((X - C a) * (f * g)) = 0
⊢ f * g ≠ 0

Tactic:
by aesop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : (f * g).natDegree = n
ha : eval a ((X - C a) * (f * g)) = 0
⊢ f ≠ 0

Tactic:
by aesop

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

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
h : (f /ₘ (X - C x)).natDegree = 1
⊢ f /ₘ (X - C x) ≠ 0

Tactic:
by aesop

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
K : Type u_4
inst✝³ : CommRing K
inst✝² : Algebra S K
inst✝¹ : Algebra R K
inst✝ : IsIntegralClosure S R K
x : K
hx : IsAlgebraic R x
r : R
hr : r ≠ 0
h : IsIntegral R (r • x)
⊢ ∃ r s, r ≠ 0 ∧ r • x = (algebraMap S K) s

Tactic:
obtain ⟨s, hs⟩ := IsIntegralClosure.isIntegral_iff (A := S) |>.mp h

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
K : Type u_4
inst✝³ : CommRing K
inst✝² : Algebra S K
inst✝¹ : Algebra R K
inst✝ : IsIntegralClosure S R K
x : K
hx : IsAlgebraic R x
r : R
hr : r ≠ 0
h : IsIntegral R (r • x)
s : S
hs : (algebraMap S K) s = r • x
⊢ ∃ r s, r ≠ 0 ∧ r • x = (algebraMap S K) s