mathlib-initiative/mathlib-tactics huggingface dataset:
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:
← transpose_one,

Goal state after:
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ᵀ
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case refine_1
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst✝¹ : LT α
inst✝ : Zero R
b : n → α
e : m ≃ n
h : ((reindex e e) M).BlockTriangular b
⊢ M.BlockTriangular (b ∘ ⇑e)

pp: case refine_2
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst✝¹ : LT α
inst✝ : Zero R
b : n → α
e : m ≃ n
h : M.BlockTriangular (b ∘ ⇑e)
⊢ ((reindex e e) M).BlockTriangular b

Tactic:
· convert! h.submatrix
    simp only [reindex_apply, submatrix_submatrix, submatrix_id_id, Equiv.symm_comp_self]

Goal state after:
case refine_2
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst✝¹ : LT α
inst✝ : Zero R
b : n → α
e : m ≃ n
h : M.BlockTriangular (b ∘ ⇑e)
⊢ ((reindex e e) M).BlockTriangular b
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case neg.inl
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
hni : n ≠ ↑i
hi : n + 1 ≤ ↑i
⊢ (if n ≤ ↑i then M (inr ()) (inl i) else 0) = if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0

pp: case neg.inr
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ (if n ≤ ↑i then M (inr ()) (inl i) else 0) = if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0

Tactic:
· simp [hi, n.le_succ.trans hi]

Goal state after:
case neg.inr
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ (if n ≤ ↑i then M (inr ()) (inl i) else 0) = if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
⊢ ((M⁻¹.toBlock (fun i ↦ b i < k) fun i ↦ b i < k) * M.toBlock (fun i ↦ b i < k) fun i ↦ b i < k) = 1

Tactic:
have h_sum :
    M⁻¹.toBlock p p * M.toBlock p p +
        (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p =
      1 := by
    rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_self]

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun i ↦ ¬p i) * M.toBlock (fun i ↦ ¬p i) p = 1
⊢ ((M⁻¹.toBlock (fun i ↦ b i < k) fun i ↦ b i < k) * M.toBlock (fun i ↦ b i < k) fun i ↦ b i < k) = 1
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
hk : (matPolyEquiv m).coeff k = 0
⊢ (m i j).coeff k = 0

Tactic:
← matPolyEquiv_coeff_apply,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
hk : (matPolyEquiv m).coeff k = 0
⊢ (matPolyEquiv m).coeff k i j = 0
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: 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 α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
⊢ (⅟(fromBlocks A B 0 D)).toBlocks₁₁ * A = 1

Tactic:
have := invOf_mul_self (fromBlocks A B 0 D)

Goal state after:
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 α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
this : ⅟(fromBlocks A B 0 D) * fromBlocks A B 0 D = 1
⊢ (⅟(fromBlocks A B 0 D)).toBlocks₁₁ * A = 1
Module: Mathlib.RingTheory.Nilpotent.Basic

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

Tactic:
obtain ⟨n, hn⟩ := hnil
  refine ⟨⟨r - 1, -∑ i ∈ Finset.range n, r ^ i, ?_, ?_⟩, rfl⟩
  · simp [mul_geom_sum, hn]
  · simp [geom_sum_mul, hn]

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

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
⊢ (x + y) ^ k = 0

Tactic:
rw [h_comm.add_pow']

Goal state after:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
⊢ ∑ m ∈ Finset.antidiagonal k, k.choose m.1 • (x ^ m.1 * y ^ m.2) = 0
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: case neg
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
hi : ¬m ≤ i
⊢ x ^ i * y ^ j = 0

Tactic:
rw [pow_eq_zero_of_le ?_ hy, mul_zero]

Goal state after:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
hi : ¬m ≤ i
⊢ n ≤ j
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 ι
⊢ Represents b 0 0

Tactic:
delta Matrix.Represents

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 ι
⊢ (PiToModule.fromMatrix R b) 0 = (PiToModule.fromEnd R b) 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
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ ↑(Fintype.card n - 1) ≤ ↑k

Tactic:
Nat.cast_le

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ Fintype.card n - 1 ≤ k
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

Tactic:
intro hr

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
hr : IsIntegral R r
⊢ ∃ s, s.Finite ∧ IsIntegral (↥(Subring.closure s)) r
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

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

Goal state after:
case mpr
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
hr : ∃ s, s.Finite ∧ IsIntegral (↥(Subring.closure s)) r
⊢ IsIntegral R r
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : S[X]
⊢ p ∈ lifts (algebraMap R S) ↔ p ∈ (mapAlg R S).range

Tactic:
simp only [coe_mapRingHom, lifts, mapAlg_eq_map, AlgHom.mem_range, RingHom.mem_rangeS]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : S[X]
r : R
hp : p ∈ lifts (algebraMap R S)
⊢ r • p ∈ lifts (algebraMap R S)

Tactic:
rw [mem_lifts_iff_mem_alg] at hp ⊢
  exact Subalgebra.smul_mem (mapAlg R S).range hp r

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

Tactic:
let q : R[T;T⁻¹] := det (1 - scalar n t * M.map LaurentPolynomial.C)

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
⊢ M.charpoly.reverse = M.charpolyRev
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' := ⋯ }
f : ↥A' →ₐ[R] Module.End R ↥N :=
  AlgHom.ofLinearMap { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
⊢ ∃ a ∈ N, a ≠ 0

Tactic:
by
    by_contra! h'
    apply hN
    rwa [eq_bot_iff]

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

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : z ∈ Subring.closure {x, y}
this✝ : Algebra R S := f.toAlgebra
this : (Subalgebra.toSubmodule R[x] * Subalgebra.toSubmodule R[y]).FG
⊢ f.IsIntegralElem z

Tactic:
rw [← Algebra.adjoin_union_coe_submodule, Set.singleton_union] at this

Goal state after:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : z ∈ Subring.closure {x, y}
this✝ : Algebra R S := f.toAlgebra
this : (Subalgebra.toSubmodule R[x, y]).FG
⊢ f.IsIntegralElem z
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g : G
x y : ↥(integralClosure R K)
⊢ g • (x * y) = g • x * g • y

Tactic:
ext; exact smul_mul' g (x : K) (y : K)

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 : ℕ
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
s : Finset n
⊢ det (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))

Tactic:
rw [h_map]

Goal state after:
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
s : Finset n
⊢ (map (s.piecewise M 1) ⇑C).det = C (det (s.piecewise M 1))
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h₁ : p.natDegree ≤ n
h₂ : n = p.natDegree
⊢ p.coeff n = p.leadingCoeff

Tactic:
subst h₂

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
h₁ : p.natDegree ≤ p.natDegree
⊢ p.coeff p.natDegree = p.leadingCoeff
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inr.inr.cons.h
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
a : R
s : Multiset R
IH : ((Multiset.map (fun x ↦ X + C x) s).prod.scaleRoots r).Splits
⊢ (X + C a).leadingCoeff * (Multiset.map (fun x ↦ X + C x) s).prod.leadingCoeff ≠ 0

Tactic:
simp only [leadingCoeff_X_add_C, one_mul, ne_eq, leadingCoeff_eq_zero]

Goal state after:
case inr.inr.cons.h
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
a : R
s : Multiset R
IH : ((Multiset.map (fun x ↦ X + C x) s).prod.scaleRoots r).Splits
⊢ ¬(Multiset.map (fun x ↦ X + C x) s).prod = 0
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
r : R
hr : IsUnit r
⊢ (p.scaleRoots r).roots = Multiset.map (fun x ↦ r * x) p.roots

Tactic:
ext a
  have : Function.Bijective (α := R) (r * ·) := IsUnit.isUnit_iff_mulLeft_bijective.mp hr
  obtain ⟨a, rfl⟩ := this.2 a
  simp [Multiset.count_map_eq_count' _ p.roots this.1 a,
    rootMultiplicity_scaleRoots _ hr.isRegular.left]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
⊢ (f.comp (-X)).Splits

Tactic:
refine Submonoid.closure_induction ?_ (by simp)
    (fun f g _ _ hf hg ↦ mul_comp_neg_X f g ▸ hf.mul hg) hf
  · rintro f (⟨a, rfl⟩ | ⟨a, rfl⟩)
    · simp
    · rw [add_comp, X_comp, C_comp, neg_add_eq_sub, ← neg_sub]
      exact (X_sub_C a).neg

Goal state after:
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
⊢ Algebra.IsIntegral R ↥⊤ ↔ Algebra.IsIntegral R A

Tactic:
(Subalgebra.topEquiv (R := R) (A := A)).isIntegral_iff

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Algebra.IsIntegral R A ↔ Algebra.IsIntegral R A
Module: Mathlib.Algebra.Polynomial.Splits

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

Tactic:
simp [splits_mul']

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

Goal state before:
pp: S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
a✝ : g ∈ ⊤
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I) g' = g
⊢ g = (aeval ((Ideal.Quotient.mkₐ S I) X)) g'

Tactic:
nth_rw 1 [← hg, aeval_eq_sum_range' (lt_add_one _),
          as_sum_range_C_mul_X_pow g', map_sum]

Goal state after:
S : Type u_4
inst✝ : CommRing S
g✝ : S[X]
mon : g✝.Monic
I : Ideal S[X]
h : g✝ ∈ I
g : S[X] ⧸ I
a✝ : g ∈ ⊤
g' : S[X]
hg : (Ideal.Quotient.mkₐ S I) g' = g
⊢ ∑ x ∈ Finset.range (g'.natDegree + 1), (Ideal.Quotient.mkₐ S I) (C (g'.coeff x) * X ^ x) =
    ∑ i ∈ Finset.range (g'.natDegree + 1), g'.coeff i • (Ideal.Quotient.mkₐ S I) X ^ i
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f g : R[X]
hp : f.Splits
hp0 : f ≠ 0
hq : f.roots ≤ g.roots
⊢ f ∣ g

Tactic:
hp.eq_prod_roots,

Goal state after:
R : Type u_1
inst✝ : Field R
f g : R[X]
hp : f.Splits
hp0 : f ≠ 0
hq : f.roots ≤ g.roots
⊢ C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) f.roots).prod ∣ g
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective ⇑f
a : R
ha : IsUnit (f a)
p : R[X]
p_monic : p.Monic
hp : eval₂ f (↑ha.unit⁻¹) p = 0
⊢ -eval a (X * p.reverse.divX) = p.leadingCoeff

Tactic:
← coeff_zero_reverse,

Goal state after:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective ⇑f
a : R
ha : IsUnit (f a)
p : R[X]
p_monic : p.Monic
hp : eval₂ f (↑ha.unit⁻¹) p = 0
⊢ -eval a (X * p.reverse.divX) = p.reverse.coeff 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_1.refine_1
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
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
i : ℕ
hi : i ∈ q.support
⊢ (X ^ i).natDegree + (reflect N (q.coeff i)).natDegree ≤ q.natDegree + N

Tactic:
natDegree_pow_le,

Goal state after:
case refine_1.refine_1
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
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
i : ℕ
hi : i ∈ q.support
⊢ i * X.natDegree + (reflect N (q.coeff i)).natDegree ≤ q.natDegree + N
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ vanishingIdeal {x} = x.asIdeal

Tactic:
by simp [vanishingIdeal]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
r : R
hr : IsUnit r
s : Set R
x✝ : PrimeSpectrum R
⊢ x✝ ∈ zeroLocus (r • s) ↔ x✝ ∈ zeroLocus s

Tactic:
simp [Set.subset_def, ← Set.image_smul, Ideal.unit_mul_mem_iff_mem _ hr]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : M.IsPrime
⊢ (Multiset.map asIdeal {{ asIdeal := M, isPrime := h_prM }}).prod ≤ M

Tactic:
Multiset.map_singleton,

Goal state after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : M.IsPrime
⊢ {{ asIdeal := M, isPrime := h_prM }.asIdeal}.prod ≤ M
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : M = ⊤
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ M

pp: case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ M

Tactic:
· rw [htop]
    exact ⟨0, le_top⟩

Goal state after:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ M
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case right
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
hA_nont : Nontrivial A
hgt : ∀ J > ⊤, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : ⊤ ≠ ⊥
p_id : Ideal A
h_nzp : p_id ≠ ⊥
h_pp : p_id.IsPrime
⊢ (Multiset.map asIdeal {{ asIdeal := p_id, isPrime := h_pp }}).prod ≠ ⊥

Tactic:
Multiset.map_singleton,

Goal state after:
case right
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
hA_nont : Nontrivial A
hgt : ∀ J > ⊤, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : ⊤ ≠ ⊥
p_id : Ideal A
h_nzp : p_id ≠ ⊥
h_pp : p_id.IsPrime
⊢ {{ asIdeal := p_id, isPrime := h_pp }.asIdeal}.prod ≠ ⊥
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case h
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : M.IsPrime
⊢ (Multiset.map asIdeal {{ asIdeal := M, isPrime := h_prM }}).prod ≤ M ∧
    (Multiset.map asIdeal {{ asIdeal := M, isPrime := h_prM }}).prod ≠ ⊥

Tactic:
Multiset.map_singleton,

Goal state after:
case h
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : M.IsPrime
⊢ {{ asIdeal := M, isPrime := h_prM }.asIdeal}.prod ≤ M ∧ {{ asIdeal := M, isPrime := h_prM }.asIdeal}.prod ≠ ⊥
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : FaithfullyFlat R A
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsNoetherian A (A ⊗[R] M)
⊢ IsNoetherian R M

Tactic:
by
  rw [isNoetherian_iff'] at h ⊢
  exact (baseChangeOrderEmbedding R M A).wellFoundedGT

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case refine_2.refine_1
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x' : R
hx : f x' ∈ I
⊢ f x' ∈ { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }.asIdeal

Tactic:
exact Ideal.mem_map_of_mem f (h_I_p hx)

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mpr.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ Ideal.under R ⁻¹' J.minimalPrimes
⊢ ∀ ⦃y : Ideal A⦄, (fun q ↦ q.IsPrime ∧ Ideal.map (algebraMap R A) J ≤ q) y → y ≤ p → p ≤ y

Tactic:
intro I hI e

Goal state after:
case mpr.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ Ideal.under R ⁻¹' J.minimalPrimes
I : Ideal A
hI : I.IsPrime ∧ Ideal.map (algebraMap R A) J ≤ I
e : I ≤ p
⊢ p ≤ I
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_5
x : α
s : ι → Opens α
⊢ x ∈ iSup s ↔ ∃ i, x ∈ s i

Tactic:
rw [← SetLike.mem_coe]
  simp

Goal state after: