mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.LinearCombination.Lemmas

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelAddMonoid α
p : a ≤ b
H : a' + b < b' + a
⊢ a' < b'

Tactic:
by
  grw [p] at H; simpa using H

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

Goal state before:
pp: case pos
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 m α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹

Tactic:
have hD := hAD.mp hA

Goal state after:
case pos
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 m α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: case neg
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 m α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
hD : ¬IsUnit D
this : ¬IsUnit (fromBlocks A B 0 D)
⊢ Ring.inverse (fromBlocks A B 0 D) = fromBlocks 0 (-(0 * B * Ring.inverse D)) 0 (Ring.inverse D)

Tactic:
Ring.inverse_non_unit _ hD,

Goal state after:
case neg
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 m α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
hD : ¬IsUnit D
this : ¬IsUnit (fromBlocks A B 0 D)
⊢ Ring.inverse (fromBlocks A B 0 D) = fromBlocks 0 (-(0 * B * 0)) 0 0
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: case pos
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 m α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹

Tactic:
have hD := hAD.mp hA

Goal state after:
case pos
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 m α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: case neg
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 m α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
hD : ¬IsUnit D
this : ¬IsUnit (fromBlocks A 0 C D)
⊢ Ring.inverse (fromBlocks A 0 C D) = fromBlocks 0 0 (-(Ring.inverse D * C * 0)) (Ring.inverse D)

Tactic:
Ring.inverse_non_unit _ hD,

Goal state after:
case neg
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 m α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
hD : ¬IsUnit D
this : ¬IsUnit (fromBlocks A 0 C D)
⊢ Ring.inverse (fromBlocks A 0 C D) = fromBlocks 0 0 (-(0 * C * 0)) 0
Module: Mathlib.RingTheory.Polynomial.Nilpotent

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

Tactic:
replace hp : eval 0 p = 0 := by rwa [coeff_zero_eq_aeval_zero] at hp₀

Goal state after:
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
i k : ℕ
hk : (p + C r) ^ k = 0
hp : eval 0 p = 0
⊢ IsNilpotent (C r)
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: case insert.hy
R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih : (∀ i ∈ s, IsNilpotent (f i)) → (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
⊢ IsNilpotent (∑ x ∈ s, f x)

Tactic:
· exact ih (fun i hi ↦ hnp i (by simp [hi]))
      (fun i j hi hj ↦ h_comm i j (by simp [hi]) (by simp [hj]))

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
⊢ (PiToModule.fromMatrix R b) 0 = (PiToModule.fromEnd R b) 0

Tactic:
map_zero,

Goal state after:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
⊢ 0 = (PiToModule.fromEnd R b) 0
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ (∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)

Tactic:
exact h1

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
⊢ M.trace = -M.charpoly.nextCoeff

Tactic:
cases isEmpty_or_nonempty n
  · simp [nextCoeff]
  nontriviality
  simp [trace_eq_neg_charpoly_coeff, nextCoeff]

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✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : B
hx : IsIntegral R x
p : R[X]
hp : p.Monic
hpx : eval₂ (algebraMap R B) x p = 0
⊢ eval₂ (algebraMap A B) x (Polynomial.map (algebraMap R A) p) = 0

Tactic:
by rw [← aeval_def, aeval_map_algebraMap, aeval_def, hpx]

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
p : R[X]
hmp : p.Monic
hpr : eval₂ (algebraMap R B) r p = 0
⊢ (aeval r) (Polynomial.map (algebraMap (↥(Subring.closure ↑p.coeffs)) R) p.restriction) = 0

Tactic:
map_restriction,

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
p : R[X]
hmp : p.Monic
hpr : eval₂ (algebraMap R B) r p = 0
⊢ (aeval r) 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
⊢ (1 + X • M.map ⇑C).det.coeff 1 = M.trace

Tactic:
by
  simp only [← derivative_det_one_add_X_smul, ← coeff_zero_eq_eval_zero,
    coeff_derivative, zero_add, Nat.cast_zero, mul_one]

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
⊢ (1 + X • M.map ⇑C).det = 1 + (C M.trace * X + (1 + X • M.map ⇑C).det.divX.divX * X * X)

Tactic:
← add_mul,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (1 + X • M.map ⇑C).det = 1 + (C M.trace + (1 + X • M.map ⇑C).det.divX.divX * X) * X
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]
r : R
hp : p ∈ lifts f
⊢ C (f r) * p ∈ lifts f

Tactic:
simp only [lifts, RingHom.mem_rangeS] at hp ⊢

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
r : R
hp : ∃ x, (mapRingHom f) x = p
⊢ ∃ x, (mapRingHom f) x = C (f r) * p
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_inv : R[T;T⁻¹] := ⋯
p : R[T;T⁻¹] := ⋯
q : R[T;T⁻¹] := ⋯
ht : t_inv * t = 1
hp : toLaurentAlg M.charpoly = p
hq : toLaurentAlg M.charpolyRev = q
this : t_inv ^ Fintype.card n * p = invert q
⊢ toLaurent M.charpoly.reverse = toLaurent M.charpolyRev

Tactic:
toLaurent_reverse,

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
⊢ invert (toLaurent M.charpoly) * T ↑M.charpoly.natDegree = toLaurent M.charpolyRev
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 0 ≤ #s

Tactic:
by positivity

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ 0 < #s

Tactic:
by positivity

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Fintype α
⊢ 0 ≤ Fintype.card α

Tactic:
by positivity

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Fintype α
⊢ 0 ≤ s.dens

Tactic:
by positivity

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
⊢ 0 < s.dens

Tactic:
by positivity

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
⊢ s.dens ≠ 0

Tactic:
by positivity

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ 0 < #univ

Tactic:
by positivity

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ 0 < Fintype.card α

Tactic:
by positivity

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ 0 < univ.dens

Tactic:
by positivity

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ univ.dens ≠ 0

Tactic:
by positivity

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.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
x : A
y : B
h : IsIntegral R y
⊢ IsIntegral A (x ⊗ₜ[R] y)

Tactic:
rw [← mul_one x, ← smul_eq_mul, ← smul_tmul']

Goal state after:
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
x : A
y : B
h : IsIntegral R y
⊢ IsIntegral A (x • 1 ⊗ₜ[R] y)
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 : ℕ
hk : M ^ k = 0
⊢ 1 = 1 - X ^ k • C.mapMatrix 0

Tactic:
map_zero,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
⊢ 1 = 1 - X ^ k • 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
hM : IsNilpotent M
a✝ : Nontrivial R
p : R[X] := M.charpolyRev
hp : p - 1 = X * (p /ₘ X)
this : IsNilpotent (p /ₘ X)
aux : (M.charpoly - X ^ Fintype.card n).natDegree ≤ M.charpoly.natDegree
⊢ IsNilpotent (M.charpolyRev - reflect M.charpoly.natDegree (X ^ Fintype.card n))

Tactic:
simpa [p, hp]

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

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

Tactic:
simp only [Finset.piecewise, if_neg i.prop, Matrix.one_apply, Subtype.ext_iff]

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

Goal state before:
pp: case e_a.e_f
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✝ : ℕ
⊢ (D (s.piecewise (fun i ↦ (X • M.map ⇑C) i) fun i ↦ 1 i)).coeff n✝ =
    (X ^ #s • D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i)).coeff n✝

Tactic:
have h_smul : s.piecewise (fun i ↦ ((X : R[X]) • M.map C) i)
            (fun i ↦ (1 : Matrix n n R[X]) i) =
            fun i => (if i ∈ s then (X : R[X]) else 1) •
              s.piecewise (fun i ↦ (M.map C) i) (fun i ↦ (1 : Matrix n n R[X]) i) i := by
          funext i j
          simp only [piecewise, Pi.smul_apply, smul_eq_mul, ite_mul, one_mul]
          split_ifs <;> rfl

Goal state after:
case e_a.e_f
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✝ : ℕ
h_smul :
  (s.piecewise (fun i ↦ (X • M.map ⇑C) i) fun i ↦ 1 i) = fun i ↦
    (if i ∈ s then X else 1) • s.piecewise (fun i ↦ M.map (⇑C) i) (fun i ↦ 1 i) i
⊢ (D (s.piecewise (fun i ↦ (X • M.map ⇑C) i) fun i ↦ 1 i)).coeff n✝ =
    (X ^ #s • D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i)).coeff n✝
Module: Mathlib.Algebra.Polynomial.Taylor

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

Tactic:
by_cases hf : f = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
hf : f = 0
⊢ ((taylor r) f).coeff f.natDegree = f.leadingCoeff

case neg
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
hf : ¬f = 0
⊢ ((taylor r) f).coeff f.natDegree = f.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
hf : f = 0
⊢ ((taylor r) f).coeff f.natDegree = f.leadingCoeff

Tactic:
hf,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
hf : f = 0
⊢ ((taylor r) 0).coeff (natDegree 0) = leadingCoeff 0
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
hf : f = 0
⊢ ((taylor r) 0).coeff (natDegree 0) = leadingCoeff 0

Tactic:
map_zero,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
hf : f = 0
⊢ coeff 0 (natDegree 0) = leadingCoeff 0
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
hp : ¬p = 0
⊢ ((taylor r) p).natDegree = p.natDegree

Tactic:
natDegree_taylor

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
hp : ¬p = 0
⊢ p.natDegree = p.natDegree
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
f : R[X]
s : R
⊢ eval (s - r) ((taylor r) f) = eval s f

Tactic:
rw [taylor_eval, sub_add_cancel]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.integralNormalization * C p.leadingCoeff = p.scaleRoots p.leadingCoeff

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

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
⊢ f.integralNormalization.support = f.support

Tactic:
by_cases hf : f = 0

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
⊢ f.integralNormalization.support = f.support

case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
⊢ f.integralNormalization.support = f.support
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r i : R
⊢ (X + C r + C i).Splits

Tactic:
simpa [add_assoc] using Splits.X_add_C (r + i)

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

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

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

Tactic:
· let S : Submonoid R[X] := MonoidHom.mrange C
    have hS : S = {C a | a : R} := MonoidHom.coe_mrange C
    rw [Splits, Submonoid.closure_union, ← hS, Submonoid.closure_eq, Submonoid.mem_sup] at hf
    obtain ⟨-, ⟨a, rfl⟩, g, hg, rfl⟩ := hf
    obtain ⟨mg, hmg, rfl⟩ := Submonoid.exists_multiset_of_mem_closure hg
    choose! j hj using hmg
    have hmg : mg = (mg.map j).map (X + C ·) := by simp [Multiset.map_congr rfl hj]
    rw [hmg, leadingCoeff_mul_monic, leadingCoeff_C]
    · use mg.map j
    · rw [hmg]
      apply monic_multiset_prod_of_monic
      simp [monic_X_add_C]

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ (∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod) → f.Splits
Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_2
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : CommMonoid M
a : A
m : M
b : B
⊢ invFun (single m (a ⊗ₜ[R] b)) = a ⊗ₜ[R] single m b

Tactic:
by
  simp [rTensorEquivAlgEquiv.invFun]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
a : R
⊢ ((X - C a) * f).Splits ↔ f.Splits

Tactic:
refine ⟨fun hf ↦ ?_, ((Splits.X_sub_C _).mul ·)⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
a : R
hf : ((X - C a) * f).Splits
⊢ f.Splits
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
inst✝ : IsDomain R
hM : M ≤ nonZeroDivisors R
p : S[X]
w✝ : R
hb₁ : w✝ ∈ M
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = w✝ • p
this✝¹ : IsDomain S := isDomain_of_le_nonZeroDivisors S hM
this✝ : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr (IsLocalization.injective S hM)
this : Function.Injective ⇑(mapRingHom (algebraMap R S)) :=
  Eq.mpr (id (congrArg (fun _a ↦ Function.Injective _a) (coe_mapRingHom (algebraMap R S))))
    (Eq.mpr (id (congrArg (fun _a ↦ _a) (propext (map_injective_iff (algebraMap R S)))))
      (IsLocalization.injective S hM))
⊢ w✝ • p = 0 ↔ p = 0

Tactic:
exact smul_eq_zero_iff_right <| nonZeroDivisors.ne_zero (hM hb₁)

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

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

Tactic:
refine eval₂_mul_eq_zero_of_left _ _ _ ?_

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

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
z : R
hz : z ∈ f.roots
⊢ f.leadingCoeff * (Multiset.map (fun x_1 ↦ x - x_1) (f.roots.erase z)).prod =
    f.leadingCoeff * ((x - z) * (Multiset.map (fun x_1 ↦ x - x_1) (f.roots.erase z)).prod / (x - z))

Tactic:
mul_div_cancel_left₀

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
z : R
hz : z ∈ f.roots
⊢ f.leadingCoeff * (Multiset.map (fun x_1 ↦ x - x_1) (f.roots.erase z)).prod =
    f.leadingCoeff * (Multiset.map (fun x_1 ↦ x - x_1) (f.roots.erase z)).prod

case ha
R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
z : R
hz : z ∈ f.roots
⊢ x - z ≠ 0
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ¬∀ (a : R), (algebraMap R A) a = 0 → a = 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
push Not at inj

Goal state after:
case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ∃ a, (algebraMap R A) a = 0 ∧ a ≠ 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)
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
ι : Type v
inst✝ : Nonempty ι
⊢ FaithfullyFlat R (ι →₀ R)

Tactic:
classical exact of_linearEquiv _ _ (finsuppLEquivDirectSum R R ι)

Goal state after: