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

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ ∀ (x : β), (f 0) x = 0

Tactic:
intro

Goal state after:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
x✝ : β
⊢ (f 0) x✝ = 0
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ ∀ (x : α), (f x) 0 = 0

Tactic:
intro

Goal state after:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
x✝ : α
⊢ (f x✝) 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
⊢ ∀ (M : Matrix n n α), f' (g M) = M

Tactic:
intro

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
M✝ : Matrix n n α
⊢ f' (g M✝) = M✝
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
⊢ ∀ (M : Matrix n n α), f' (g M).adjugate = M.adjugate

Tactic:
intro

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
M✝ : Matrix n n α
⊢ f' (g M✝).adjugate = M✝.adjugate
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 α
h : IsUnit A.det
⊢ A.det⁻¹ʳ • A.adjugate = (↑h.unit)⁻¹ʳ • A.adjugate

Tactic:
IsUnit.unit_spec

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A.det⁻¹ʳ • A.adjugate = A.det⁻¹ʳ • A.adjugate
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 α
inst✝ : Invertible A
⊢ Invertible ⅟A

Tactic:
infer_instance

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

Goal state before:
pp: m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ (M.toSquareBlockProp fun i ↦ ¬p i).det * (M.toSquareBlockProp fun i ↦ ¬¬p i).det =
    (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i ↦ ¬p i).det

pp: m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ ∀ (i : m), ¬¬p i → ∀ (j : m), ¬p j → M i j = 0

Tactic:
mul_comm

Goal state after:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ (M.toSquareBlockProp fun i ↦ ¬¬p i).det * (M.toSquareBlockProp fun i ↦ ¬p i).det =
    (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i ↦ ¬p i).det

m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ ∀ (i : m), ¬¬p i → ∀ (j : m), ¬p j → M i j = 0
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this✝ : Inhabited m
k : α := (image b univ).max' ⋯
b' : { a // b a < k } → α := fun i ↦ b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i ↦ b i < k) fun j ↦ b j < k
hi : b i < (image b univ).max' ⋯
this : Invertible A
hA : A.BlockTriangular b'
hb' : image b' univ ⊂ image b univ
hij' : b' ⟨j, ⋯⟩ < b' ⟨i, hi⟩
⊢ M⁻¹ i j = 0

Tactic:
simp [A, hM.inv_toBlock k, (ih (image b' univ) hb' hA rfl hij').symm]

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:
by
  rw [charmatrix, scalar_apply, RingHom.mapMatrix_apply, (blockTriangular_diagonal _).sub_iff_right]
  simp [BlockTriangular]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (r + 1)

Tactic:
rw [← IsUnit.neg_iff, neg_add']
  exact isUnit_sub_one hnil.neg

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

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
k : ℕ
hk : 1 < k
⊢ IsRadical 0 ↔ ∀ (x : R), x ^ k = 0 → x = 0

Tactic:
isRadical_iff_pow_one_lt k hk,

Goal state after:
R : Type u_1
inst✝ : MonoidWithZero R
k : ℕ
hk : 1 < k
⊢ (∀ (x : R), 0 ∣ x ^ k → 0 ∣ x) ↔ ∀ (x : R), x ^ k = 0 → x = 0
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case neg
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 : Set M
h : span R s = p
hs : ¬s.Finite
⊢ ⨅ s, (↑↑s).encard ≤ s.encard

Tactic:
rw [Set.Infinite.encard_eq hs]
        exact OrderTop.le_top _

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:
exact le_trans (Submodule.spanFinrank_span_le_ncard_of_finite (by simp)) (by simp)

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

Goal state before:
pp: case refine_2
R : Type u_6
A : Type u_7
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : (aeval x) f = 0
a✝ : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : (aeval x) p ∈ (aeval x).range
⊢ (aeval x) p ∈ span R ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range f.natDegree))

Tactic:
← modByMonic_add_div p f,

Goal state after:
case refine_2
R : Type u_6
A : Type u_7
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : (aeval x) f = 0
a✝ : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : (aeval x) p ∈ (aeval x).range
⊢ (aeval x) (p %ₘ f + f * (p /ₘ f)) ∈ span R ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range f.natDegree))
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x : B
f : R[X]
hfm : f.Monic
hfx : eval₂ (algebraMap R B) x f = 0
⊢ (aeval x) f = 0

Tactic:
rwa [aeval_def]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : { s // LinearIndepOn R id s }
s : { s // span R s = ⊤ }
⊢ #↑↑ι ≤ #↑↑s

Tactic:
have := linearIndependent_le_span'' ι.2 s.1 s.2

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : { s // LinearIndepOn R id s }
s : { s // span R s = ⊤ }
this : #↑↑ι ≤ #↑↑s
⊢ #↑↑ι ≤ #↑↑s
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : CommRing T
inst✝² : Ring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
⊢ eval (ψ a) (Polynomial.map ψ (Polynomial.map (algebraMap R S) p)) = 0

Tactic:
eval_map,

Goal state after:
R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : CommRing T
inst✝² : Ring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
⊢ eval₂ ψ (ψ a) (Polynomial.map (algebraMap R S) p) = 0
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : CommRing T
inst✝² : Ring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
⊢ ψ (eval a (Polynomial.map (algebraMap R S) p)) = 0

Tactic:
eval_map,

Goal state after:
R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : CommRing T
inst✝² : Ring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
⊢ ψ (eval₂ (algebraMap R S) a p) = 0
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
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
t_inv : R[T;T⁻¹] := T (-1)
p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det
q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det
ht : t_inv * t = 1
hp : toLaurentAlg M.charpoly = p
hq : toLaurentAlg M.charpolyRev = q
this : t_inv ^ Fintype.card n * p = invert q
⊢ p * T (-1) ^ Fintype.card n = invert q

Tactic:
mul_comm

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
t_inv : R[T;T⁻¹] := T (-1)
p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det
q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det
ht : t_inv * t = 1
hp : toLaurentAlg M.charpoly = p
hq : toLaurentAlg M.charpolyRev = q
this : t_inv ^ Fintype.card n * p = invert q
⊢ T (-1) ^ Fintype.card n * p = invert q
Module: Mathlib.Algebra.Polynomial.HasseDeriv

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

Tactic:
mul_comm

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
this : ((hasseDeriv f.natDegree) f).natDegree ≤ 0
⊢ C (f.coeff f.natDegree) = C f.leadingCoeff

Tactic:
leadingCoeff

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
this : ((hasseDeriv f.natDegree) f).natDegree ≤ 0
⊢ C (f.coeff f.natDegree) = C (f.coeff f.natDegree)
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ f.leadingCoeff = f.coeff f.natDegree

Tactic:
leadingCoeff

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ f.coeff f.natDegree = f.coeff f.natDegree
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
⊢ (p.scaleRoots s).support ⊆ p.support

Tactic:
intro

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
x✝ : ℕ
⊢ x✝ ∈ (p.scaleRoots s).support → x✝ ∈ p.support
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
hi : i ∈ p.support
⊢ f (p.coeff i) * f s ^ (p.natDegree - i + i) * a ^ i = f s ^ p.natDegree * (f (p.coeff i) * a ^ i)

Tactic:
by
        rw [mul_assoc, ← map_pow, (hf _ _).left_comm, map_pow, tsub_add_cancel_of_le]
        exact le_natDegree_of_ne_zero (Polynomial.mem_support_iff.mp hi)

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

Goal state before:
pp: case hf
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
s₁✝ s₂✝ : R
⊢ (algebraMap R A) (s₁✝ * s₂✝) = (algebraMap R A) (s₂✝ * s₁✝)

Tactic:
mul_comm

Goal state after:
case hf
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
s₁✝ s₂✝ : R
⊢ (algebraMap R A) (s₂✝ * s₁✝) = (algebraMap R A) (s₂✝ * s₁✝)
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.integralNormalization.support ⊆ p.support

Tactic:
intro

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
x✝ : ℕ
⊢ x✝ ∈ p.integralNormalization.support → x✝ ∈ p.support
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
x✝ : ℕ
⊢ x✝ ∈ p.integralNormalization.support → x✝ ∈ p.support

Tactic:
simp +contextual [sum_def, integralNormalization, coeff_monomial, mem_support_iff]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : A ≃ₐ[R] S
y : S
⊢ y ∈ Subalgebra.map (↑f) (integralClosure R A) ↔ y ∈ integralClosure R S

Tactic:
rw [Subalgebra.mem_map]

Goal state after:
R : Type u_1
A : Type u_2
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : A ≃ₐ[R] S
y : S
⊢ (∃ x ∈ integralClosure R A, ↑f x = y) ↔ y ∈ integralClosure R S
Module: Mathlib.RingTheory.Localization.Integral

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
p : S[X]
b : R
hb : b ∈ ↑M
h : IsInteger R[X] (b • p)
q' : R[X]
h₁ : Polynomial.map (algebraMap R S) q' = b • p
h₂ : q'.support = (b • p).support
⊢ ∃ b ∈ M, ∃ q, Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support

Tactic:
exact ⟨b, hb, q', h₁, h₂ ▸ support_smul b p⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Field A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra R B
f : R[X]
hf : (map (algebraMap R A) f).Splits
g : A →ₐ[R] B
⊢ Algebra.adjoin R (f.rootSet B) = g.range ↔ Algebra.adjoin R (f.rootSet A) = ⊤

Tactic:
rw [← hf.image_rootSet g, Algebra.adjoin_image, ← Algebra.map_top]

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Field A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra R B
f : R[X]
hf : (map (algebraMap R A) f).Splits
g : A →ₐ[R] B
⊢ Subalgebra.map g (Algebra.adjoin R (f.rootSet A)) = Subalgebra.map g ⊤ ↔ Algebra.adjoin R (f.rootSet A) = ⊤
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ (algebraMap R Rₘ) (↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n - 1)) *
      ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) * p.coeff n) ∈
    Set.range ⇑(algebraMap R Rₘ)

Tactic:
change _ ∈ (algebraMap R Rₘ).range

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ (algebraMap R Rₘ) (↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n - 1)) *
      ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) * p.coeff n) ∈
    (algebraMap R Rₘ).range
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
⊢ f (eval a p.reverse) = 0

Tactic:
← eval₂_hom

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
⊢ eval₂ f (f a) p.reverse = 0
Module: Mathlib.RingTheory.Localization.Integral

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
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
hx : IsIntegral Rₘ x
⊢ ∃ m, IsIntegral R (m • x)

Tactic:
rcases subsingleton_or_nontrivial Rₘ with _ | nontriv

Goal state after:
case inl
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
hx : IsIntegral Rₘ x
h✝ : Subsingleton Rₘ
⊢ ∃ m, IsIntegral R (m • x)

case inr
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
hx : IsIntegral Rₘ x
nontriv : Nontrivial Rₘ
⊢ ∃ m, IsIntegral R (m • x)
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 : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r p.divX * eval₂ f r X + f (p.coeff 0) ∈ I
⊢ p.coeff 0 ∈ comap f I

Tactic:
eval₂_X

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
hr : r ∈ I
p : R[X]
hp : eval₂ f r p.divX * r + f (p.coeff 0) ∈ I
⊢ p.coeff 0 ∈ comap f I
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_3
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
a✝ : p * X ≠ 0
hp : eval₂ f r p * eval₂ f r X = 0
⊢ ∃ i, (p * X).coeff i ≠ 0 ∧ (p * X).coeff i ∈ comap f I

Tactic:
eval₂_X

Goal state after:
case refine_3
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
p_nonzero : p ≠ 0
ih : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
a✝ : p * X ≠ 0
hp : eval₂ f r p * r = 0
⊢ ∃ i, (p * X).coeff i ≠ 0 ∧ (p * X).coeff i ∈ 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
inst✝² : FaithfullyFlat R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : Nontrivial N
⊢ Nontrivial (N ⊗[R] M)

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
p : (↥R[s])[X]
hpm : p.Monic
hpt : eval₂ (algebraMap (↥R[s]) S) t p = 0
this : Polynomial.map (algebraMap (↥R[s]) S) p ∈ lifts φ.toRingHom
q : R[X][X]
hqp : Polynomial.map φ.toRingHom q = Polynomial.map (algebraMap (↥R[s]) S) p
hqd : q.degree = (Polynomial.map (algebraMap (↥R[s]) S) p).degree
hqm : q.Monic
⊢ eval t (Polynomial.map (algebraMap (↥R[s]) S) p) = 0

Tactic:
eval_map,

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
p : (↥R[s])[X]
hpm : p.Monic
hpt : eval₂ (algebraMap (↥R[s]) S) t p = 0
this : Polynomial.map (algebraMap (↥R[s]) S) p ∈ lifts φ.toRingHom
q : R[X][X]
hqp : Polynomial.map φ.toRingHom q = Polynomial.map (algebraMap (↥R[s]) S) p
hqd : q.degree = (Polynomial.map (algebraMap (↥R[s]) S) p).degree
hqm : q.Monic
⊢ eval₂ (algebraMap (↥R[s]) S) t p = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
⊢ x.asIdeal.IsPrime

Tactic:
infer_instance

Goal state after: