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

Goal state before:
pp: case refine_2
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✝
p✝ : Ideal R✝
inst✝²³ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝²² : CommSemiring Rₚ✝
inst✝²¹ : Algebra R✝ Rₚ✝
inst✝²⁰ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁹ : IsLocalRing Rₚ✝
Sₚ✝ : Type u_5
inst✝¹⁸ : CommSemiring Sₚ✝
inst✝¹⁷ : Algebra S✝ Sₚ✝
inst✝¹⁶ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ✝
inst✝¹⁵ : Algebra Rₚ✝ Sₚ✝
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝¹⁴ : CommRing R
p : Ideal R
inst✝¹³ : p.IsMaximal
Rₚ : Type u_8
inst✝¹² : CommRing Rₚ
inst✝¹¹ : Algebra R Rₚ
inst✝¹⁰ : IsLocalization.AtPrime Rₚ p
inst✝⁹ : IsLocalRing Rₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
· intro x
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq
      (Algebra.algebraMapSubmonoid S p.primeCompl) x
    obtain ⟨α, hα : α ∉ p, e⟩ := s.prop
    obtain ⟨β, γ, hγ, hβ⟩ : ∃ β γ, γ ∈ p ∧ α * β = 1 + γ := by
      obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹
      refine ⟨β, α * β - 1, ?_, ?_⟩
      · rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
          map_mul, hβ, mul_inv_cancel₀, sub_self]
        rwa [Ne, Ideal.Quotient.eq_zero_iff_mem]
      · rw [add_sub_cancel]
    use β • x
    rw [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ pSₚ), Ideal.Quotient.algebraMap_eq,
      RingHom.comp_apply, ← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
    rw [h, IsLocalization.mem_map_algebraMap_iff
      (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
    refine ⟨⟨⟨γ • x, ?_⟩, s⟩, ?_⟩
    · rw [Algebra.smul_def]
      apply Ideal.mul_mem_right
      exact Ideal.mem_map_of_mem _ hγ
    simp only
    rw [mul_comm, mul_sub, IsLocalization.mul_mk'_eq_mk'_of_mul,
      IsLocalization.mk'_mul_cancel_left, ← map_mul, ← e, ← Algebra.smul_def, smul_smul,
      hβ, ← map_sub, add_smul, one_smul, add_comm x, add_sub_cancel_right]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
⊢ (C a).degree = (C a * T 0).degree

Tactic:
rw [T_zero, mul_one]

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

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i, b i • Pi.single i 1
⊢ A.cramer (∑ i, b i • Pi.single i 1) = (of fun i ↦ Aᵀᵀ.cramer (Pi.single i 1))ᵀ *ᵥ b

Tactic:
ext k

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i, b i • Pi.single i 1
k : n
⊢ A.cramer (∑ i, b i • Pi.single i 1) k = ((of fun i ↦ Aᵀᵀ.cramer (Pi.single i 1))ᵀ *ᵥ b) k
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
hM : ∀ (t : TransvectionStruct n R), Commute t.toMatrix M
⊢ M ∈ Set.range ⇑(scalar n)

Tactic:
refine mem_range_scalar_of_commute_single ?_

Goal state after:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
hM : ∀ (t : TransvectionStruct n R), Commute t.toMatrix M
⊢ Pairwise fun i j ↦ Commute (single i j 1) M
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.det = A'.det ^ (Fintype.card n - 1)
⊢ (MvPolynomial.aeval fun p ↦ A p.1 p.2) (mvPolynomialX n n ℤ).adjugate.det =
    (MvPolynomial.aeval fun p ↦ A p.1 p.2) (mvPolynomialX n n ℤ).det ^ (Fintype.card n - 1)

Tactic:
← map_pow,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.det = A'.det ^ (Fintype.card n - 1)
⊢ (MvPolynomial.aeval fun p ↦ A p.1 p.2) (mvPolynomialX n n ℤ).adjugate.det =
    (MvPolynomial.aeval fun p ↦ A p.1 p.2) ((mvPolynomialX n n ℤ).det ^ (Fintype.card n - 1))
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: R : Type u_6
inst✝² : AddCommMonoid R
o : Type u_8
inst✝¹ : Fintype o
inst✝ : DecidableEq o
d : o → R
⊢ (diagonal d).trace = ∑ i, d i

Tactic:
simp only [trace, diag_apply, diagonal_apply_eq]

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

Goal state before:
pp: R : Type u_6
inst✝ : AddCommMonoid R
A : Matrix (Fin 3) (Fin 3) R
⊢ A.trace = A 0 0 + A 1 1 + (A 2 2 + 0)

Tactic:
add_assoc

Goal state after:
R : Type u_6
inst✝ : AddCommMonoid R
A : Matrix (Fin 3) (Fin 3) R
⊢ A.trace = A 0 0 + (A 1 1 + (A 2 2 + 0))
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B : Matrix n n α
⊢ ∀ ⦃a₂ : Matrix n n α⦄, (fun x ↦ A * x) B = (fun x ↦ A * x) a₂ → B = a₂

Tactic:
C

Goal state after:
case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
⊢ (fun x ↦ A * x) B = (fun x ↦ A * x) C → B = C
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B : Matrix n n α
⊢ ∀ ⦃a₂ : Matrix n n α⦄, (fun x ↦ x * A) B = (fun x ↦ x * A) a₂ → B = a₂

Tactic:
C

Goal state after:
case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
⊢ (fun x ↦ x * A) B = (fun x ↦ x * A) C → B = C
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.det = 1

Tactic:
rw [← det_mul, A.nonsing_inv_mul h, det_one]

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

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ blockDiagonal d (i, i') (j, j') = 0

Tactic:
rw [blockDiagonal'_eq_blockDiagonal, blockTriangular_blockDiagonal']

Goal state after:
case a
α : Type u_1
m : Type u_3
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ ⟨j', j⟩.fst < ⟨i', i⟩.fst
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case e_a
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 p).det

Tactic:
exact equiv_block_det _ fun _ => not_not.symm

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

Goal state before:
pp: α : 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'
⊢ k ∈ image b univ

Tactic:
convert! max'_mem (α := α) _ _

Goal state after:
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
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
⊢ M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)

Tactic:
simp [M, N, fromBlocks_multiply, smul_eq_mul_diagonal, -diagonal_neg]

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

Goal state before:
pp: case convert_1
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
⊢ Invertible (fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1)

Tactic:
letI : Invertible (1 : Matrix n n α) := invertibleOne
    letI : Invertible (1 : Matrix m m α) := invertibleOne
    refine Invertible.mul ?_ (fromBlocksZero₁₂Invertible _ _ _)
    exact
      Invertible.mul (fromBlocksZero₂₁Invertible _ _ _)
        (fromBlocksZero₂₁Invertible _ _ _)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
⊢ IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)

Tactic:
by
  obtain ⟨Q, hQ⟩ := IsUnit.exists_right_inv hunit
  constructor
  · refine .of_mul_eq_one (Q.coeff 0) ?_
    have h := (mul_coeff_zero P Q).symm
    rwa [hQ, coeff_one_zero] at h
  · intro n hn
    rw [nilpotent_iff_mem_prime]
    intro I hI
    let f := mapRingHom (Ideal.Quotient.mk I)
    have hPQ : degree (f P) = 0 ∧ degree (f Q) = 0 := by
      rw [← Nat.WithBot.add_eq_zero_iff, ← degree_mul, ← map_mul, hQ, map_one, degree_one]
    have hcoeff : (f P).coeff n = 0 := by
      refine coeff_eq_zero_of_degree_lt ?_
      rw [hPQ.1]
      exact WithBot.coe_pos.2 hn.bot_lt
    rw [coe_mapRingHom, coeff_map, ← RingHom.mem_ker, Ideal.mk_ker] at hcoeff
    exact hcoeff

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 ι
hb : Submodule.span R (Set.range b) = ⊤
⊢ Function.Surjective ⇑(toEnd R b hb)

Tactic:
by
  intro f
  obtain ⟨M, e, -⟩ := Matrix.isRepresentation.toEnd_exists_mem_ideal R b hb f ⊤ (by simp)
  exact ⟨M, e⟩

Goal state after:
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
⊢ M.charpoly.degree = ↑(Fintype.card n)

Tactic:
← sub_add_cancel M.charpoly (∏ i : n, (X - C (M i i)))

Goal state after:
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
⊢ (M.charpoly - ∏ i, (X - C (M i i)) + ∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: 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

Tactic:
constructor <;> intro ha

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
ha : 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
ha : IsIntegral T a
⊢ IsIntegral R a
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case insert
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s✝ : Set A
a : A
s : Set A
a✝ : a ∉ s
hs✝ : s.Finite
ih : (∀ x ∈ s, IsIntegral R x) → (Subalgebra.toSubmodule (Algebra.adjoin R s)).FG
his : ∀ x ∈ insert a s, IsIntegral R x
⊢ (Subalgebra.toSubmodule (Algebra.adjoin R (insert a s))).FG

Tactic:
rw [← Set.union_singleton, Algebra.adjoin_union_coe_submodule]
    exact FG.mul
      (ih fun i hi => his i <| Set.mem_insert_of_mem a hi)
      (his a <| Set.mem_insert a s).fg_adjoin_singleton

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.charpoly.reverse = M.charpolyRev

Tactic:
nontriviality R
  let t : R[T;T⁻¹] := T 1
  let t_inv : R[T;T⁻¹] := T (-1)
  let p : R[T;T⁻¹] := det (scalar n t - M.map LaurentPolynomial.C)
  let q : R[T;T⁻¹] := det (1 - scalar n t * M.map LaurentPolynomial.C)
  have ht : t_inv * t = 1 := by rw [← T_add, neg_add_cancel, T_zero]
  have hp : toLaurentAlg M.charpoly = p := by
    simp [p, t, charpoly, charmatrix, AlgHom.map_det, map_sub]
  have hq : toLaurentAlg M.charpolyRev = q := by
    simp [q, t, charpolyRev, AlgHom.map_det, map_sub, smul_eq_diagonal_mul]
  suffices t_inv ^ Fintype.card n * p = invert q by
    apply toLaurent_injective
    rwa [toLaurent_reverse, ← coe_toLaurentAlg, hp, hq, ← involutive_invert.injective.eq_iff,
      map_mul, involutive_invert p, charpoly_natDegree_eq_dim,
      ← mul_one (Fintype.card n : ℤ), ← T_pow, map_pow, invert_T, mul_comm]
  rw [← det_smul, smul_sub, scalar_apply, ← diagonal_smul, Pi.smul_def, smul_eq_mul, ht,
    diagonal_one, invert.map_det]
  simp [t_inv, map_sub, map_one, map_mul, t, smul_eq_diagonal_mul]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
⊢ 1 = 1 - X ^ k • C.mapMatrix M ^ k

Tactic:
← map_pow,

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 • C.mapMatrix (M ^ k)
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
⊢ IsNilpotent M.trace

Tactic:
by
  cases isEmpty_or_nonempty n
  · simp
  suffices IsNilpotent (coeff (charpolyRev M) 1) by simpa using this
  exact (isUnit_iff_coeff_isUnit_isNilpotent.mp (isUnit_charpolyRev_of_isNilpotent hM)).2
    _ one_ne_zero

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ ∑ n_1 ∈ p.support, (monomial (n_1 - n)) (↑(n_1.choose n) * p.coeff n_1) = 0

Tactic:
refine Finset.sum_eq_zero fun x hx => ?_

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
x : ℕ
hx : x ∈ p.support
⊢ (monomial (x - n)) (↑(x.choose n) * p.coeff x) = 0
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0
⊢ (taylor r) f = 0

Tactic:
ext k

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0
k : ℕ
⊢ ((taylor r) f).coeff k = coeff 0 k
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:
← map_pow,

Goal state after:
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)
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
⊢ (p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n) * r ^ (p.natDegree - (p + q).natDegree) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)

Tactic:
#adaptation_note /-- v4.7.0-rc1
  Previously `mul_assoc` was part of the `simp only` above, and this `rw` was not needed.
  but this now causes a max rec depth error. -/

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.natDegree = q.natDegree
n : ℕ
⊢ (p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n) * r ^ (p.natDegree - (p + q).natDegree) =
    (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.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 A B
inst✝³ : Algebra R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R ↑p.coeffs
this✝² : Module.Finite R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
hSx : IsIntegral (↥S) x
Sx : Submodule (↥S) B := Subalgebra.toSubmodule (↥S)[x]
MSx : Module ↥S ↥Sx := SMulMemClass.toModule Sx
this✝¹ : Module.Finite ↥S ↥Sx
this✝ : SMul ↥S ↥Sx := MSx.toSMul
this : IsScalarTower R ↥S ↥Sx
⊢ Module.Finite R ↥(Subalgebra.toSubmodule (Subalgebra.restrictScalars R (↥S)[x]))

Tactic:
exact Module.Finite.trans S Sx

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

Goal state before:
pp: case inr.refine_1
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
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
⊢ p.leadingCoeff ∈ (algebraMap R Rₘ).range

Tactic:
rw [hp₁.leadingCoeff]

Goal state after:
case inr.refine_1
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
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
⊢ 1 ∈ (algebraMap R Rₘ).range
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst✝ : Away r Sₘ
x : S
a✝ : Nontrivial S
p : R[X]
hpm : p.Monic
m : ℕ
hm : r ^ m * eval₂ (algebraMap R S) x p = 0
this : IsIntegral R ((C ⟨r, hr⟩ ^ m * Polynomial.map (algebraMap R ↥(integralClosure R S)) p).leadingCoeff • x)
⊢ ∃ n, IsIntegral R (r ^ n * x)

Tactic:
← map_pow,

Goal state after:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst✝ : Away r Sₘ
x : S
a✝ : Nontrivial S
p : R[X]
hpm : p.Monic
m : ℕ
hm : r ^ m * eval₂ (algebraMap R S) x p = 0
this : IsIntegral R ((C (⟨r, hr⟩ ^ m) * Polynomial.map (algebraMap R ↥(integralClosure R S)) p).leadingCoeff • x)
⊢ ∃ n, IsIntegral R (r ^ n * x)
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case pos
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
I : Ideal S
inst✝³ : Algebra R S
inst✝² : Nontrivial R
inst✝¹ : IsDomain S
inst✝ : Algebra.IsIntegral R S
hI : comap (algebraMap R S) I = ⊥
x : S
hx : x ∈ I
hx0 : x = 0
⊢ x ∈ ⊥

Tactic:
exact hx0.symm ▸ Ideal.zero_mem ⊥

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
ht : IsIntegral (↥R[s]) t
⊢ IsIntegral R t

Tactic:
nontriviality S
  let φ := aeval (R := R) s
  obtain ⟨q, hqm, hqt⟩ : φ.IsIntegralElem t := by
    obtain ⟨p, hpm, hpt⟩ := ht
    have : p.map (algebraMap _ S) ∈ lifts φ.toRingHom := (lifts_iff_coeff_lifts _).mpr
      (by simp [← AlgHom.mem_range, φ, ← Algebra.adjoin_singleton_eq_range_aeval])
    obtain ⟨q, hqp, hqd, hqm⟩ := lifts_and_degree_eq_and_monic this (hpm.map _)
    exact ⟨q, hqm, by rw [← eval_map, hqp, eval_map, hpt]⟩
  let N := q.support.sup (q.coeff · |>.natDegree)
  have hN (i : _) : (q.coeff i).natDegree ≤ N := by
    by_cases hi : i ∈ q.support
    · exact Finset.le_sup (f := (q.coeff · |>.natDegree)) hi
    · simp_all
  let q' := q.sum fun i r ↦ X ^ i * r.reflect N
  have (i : _) : aeval t (reflect N (q.coeff i)) = t ^ N * (aeval s (q.coeff i)) := by
    let : Invertible t := ⟨s, hst, (mul_comm _ _).trans hst⟩
    rw [aeval_def, ← eval₂_reflect_mul_pow _ _ N _ ((natDegree_reflect_le ..).trans (by simp [hN]))]
    simp +instances [mul_comm, this, aeval_def]
  refine ⟨q', ?_, ?_⟩
  · refine monic_of_natDegree_le_of_coeff_eq_one (q.natDegree + N) ?_ ?_
    · refine natDegree_sum_le_of_forall_le _ _ fun i hi ↦ ?_
      grw [natDegree_mul_le, natDegree_pow_le, natDegree_X_le, natDegree_reflect_le]
      simp [max_eq_left (hN _), le_natDegree_of_mem_supp _ hi]
    · simp only [sum, finsetSum_coeff, coeff_X_pow_mul', coeff_reflect, q']
      rw [Finset.sum_eq_single q.natDegree]
      · simp [hqm.leadingCoeff]
      · intro i hi₁ hi₂
        have : N + i < q.natDegree + N :=
          add_comm N i ▸ add_lt_add_left ((le_natDegree_of_mem_supp _ hi₁).lt_of_ne hi₂) _
        simpa [(le_natDegree_of_mem_supp _ hi₁).trans, revAt, this.not_ge] using
          coeff_eq_zero_of_natDegree_lt (by grind)
      · simp +contextual
  · trans t ^ N * q.sum (t ^ · * φ.toRingHom ·)
    · simp [φ, q', Polynomial.sum, ← aeval_def, this, mul_left_comm _ (t ^ N), ← Finset.mul_sum]
    · simp_rw [mul_comm (t ^ _), ← eval₂_eq_sum, hqt, zero_mul]

Goal state after:
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
h✝ : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
h : LinearMap.rTensor M f = 0
m : M
n : N
⊢ (TensorProduct.comm R M N') (((AlgebraTensorModule.curry (LinearMap.lTensor M f)) m) n) =
    (TensorProduct.comm R M N') (((AlgebraTensorModule.curry 0) m) n)

Tactic:
by simpa using congr($h (n ⊗ₜ m))

Goal state after: