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

Goal state before:
pp: case mp
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
⊢ IsIntegral R a → IsIntegral T a

pp: case mpr
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
⊢ IsIntegral T a → IsIntegral R a

Tactic:
<;>

Goal state after:
case mp
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
⊢ IsIntegral R a → IsIntegral T a

case mpr
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
⊢ IsIntegral T a → IsIntegral R a
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✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : A
h : IsIntegral R x
⊢ IsIntegral R ((algebraMap A B) x)

Tactic:
by
  rcases h with ⟨f, hf, hx⟩
  use f, hf
  rw [IsScalarTower.algebraMap_eq R A B, ← hom_eval₂, hx, map_zero]

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

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

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

Tactic:
<;>

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

case mpr
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
⊢ (∃ s, s.Finite ∧ IsIntegral (↥(Subring.closure s)) r) → IsIntegral R r
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : m = k
m0 : m = 0
⊢ 1 - (M ^ k) j j = (1 - M ^ k) j j

pp: case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : m = k
m0 : ¬m = 0
⊢ 1 - 0 = (1 - 0) j j

pp: case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : ¬m = k
h✝ : m = 0
⊢ 0 - (M ^ k) j j = (0 - M ^ k) j j

pp: case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : ¬m = k
h✝ : ¬m = 0
⊢ 0 - 0 = (0 - 0) j j

Tactic:
<;>

Goal state after:
case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : m = k
m0 : m = 0
⊢ 1 - (M ^ k) j j = (1 - M ^ k) j j

case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : m = k
m0 : ¬m = 0
⊢ 1 - 0 = (1 - 0) j j

case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : ¬m = k
h✝ : m = 0
⊢ 0 - (M ^ k) j j = (0 - M ^ k) j j

case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : ¬m = k
h✝ : ¬m = 0
⊢ 0 - 0 = (0 - 0) j j
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
m0 : m = 0
mp : m = k
⊢ -(M ^ k) i j = (1 - M ^ k) i j

pp: case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
m0 : m = 0
mp : ¬m = k
⊢ -(M ^ k) i j = (0 - M ^ k) i j

pp: case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
m0 : ¬m = 0
h✝ : m = k
⊢ -0 = (1 - 0) i j

pp: case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
m0 : ¬m = 0
h✝ : ¬m = k
⊢ -0 = (0 - 0) i j

Tactic:
<;>

Goal state after:
case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
m0 : m = 0
mp : m = k
⊢ -(M ^ k) i j = (1 - M ^ k) i j

case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
m0 : m = 0
mp : ¬m = k
⊢ -(M ^ k) i j = (0 - M ^ k) i j

case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
m0 : ¬m = 0
h✝ : m = k
⊢ -0 = (1 - 0) i j

case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
m0 : ¬m = 0
h✝ : ¬m = k
⊢ -0 = (0 - 0) i j
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' := ⋯ }
⊢ { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } 1 = 1

Tactic:
ext; apply one_smul

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
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
⊢ (1 - t_inv • M.map ⇑LaurentPolynomial.C).det = invert q

Tactic:
invert.map_det

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
⊢ (1 - t_inv • M.map ⇑LaurentPolynomial.C).det = (invert.mapMatrix (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C)).det
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i j : n
hij : i = j
⊢ (1 - X • M.map ⇑C).map (eval 0) i j = 1 i j

pp: case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i j : n
hij : i ≠ j
⊢ (1 - X • M.map ⇑C).map (eval 0) i j = 1 i j

Tactic:
<;>

Goal state after:
case inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i j : n
hij : i = j
⊢ (1 - X • M.map ⇑C).map (eval 0) i j = 1 i j

case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i j : n
hij : i ≠ j
⊢ (1 - X • M.map ⇑C).map (eval 0) i j = 1 i j
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
hM : IsNilpotent M
⊢ IsUnit M.charpolyRev

Tactic:
by
  obtain ⟨k, hk⟩ := hM
  replace hk : 1 - (X : R[X]) • M.map C ∣ 1 := by
    convert! one_sub_dvd_one_sub_pow ((X : R[X]) • M.map C) k
    rw [← C.mapMatrix_apply, smul_pow, ← map_pow, hk, map_zero, smul_zero, sub_zero]
  apply isUnit_of_dvd_one
  rw [← det_one (R := R[X]) (n := n)]
  exact map_dvd detMonoidHom hk

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

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
s : Finset n
i j : n
n✝ : ℕ
h : i ∈ s
⊢ (M.map (⇑C) i j).coeff n✝ = (C (M i j)).coeff n✝

pp: case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
s : Finset n
i j : n
n✝ : ℕ
h : i ∉ s
⊢ (1 i j).coeff n✝ = (C (1 i j)).coeff n✝

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
s : Finset n
i j : n
n✝ : ℕ
h : i ∈ s
⊢ (M.map (⇑C) i j).coeff n✝ = (C (M i j)).coeff n✝

case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
s : Finset n
i j : n
n✝ : ℕ
h : i ∉ s
⊢ (1 i j).coeff n✝ = (C (1 i j)).coeff n✝
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
s : Finset n
n✝ : ℕ
i j : n
h✝ : i ∈ s
⊢ (X • M.map ⇑C) i j = X * M.map (⇑C) i j

pp: case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
s : Finset n
n✝ : ℕ
i j : n
h✝ : i ∉ s
⊢ 1 i j = 1 i j

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
s : Finset n
n✝ : ℕ
i j : n
h✝ : i ∈ s
⊢ (X • M.map ⇑C) i j = X * M.map (⇑C) i j

case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
s : Finset n
n✝ : ℕ
i j : n
h✝ : i ∉ s
⊢ 1 i j = 1 i j
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
r s : R
a✝ : Nontrivial R
⊢ ((X + C r).scaleRoots s).coeff 0 = (X + C (r * s)).coeff 0

pp: case succ.zero
R : Type u_1
inst✝ : Semiring R
r s : R
a✝ : Nontrivial R
⊢ ((X + C r).scaleRoots s).coeff (0 + 1) = (X + C (r * s)).coeff (0 + 1)

pp: case succ.succ
R : Type u_1
inst✝ : Semiring R
r s : R
a✝ : Nontrivial R
i : ℕ
⊢ ((X + C r).scaleRoots s).coeff (i + 1 + 1) = (X + C (r * s)).coeff (i + 1 + 1)

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
r s : R
a✝ : Nontrivial R
⊢ ((X + C r).scaleRoots s).coeff 0 = (X + C (r * s)).coeff 0

case succ.zero
R : Type u_1
inst✝ : Semiring R
r s : R
a✝ : Nontrivial R
⊢ ((X + C r).scaleRoots s).coeff (0 + 1) = (X + C (r * s)).coeff (0 + 1)

case succ.succ
R : Type u_1
inst✝ : Semiring R
r s : R
a✝ : Nontrivial R
i : ℕ
⊢ ((X + C r).scaleRoots s).coeff (i + 1 + 1) = (X + C (r * s)).coeff (i + 1 + 1)
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
aux :
  ∀ x ∈ antidiagonal k,
    (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
      (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
⊢ (monomial (m + n - k)) (↑((m + n).choose k) * (r * s)) =
    ∑ x ∈ antidiagonal k, (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Tactic:
← map_sum,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
aux :
  ∀ x ∈ antidiagonal k,
    (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
      (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
⊢ (monomial (m + n - k)) (↑((m + n).choose k) * (r * s)) =
    (monomial (m + n - k)) (∑ x ∈ antidiagonal k, ↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
hp : ¬p = 0
⊢ p.integralNormalization.degree = p.degree

Tactic:
rw [degree_eq_natDegree hp]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
hp : ¬p = 0
⊢ p.integralNormalization.degree = ↑p.natDegree
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
hfi : f.coeff i ≠ 0
hi : f.degree = ↑i
⊢ 1 ≠ 0

pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
hfi : f.coeff i ≠ 0
hi : ¬f.degree = ↑i
⊢ f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i) ≠ 0

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
hfi : f.coeff i ≠ 0
hi : f.degree = ↑i
⊢ 1 ≠ 0

case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
hfi : f.coeff i ≠ 0
hi : ¬f.degree = ↑i
⊢ f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i) ≠ 0
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Ring R
r s : R
a✝ : Nontrivial R
⊢ ((X - C r).scaleRoots s).coeff 0 = (X - C (r * s)).coeff 0

pp: case succ.zero
R : Type u_1
inst✝ : Ring R
r s : R
a✝ : Nontrivial R
⊢ ((X - C r).scaleRoots s).coeff (0 + 1) = (X - C (r * s)).coeff (0 + 1)

pp: case succ.succ
R : Type u_1
inst✝ : Ring R
r s : R
a✝ : Nontrivial R
i : ℕ
⊢ ((X - C r).scaleRoots s).coeff (i + 1 + 1) = (X - C (r * s)).coeff (i + 1 + 1)

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝ : Ring R
r s : R
a✝ : Nontrivial R
⊢ ((X - C r).scaleRoots s).coeff 0 = (X - C (r * s)).coeff 0

case succ.zero
R : Type u_1
inst✝ : Ring R
r s : R
a✝ : Nontrivial R
⊢ ((X - C r).scaleRoots s).coeff (0 + 1) = (X - C (r * s)).coeff (0 + 1)

case succ.succ
R : Type u_1
inst✝ : Ring R
r s : R
a✝ : Nontrivial R
i : ℕ
⊢ ((X - C r).scaleRoots s).coeff (i + 1 + 1) = (X - C (r * s)).coeff (i + 1 + 1)
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case mem
R : Type u_1
inst✝¹ : Semiring R
f : R[X]
S : Type u_2
inst✝ : Semiring S
i : R →+* S
x✝ : R[X]
h✝ : x✝ ∈ {x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x}
⊢ (map i x✝).Splits

pp: case one
R : Type u_1
inst✝¹ : Semiring R
f : R[X]
S : Type u_2
inst✝ : Semiring S
i : R →+* S
⊢ (map i 1).Splits

pp: case mul
R : Type u_1
inst✝¹ : Semiring R
f : R[X]
S : Type u_2
inst✝ : Semiring S
i : R →+* S
x✝ y✝ : R[X]
hx✝ : x✝ ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hy✝ : y✝ ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
a✝¹ : (map i x✝).Splits
a✝ : (map i y✝).Splits
⊢ (map i (x✝ * y✝)).Splits

Tactic:
<;>

Goal state after:
case mem
R : Type u_1
inst✝¹ : Semiring R
f : R[X]
S : Type u_2
inst✝ : Semiring S
i : R →+* S
x✝ : R[X]
h✝ : x✝ ∈ {x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x}
⊢ (map i x✝).Splits

case one
R : Type u_1
inst✝¹ : Semiring R
f : R[X]
S : Type u_2
inst✝ : Semiring S
i : R →+* S
⊢ (map i 1).Splits

case mul
R : Type u_1
inst✝¹ : Semiring R
f : R[X]
S : Type u_2
inst✝ : Semiring S
i : R →+* S
x✝ y✝ : R[X]
hx✝ : x✝ ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hy✝ : y✝ ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
a✝¹ : (map i x✝).Splits
a✝ : (map i y✝).Splits
⊢ (map i (x✝ * y✝)).Splits
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case mem
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
this : ∀ (i : R), (X + C r + C i).Splits
x✝ : R[X]
h✝ : x✝ ∈ {x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x}
⊢ ((Polynomial.taylor r) x✝).Splits

pp: case one
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
this : ∀ (i : R), (X + C r + C i).Splits
⊢ ((Polynomial.taylor r) 1).Splits

pp: case mul
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
this : ∀ (i : R), (X + C r + C i).Splits
x✝ y✝ : R[X]
hx✝ : x✝ ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hy✝ : y✝ ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
a✝¹ : ((Polynomial.taylor r) x✝).Splits
a✝ : ((Polynomial.taylor r) y✝).Splits
⊢ ((Polynomial.taylor r) (x✝ * y✝)).Splits

Tactic:
<;>

Goal state after:
case mem
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
this : ∀ (i : R), (X + C r + C i).Splits
x✝ : R[X]
h✝ : x✝ ∈ {x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x}
⊢ ((Polynomial.taylor r) x✝).Splits

case one
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
this : ∀ (i : R), (X + C r + C i).Splits
⊢ ((Polynomial.taylor r) 1).Splits

case mul
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
this : ∀ (i : R), (X + C r + C i).Splits
x✝ y✝ : R[X]
hx✝ : x✝ ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
hy✝ : y✝ ∈ Submonoid.closure ({x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x})
a✝¹ : ((Polynomial.taylor r) x✝).Splits
a✝ : ((Polynomial.taylor r) y✝).Splits
⊢ ((Polynomial.taylor r) (x✝ * y✝)).Splits
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ (∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod) →
    ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod

pp: case refine_2
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ (∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod) →
    ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ (∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod) →
    ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod

case refine_2
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ (∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod) →
    ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod

pp: case refine_2
R : Type u_1
inst✝ : CommRing R
f : R[X]
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
⊢ ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod

case refine_2
R : Type u_1
inst✝ : CommRing R
f : R[X]
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
⊢ ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case mem.inl
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
φ : R →+* S
r : R
hφ : map φ (C r) ≠ 0
⊢ (map φ (C r)).roots = Multiset.map (⇑φ) (C r).roots

pp: case mem.inr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
φ : R →+* S
a : R
hφ : map φ (X + C a) ≠ 0
⊢ (map φ (X + C a)).roots = Multiset.map (⇑φ) (X + C a).roots

Tactic:
<;>

Goal state after:
case mem.inl
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
φ : R →+* S
r : R
hφ : map φ (C r) ≠ 0
⊢ (map φ (C r)).roots = Multiset.map (⇑φ) (C r).roots

case mem.inr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
φ : R →+* S
a : R
hφ : map φ (X + C a) ≠ 0
⊢ (map φ (X + C a)).roots = Multiset.map (⇑φ) (X + C a).roots
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: case neg
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' : ¬p.natDegree ≠ 0
hp : ¬Polynomial.map f p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)

Tactic:
Classical.not_not

Goal state after:
case neg
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' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
⊢ f.IsIntegralElem (f p.leadingCoeff * x)
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case mp
A : Type u_3
K : Type u_4
C : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
⊢ IsAlgebraic A x → IsAlgebraic K x

pp: case mpr
A : Type u_3
K : Type u_4
C : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
⊢ IsAlgebraic K x → IsAlgebraic A x

Tactic:
<;>

Goal state after:
case mp
A : Type u_3
K : Type u_4
C : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
⊢ IsAlgebraic A x → IsAlgebraic K x

case mpr
A : Type u_3
K : Type u_4
C : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
⊢ IsAlgebraic K x → IsAlgebraic A x