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✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 - 1 * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A - U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A =
    1 + U * C * V * ⅟A - (U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A)

Tactic:
Matrix.one_mul

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 - U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A - U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A =
    1 + U * C * V * ⅟A - (U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A)
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ (((kroneckerMapBilinear f) A) B).det = (((kroneckerMapBilinear f) A) (1 * B)).det

Tactic:
Matrix.one_mul

Goal state after:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ (((kroneckerMapBilinear f) A) B).det = (((kroneckerMapBilinear f) A) B).det
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 α
i : n
this✝ : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x✝ : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e) A
this : A.det = ∑ x, A i x * A.adjugate x i
⊢ A.det = ∑ j, A i j * A.adjugate j i

Tactic:
exact this

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 α
this : A.det • (1 * A.adjugate.adjugate) = A.det ^ (Fintype.card n - 1) • A
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A

Tactic:
Matrix.one_mul

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
this : A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
⊢ (Function.Injective fun v ↦ v ᵥ* A) ↔ IsUnit A

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : Function.Injective fun v ↦ v ᵥ* A
⊢ IsUnit A

case refine_2
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : IsUnit A
⊢ Function.Injective fun v ↦ v ᵥ* A
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⁻¹⁻¹ = 1 * A⁻¹⁻¹

Tactic:
Matrix.one_mul

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A⁻¹⁻¹ = A⁻¹⁻¹
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: m : Type u_3
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
M : Matrix m m R
p q : m → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : ∀ (x : m), q x ↔ p x
⊢ (M.toSquareBlockProp p).det = (M.toSquareBlockProp q).det

Tactic:
by
  convert!
    Matrix.det_reindex_self (Equiv.subtypeEquivRight e)
      (toSquareBlockProp M q)

Goal state after:
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
⊢ h.unit⁻¹ • A * A.adjugate = 1

Tactic:
rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.val_inv_mul, one_smul]

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

Goal state before:
pp: 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 fun i ↦ ¬p i).det =
    (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i ↦ ¬p i).det

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

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ ∀ (p q : R[X]),
    (matPolyEquiv (single i j p)).coeff k = single i j (p.coeff k) →
      (matPolyEquiv (single i j q)).coeff k = single i j (q.coeff k) →
        (matPolyEquiv (single i j (p + q))).coeff k = single i j ((p + q).coeff k)

Tactic:
intro p

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p✝ : R[X]
k : ℕ
p : R[X]
⊢ ∀ (q : R[X]),
    (matPolyEquiv (single i j p)).coeff k = single i j (p.coeff k) →
      (matPolyEquiv (single i j q)).coeff k = single i j (q.coeff k) →
        (matPolyEquiv (single i j (p + q))).coeff k = single i j ((p + q).coeff k)
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j : n
⊢ ∀ (p q : Matrix n n R[X]),
    (matPolyEquiv p).coeff k i j = (p i j).coeff k →
      (matPolyEquiv q).coeff k i j = (q i j).coeff k → (matPolyEquiv (p + q)).coeff k i j = ((p + q) i j).coeff k

Tactic:
intro p

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j : n
p : Matrix n n R[X]
⊢ ∀ (q : Matrix n n R[X]),
    (matPolyEquiv p).coeff k i j = (p i j).coeff k →
      (matPolyEquiv q).coeff k i j = (q i j).coeff k → (matPolyEquiv (p + q)).coeff k i j = ((p + q) i j).coeff k
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
n : Type u_4
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : LinearOrder n
M : Matrix n n R
h : M.IsUpperTriangular
⊢ M.charpoly = ∏ i, (X - C (M i i))

Tactic:
simp [charpoly, det_of_isUpperTriangular h.charmatrix]

Goal state after:
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 α
C : Matrix l m α
D : Matrix l n α
inst✝ : Invertible A
⊢ fromBlocks A B C D = fromBlocks 1 0 (C * ⅟A) 1 * fromBlocks A 0 0 (D - C * ⅟A * B) * fromBlocks 1 (⅟A * B) 0 1

Tactic:
by
  simp only [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, add_zero, zero_add,
    Matrix.one_mul, Matrix.mul_one, invOf_mul_self, Matrix.mul_invOf_cancel_left,
    Matrix.mul_assoc, add_sub_cancel]

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: case add
n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun n R A ((toFunAlgHom n R A) x) = x
hy : invFun n R A ((toFunAlgHom n R A) y) = y
⊢ invFun n R A ((toFunAlgHom n R A) (x + y)) = x + y

Tactic:
map_add

Goal state after:
case add
n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun n R A ((toFunAlgHom n R A) x) = x
hy : invFun n R A ((toFunAlgHom n R A) y) = y
⊢ invFun n R A ((toFunAlgHom n R A) x + (toFunAlgHom n R A) y) = x + y
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
hle : Fintype.card n ≤ Fintype.card m
⊢ X ^ Fintype.card n * (A * B).charpoly = X ^ Fintype.card m * (B * A).charpoly

Tactic:
charpoly_mul_comm'

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
hle : Fintype.card n ≤ Fintype.card m
⊢ X ^ Fintype.card m * (B * A).charpoly = X ^ Fintype.card m * (B * A).charpoly
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u v : n → R
⊢ (vecMulVec u v).charpoly = X ^ Fintype.card n - (u ⬝ᵥ v) • X ^ (Fintype.card n - 1)

Tactic:
cases isEmpty_or_nonempty n
  · simp
  · have h : 1 ≤ Fintype.card n := NeZero.one_le
    rw [vecMulVec_eq (ι := Unit), charpoly_mul_comm_of_le (n := Unit) _ _ h, charpoly, charmatrix]
    simp [-Matrix.map_mul, mul_sub, ← pow_succ, h, dotProduct_comm, smul_eq_C_mul]

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ⨅ s, #↑↑s < ℵ₀ → ∃ S, S.Finite ∧ span R S = p

Tactic:
rintro h
    obtain ⟨s, hs⟩ : ⨅ (s : {s : Set M // span R s = p}), #s ∈
      Set.range (fun (s : {s : Set M // span R s = p}) ↦ #s) := csInf_mem ⟨#p, ⟨⟨p, by simp⟩, rfl⟩⟩
    refine ⟨s.1, ?_, s.2⟩
    simpa [← hs] using h

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
h : ¬Fintype.card n = 0
⊢ (∏ i, (X - C (M i i))).Monic

Tactic:
apply monic_prod_of_monic univ fun i : n => X - C (M i i)

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
h : ¬Fintype.card n = 0
⊢ ∀ i ∈ univ, (X - C (M i i)).Monic
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (hasseDeriv 1) f = derivative f

Tactic:
simp only [hasseDeriv_apply, derivative_apply, ← C_mul_X_pow_eq_monomial, Nat.choose_one_right,
    (Nat.cast_commute _ _).eq]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : n < k
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
Nat.choose_eq_zero_of_lt hkn,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : n < k
⊢ 0 = if n - k = i then ↑0 * r else 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ Finset.fold max 0 (natDegree ∘ fun n_1 ↦ (monomial (n_1 - n)) (↑(n_1.choose n) * p.coeff n_1)) p.support ≤
    p.natDegree - n

Tactic:
simp_rw [Function.comp, natDegree_monomial]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ Finset.fold max 0 (fun x ↦ if ↑(x.choose n) * p.coeff x = 0 then 0 else x - n) p.support ≤ p.natDegree - n
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
i : ℕ
⊢ (p.scaleRoots s).coeff i = p.coeff i * s ^ (p.natDegree - i)

Tactic:
simp +contextual [scaleRoots, coeff_monomial]

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

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

Tactic:
coeff_mul_C,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
⊢ p.integralNormalization.coeff i * p.leadingCoeff = (p.scaleRoots p.leadingCoeff).coeff i
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
n : ℕ
IH : p.leadingCoeff ^ n ≠ 0 → (p ^ n).scaleRoots r = p.scaleRoots r ^ n
hp : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ p.leadingCoeff ^ n ≠ 0

pp: case succ.h
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
n : ℕ
IH : p.leadingCoeff ^ n ≠ 0 → (p ^ n).scaleRoots r = p.scaleRoots r ^ n
hp : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0

Tactic:
· refine mt (by simp +contextual [pow_succ]) hp

Goal state after:
case succ.h
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
n : ℕ
IH : p.leadingCoeff ^ n ≠ 0 → (p ^ n).scaleRoots r = p.scaleRoots r ^ n
hp : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case succ.h
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
n : ℕ
IH : p.leadingCoeff ^ n ≠ 0 → (p ^ n).scaleRoots r = p.scaleRoots r ^ n
hp : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0

Tactic:
· rwa [leadingCoeff_pow' (mt (by simp +contextual [pow_succ]) hp), ← pow_succ]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : DivisionSemiring R
a b : R
hf : (C a * X + C b).natDegree ≤ 1
ha : ¬a = 0
⊢ (C a * X + C b).Splits

Tactic:
← mul_inv_cancel_left₀ ha b,

Goal state after:
case neg
R : Type u_1
inst✝ : DivisionSemiring R
a b : R
hf : (C a * X + C b).natDegree ≤ 1
ha : ¬a = 0
⊢ (C a * X + C (a * (a⁻¹ * b))).Splits
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
hf : f.Splits
hf0 : f ≠ 0
i : R →+* S
x : S
hx : x ∈ (map i f).roots
⊢ x ∈ i.range

Tactic:
hf.roots_map,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
hf : f.Splits
hf0 : f ≠ 0
i : R →+* S
x : S
hx : x ∈ Multiset.map (⇑i) f.roots
⊢ x ∈ i.range
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✝⁹ : CommRing B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsIntegralClosure A R B
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S B
inst✝² : IsScalarTower R S B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
x y : S
⊢ mk' A ((algebraMap S B) (x + y)) ⋯ = mk' A ((algebraMap S B) x + (algebraMap S B) y) ⋯

Tactic:
map_add

Goal state after:
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
hx : IsIntegral A x
⊢ IsIntegral R x

Tactic:
rcases hx with ⟨p, pmonic, hp⟩

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 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
⊢ IsIntegral R x
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ ∀ (p : R[X]) (a : R),
    p.coeff 0 = 0 →
      a ≠ 0 →
        (p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I) →
          p + C a ≠ 0 → eval₂ f r (p + C a) = 0 → ∃ i, (p + C a).coeff i ≠ 0 ∧ (p + C a).coeff i ∈ comap f I

Tactic:
intro p

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
⊢ ∀ (a : R),
    p.coeff 0 = 0 →
      a ≠ 0 →
        (p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I) →
          p + C a ≠ 0 → eval₂ f r (p + C a) = 0 → ∃ i, (p + C a).coeff i ≠ 0 ∧ (p + C a).coeff i ∈ comap f I
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ ∀ (p : R[X]) (a : R),
    p.coeff 0 = 0 →
      a ≠ 0 →
        (p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I) →
          p + C a ≠ 0 → eval₂ f r (p + C a) = 0 → ∃ i, (p + C a).coeff i ≠ 0 ∧ (p + C a).coeff i ∈ comap f I

Tactic:
intro p a coeff_eq_zero a_ne_zero _ _ hp

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
a : R
coeff_eq_zero : p.coeff 0 = 0
a_ne_zero : a ≠ 0
a✝¹ : p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I
a✝ : p + C a ≠ 0
hp : eval₂ f r (p + C a) = 0
⊢ ∃ i, (p + C a).coeff i ≠ 0 ∧ (p + C a).coeff i ∈ comap f I
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_3
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p : R[X]
⊢ ∀ (p : R[X]),
    p ≠ 0 →
      (p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I) →
        p * X ≠ 0 → eval₂ f r (p * X) = 0 → ∃ i, (p * X).coeff i ≠ 0 ∧ (p * X).coeff i ∈ comap f I

Tactic:
intro p

Goal state after:
case refine_3
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
r : S
r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0
hr : r ∈ I
p✝ p : R[X]
⊢ p ≠ 0 →
    (p ≠ 0 → eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ comap f I) →
      p * X ≠ 0 → eval₂ f r (p * X) = 0 → ∃ i, (p * X).coeff i ≠ 0 ∧ (p * X).coeff i ∈ comap f I
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
x : A
⊢ IsAlgebraic K x ↔ IsIntegral K x

Tactic:
by
  refine ⟨?_, IsIntegral.isAlgebraic⟩
  rintro ⟨p, hp, hpx⟩
  refine ⟨_, monic_mul_leadingCoeff_inv hp, ?_⟩
  rw [← aeval_def, map_mul, hpx, zero_mul]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus ↑(Ideal.span s) = zeroLocus s

Tactic:
ext x
  exact (Submodule.gi R R).gc s x.asIdeal

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ zeroLocus ↑I ⊆ zeroLocus ↑J ↔ J ≤ I.radical

Tactic:
by
  rw [subset_zeroLocus_iff_le_vanishingIdeal, vanishingIdeal_zeroLocus_eq_radical]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst✝¹² : CommRing Rf
inst✝¹¹ : CommRing Sf
inst✝¹⁰ : Algebra R Rf
inst✝⁹ : Algebra S Sf
inst✝⁸ : Algebra Rf Sf
inst✝⁷ : Algebra R Sf
inst✝⁶ : IsScalarTower R S Sf
inst✝⁵ : IsScalarTower R Rf Sf
M : Submonoid R
inst✝⁴ : IsLocalization M Rf
inst✝³ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst✝² : Algebra ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst✝¹ : IsScalarTower (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst✝ : IsScalarTower R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
s : Sf
hs : s ∈ integralClosure Rf Sf
x : S
m₁ : R
hm₁ : m₁ ∈ ↑M
e : s * (algebraMap R Sf) m₁ = (algebraMap S Sf) x
m₂ : R
hm₂ : m₂ ∈ M
hm₂s : IsIntegral R ((algebraMap R Sf) m₂ * s)
m₃ : R
hm₃ : m₃ ∈ M
hm₃s : IsIntegral R (m₃ • m₂ • x)
⊢ (algebraMap (↥(integralClosure Rf Sf)) Sf)
      (⟨s, hs⟩ *
        (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf))
          ↑(⟨m₃ • m₂ • x, hm₃s⟩, ⟨(algebraMap R ↥(integralClosure R S)) (m₁ * (m₂ * m₃)), ⋯⟩).2) =
    (algebraMap (↥(integralClosure Rf Sf)) Sf)
      ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf))
        (⟨m₃ • m₂ • x, hm₃s⟩, ⟨(algebraMap R ↥(integralClosure R S)) (m₁ * (m₂ * m₃)), ⋯⟩).1)

Tactic:
simp [← IsScalarTower.algebraMap_apply, e, ← mul_assoc, Algebra.smul_def]

Goal state after:
case refine_2
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst✝¹² : CommRing Rf
inst✝¹¹ : CommRing Sf
inst✝¹⁰ : Algebra R Rf
inst✝⁹ : Algebra S Sf
inst✝⁸ : Algebra Rf Sf
inst✝⁷ : Algebra R Sf
inst✝⁶ : IsScalarTower R S Sf
inst✝⁵ : IsScalarTower R Rf Sf
M : Submonoid R
inst✝⁴ : IsLocalization M Rf
inst✝³ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst✝² : Algebra ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst✝¹ : IsScalarTower (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst✝ : IsScalarTower R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
s : Sf
hs : s ∈ integralClosure Rf Sf
x : S
m₁ : R
hm₁ : m₁ ∈ ↑M
e : s * (algebraMap R Sf) m₁ = (algebraMap S Sf) x
m₂ : R
hm₂ : m₂ ∈ M
hm₂s : IsIntegral R ((algebraMap R Sf) m₂ * s)
m₃ : R
hm₃ : m₃ ∈ M
hm₃s : IsIntegral R (m₃ • m₂ • x)
⊢ (algebraMap S Sf) x * (algebraMap R Sf) m₂ * (algebraMap R Sf) m₃ =
    (algebraMap R Sf) m₃ * (algebraMap R Sf) m₂ * (algebraMap S Sf) x
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
m : Ideal R
inst✝ : m.IsMaximal
I : PrimeSpectrum R
⊢ I ∈ zeroLocus ↑m ↔ I ∈ {{ asIdeal := m, isPrime := ⋯ }}

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
m : Ideal R
inst✝ : m.IsMaximal
I : PrimeSpectrum R
h : I ∈ zeroLocus ↑m
⊢ I ∈ {{ asIdeal := m, isPrime := ⋯ }}

case refine_2
R : Type u
inst✝¹ : CommSemiring R
m : Ideal R
inst✝ : m.IsMaximal
I : PrimeSpectrum R
h : I ∈ {{ asIdeal := m, isPrime := ⋯ }}
⊢ I ∈ zeroLocus ↑m