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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
⊢ ∃ y, x * (algebraMap R T) ↑y.2 = (algebraMap R T) y.1

Tactic:
rcases IsLocalization.surj N x with ⟨⟨y, s⟩, eq₁⟩
  -- x = y / s
  rcases IsLocalization.surj M y with ⟨⟨z, t⟩, eq₂⟩
  -- y = z / t
  rcases IsLocalization.surj M (s : S) with ⟨⟨z', t'⟩, eq₃⟩
  -- s = z' / t'
  dsimp only at eq₁ eq₂ eq₃
  refine ⟨⟨z * t', z' * t, ?_⟩, ?_⟩ -- x = y / s = (z * t') / (z' * t)
  · rw [mem_localizationLocalizationSubmodule]
    refine ⟨s, t * t', ?_⟩
    rw [map_mul, ← eq₃, mul_assoc, ← map_mul, mul_comm t, Submonoid.coe_mul]
  · simp only [map_mul, IsScalarTower.algebraMap_apply R S T, ← eq₃, ← eq₂, ← eq₁]
    ring

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑⟨↑c * z', ⋯⟩ * x = ↑⟨↑c * z', ⋯⟩ * y

Tactic:
mul_comm _ z',

Goal state after:
case refine_2
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (z' * x) = ↑c * (y * z')
⊢ ↑⟨↑c * z', ⋯⟩ * x = ↑⟨↑c * z', ⋯⟩ * y
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (z' * x) = ↑c * (y * z')
⊢ ↑⟨↑c * z', ⋯⟩ * x = ↑⟨↑c * z', ⋯⟩ * y

Tactic:
mul_comm _ z',

Goal state after:
case refine_2
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (z' * x) = ↑c * (z' * y)
⊢ ↑⟨↑c * z', ⋯⟩ * x = ↑⟨↑c * z', ⋯⟩ * y
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S✝ : Type u_2
inst✝³ : CommSemiring S✝
inst✝² : Algebra R S✝
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
S : Type u_4
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
K : Ideal P
hK : K.IsPrime
f : R →+* S
hIJ : I = Ideal.comap f J
g : S →+* P
hJK : J = Ideal.comap g K
⊢ Ideal.comap f (Ideal.comap g K) = Ideal.comap (g.comp f) K

Tactic:
Ideal.comap_comap f g

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S✝ : Type u_2
inst✝³ : CommSemiring S✝
inst✝² : Algebra R S✝
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
S : Type u_4
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
K : Ideal P
hK : K.IsPrime
f : R →+* S
hIJ : I = Ideal.comap f J
g : S →+* P
hJK : J = Ideal.comap g K
⊢ Ideal.comap (g.comp f) K = Ideal.comap (g.comp f) K
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 : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hT :
  ∀ (r : ↑s),
    ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
      ∃ (_ : IsLocalization.Away (↑r) Rᵣ) (_ : IsLocalization.Away (f ↑r) Sᵣ),
        ∃ fᵣ, ∃ (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ
r : ↑s
Rᵣ Sᵣ : Type u
w✝⁵ : CommRing Rᵣ
w✝⁴ : CommRing Sᵣ
w✝³ : Algebra R Rᵣ
w✝² : Algebra S Sᵣ
w✝¹ : IsLocalization.Away (↑r) Rᵣ
w✝ : IsLocalization.Away (f ↑r) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f
hf : P fᵣ
e₁ : Localization (Submonoid.powers ↑r) ≃+* Rᵣ := (Localization.algEquiv (Submonoid.powers ↑r) Rᵣ).toRingEquiv
e₂ : Sᵣ ≃+* Localization (Submonoid.powers (f ↑r)) :=
  (IsLocalization.algEquiv (Submonoid.powers (f ↑r)) (Localization (Submonoid.powers (f ↑r))) Sᵣ).symm.toRingEquiv
x : R
⊢ fᵣ ((algebraMap R Rᵣ) x) = (algebraMap S Sᵣ) (f x)

Tactic:
← RingHom.comp_apply,

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hT :
  ∀ (r : ↑s),
    ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
      ∃ (_ : IsLocalization.Away (↑r) Rᵣ) (_ : IsLocalization.Away (f ↑r) Sᵣ),
        ∃ fᵣ, ∃ (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ
r : ↑s
Rᵣ Sᵣ : Type u
w✝⁵ : CommRing Rᵣ
w✝⁴ : CommRing Sᵣ
w✝³ : Algebra R Rᵣ
w✝² : Algebra S Sᵣ
w✝¹ : IsLocalization.Away (↑r) Rᵣ
w✝ : IsLocalization.Away (f ↑r) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f
hf : P fᵣ
e₁ : Localization (Submonoid.powers ↑r) ≃+* Rᵣ := (Localization.algEquiv (Submonoid.powers ↑r) Rᵣ).toRingEquiv
e₂ : Sᵣ ≃+* Localization (Submonoid.powers (f ↑r)) :=
  (IsLocalization.algEquiv (Submonoid.powers (f ↑r)) (Localization (Submonoid.powers (f ↑r))) Sᵣ).symm.toRingEquiv
x : R
⊢ (fᵣ.comp (algebraMap R Rᵣ)) x = (algebraMap S Sᵣ) (f x)
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 α
g : Equiv.Perm n
i : n
x✝ : i ∈ Finset.univ
⊢ (X * C (A (g i) i) + C (B (g i) i)).natDegree ≤ 1

Tactic:
compute_degree

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

Goal state before:
pp: case e'_3.convert_5
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
p : n
⊢ (X * C (A (g p) p) + C (B (g p) p)).natDegree ≤ 1

Tactic:
compute_degree

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

Goal state before:
pp: case inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Subsingleton α
⊢ (X • 1 + A.map ⇑C).det.leadingCoeff = 1

pp: case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ (X • 1 + A.map ⇑C).det.leadingCoeff = 1

Tactic:
· simp [eq_iff_true_of_subsingleton]

Goal state after:
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ (X • 1 + A.map ⇑C).det.leadingCoeff = 1
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inl
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⁰
h✝ : Subsingleton R
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)

pp: case inr
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⁰
h✝ : Nontrivial R
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)

Tactic:
· simp only [rank_subsingleton, lift_one]

Goal state after:
case inr
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⁰
h✝ : Nontrivial R
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
x : Sˣ
n : ℤ
r : R
⊢ smeval (AddMonoidAlgebra.single n r) x = r • ↑(x ^ n)

Tactic:
smeval_single

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
x : Sˣ
n : ℤ
r : R
⊢ r • ↑(x ^ n) = r • ↑(x ^ n)
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✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible A
⊢ Aᵀ * (⅟A)ᵀ = 1

Tactic:
rw [← transpose_mul, invOf_mul_self, transpose_one]

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

Goal state before:
pp: case intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A
⊢ A⁻¹ * A = 1

Tactic:
rw [← invOf_eq_nonsing_inv, invOf_mul_self]

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

Goal state before:
pp: case inl
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Subsingleton α
⊢ 0⁻¹ = 0

pp: case inr
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
⊢ 0⁻¹ = 0

Tactic:
· simp [eq_iff_true_of_subsingleton]

Goal state after:
case inr
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
⊢ 0⁻¹ = 0
Module: Mathlib.LinearAlgebra.Matrix.Block

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

Tactic:
rw [insert_erase]

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

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (A * B)⁻¹ = B⁻¹ * A⁻¹

Tactic:
simp only [inv_def]

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

Goal state after:
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
i j : m
x : ℕ
⊢ (((reindex e e) M).charmatrix i j).coeff x = ((reindex e e) M.charmatrix i j).coeff x
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
inst✝ : LinearOrder n
M : Matrix n n R
h : M.IsUpperTriangular
⊢ M.charpoly = ∏ i, (X - C (M i i))

Tactic:
by
  simp [charpoly, det_of_isUpperTriangular h.charmatrix]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (1 - A * B).det = (1 - B * A).det

Tactic:
rw [sub_eq_add_neg, ← Matrix.neg_mul, det_one_add_mul_comm, Matrix.mul_neg, ← sub_eq_add_neg]

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

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Ring R
h_comm : Commute x y
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (x - y)

Tactic:
by
  rw [← neg_right_iff] at h_comm
  rw [← isNilpotent_neg_iff] at hy
  rw [sub_eq_add_neg]
  exact h_comm.isNilpotent_add hx hy

Goal state after:
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
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
⊢ ⨅ s, (↑↑s).encard ≤ s.encard

Tactic:
by_cases hs : s.Finite

Goal state after:
case pos
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

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
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
p : Submodule R M
a : Cardinal.{u}
⊢ p.spanRank ≤ a ↔ ∃ s, #↑s ≤ a ∧ span R s = p

Tactic:
by
  convert! lift_spanRank_le_iff_exists_span_set_card_le p (a := a) <;> simp

Goal state after:
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)
⊢ ∑ i ∈ p.support, map f ((monomial i) (g i)) = p

Tactic:
map_monomial,

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)
⊢ ∑ x ∈ p.support, (monomial x) (f (g x)) = p
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
r : R
hk : 0 < k
⊢ (hasseDeriv k) (C r) = 0

Tactic:
← monomial_zero_left,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
r : R
hk : 0 < k
⊢ (hasseDeriv k) ((monomial 0) r) = 0
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)! • hasseDeriv (k + 1)) f).coeff n = ((⇑derivative)^[k + 1] f).coeff n

Tactic:
rw [iterate_succ_apply', ← ih]

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)! • hasseDeriv (k + 1)) f).coeff n = (derivative ((k ! • hasseDeriv k) f)).coeff n
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).Monic ↔ p.Monic

Tactic:
simp_rw [Monic, leadingCoeff, natDegree_toSubring, ← coeff_toSubring p T hp]

Goal state after:
R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).coeff p.natDegree = 1 ↔ ↑((p.toSubring T hp).coeff p.natDegree) = 1
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
i : R
hi : i ∈ ↑(ofSubring T p).coeffs
⊢ i ∈ ↑T

Tactic:
simp only [coeffs, Set.mem_image, mem_support_iff, Ne, Finset.mem_coe,
    (Finset.coe_image)] at hi

Goal state after:
R : Type u_1
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
i : R
hi : ∃ x, ¬(ofSubring T p).coeff x = 0 ∧ (ofSubring T p).coeff x = i
⊢ i ∈ ↑T
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
hf : f.Splits
a✝ : Nontrivial R
a : R
m : Multiset R
h : Irreducible (C f.leadingCoeff * ((X + C a) * (Multiset.map (fun x ↦ X + C x) m).prod))
hm : f = C f.leadingCoeff * ((X + C a) * (Multiset.map (fun x ↦ X + C x) m).prod)
ha : a ∈ a ::ₘ m
⊢ f.natDegree ≤ 1

Tactic:
simp only [irreducible_mul_iff, IsUnit.mul_iff, not_isUnit_X_add_C, false_and, and_false,
      or_false, false_or, ← Multiset.prod_toList, List.prod_isUnit_iff] at h

Goal state after:
case inr
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
hf : f.Splits
a✝ : Nontrivial R
a : R
m : Multiset R
hm : f = C f.leadingCoeff * ((X + C a) * (Multiset.map (fun x ↦ X + C x) m).prod)
ha : a ∈ a ::ₘ m
h : (Irreducible (X + C a) ∧ ∀ m_1 ∈ (Multiset.map (fun x ↦ X + C x) m).toList, IsUnit m_1) ∧ IsUnit (C f.leadingCoeff)
⊢ f.natDegree ≤ 1
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
⊢ integralClosure R A = ⊤ ↔ Algebra.IsIntegral R A

Tactic:
rw [← top_le_iff, le_integralClosure_iff_isIntegral,
      (Subalgebra.topEquiv (R := R) (A := A)).isIntegral_iff]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ (Multiset.map (fun ij ↦ ij.1 - ij.2) (g.roots ×ˢ s)).prod =
    (-1) ^ (s.card * g.roots.card) * (Multiset.map (fun x ↦ eval x g) s).prod

Tactic:
trans ((s ×ˢ g.roots).map fun ij ↦ (-1) * (ij.1 - ij.2)).prod

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ (Multiset.map (fun ij ↦ ij.1 - ij.2) (g.roots ×ˢ s)).prod =
    (Multiset.map (fun ij ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)).prod

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ (Multiset.map (fun ij ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)).prod =
    (-1) ^ (s.card * g.roots.card) * (Multiset.map (fun x ↦ eval x g) s).prod
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
⊢ ⇑g '' ↑(f.aroots A).toFinset = f.rootSet B

Tactic:
← Finset.coe_image,

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
⊢ ↑(Finset.image (⇑g) (f.aroots A).toFinset) = f.rootSet B
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✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : FaithfulSMul A B
inst✝ : IsScalarTower R A B
f : R[X]
hf : (map (algebraMap R A) f).Splits
⊢ ⇑(algebraMap A B) '' ↑(f.aroots A).toFinset = f.rootSet B

Tactic:
← Finset.coe_image,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : FaithfulSMul A B
inst✝ : IsScalarTower R A B
f : R[X]
hf : (map (algebraMap R A) f).Splits
⊢ ↑(Finset.image (⇑(algebraMap A B)) (f.aroots A).toFinset) = f.rootSet B
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_2
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]
a : R
coeff_eq_zero : p.coeff 0 = 0
⊢ a ≠ 0 →
    (p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I) →
      p + C a ≠ 0 → eval₂ f r (p + C a) = 0 → ∃ i, (p + C a).coeff i ≠ 0 ∧ (p + C a).coeff i ∈ comap f I

Tactic:
a_ne_zero

Goal state after:
case refine_2
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]
a : R
coeff_eq_zero : p.coeff 0 = 0
a_ne_zero : a ≠ 0
⊢ (p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I) →
    p + C a ≠ 0 → eval₂ f r (p + C a) = 0 → ∃ i, (p + C a).coeff i ≠ 0 ∧ (p + C a).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
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
faithful : ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
m : Ideal R
hm : m.IsMaximal
rid : m • ⊤ = ⊤
⊢ False

Tactic:
specialize faithful (ULift (R ⧸ m)) inferInstance

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
hm : m.IsMaximal
rid : m • ⊤ = ⊤
⊢ False
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : (aeval a) p = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
⊢ IsAlgebraic R a

Tactic:
have ⟨r, hr, int⟩ := Algebra.IsAlgebraic.exists_integral_multiples R (p.support.image (coeff p))

Goal state after:
case pos
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : (aeval a) p = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p.coeff p.support, IsIntegral R (r • z)
⊢ IsAlgebraic R a