mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single x 1
i j : m
⊢ (A * (of cols)ᵀ) i j = 1 i j

Tactic:
one_eq_pi_single,

Goal state after:
case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single x 1
i j : m
⊢ (A * (of cols)ᵀ) i j = Pi.single i 1 j
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
⊢ ∀ x ∈ univ, (fun j ↦ M i j) x * (fun j_1 ↦ N j_1 j) x = 0

Tactic:
intro k

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
k : m
⊢ k ∈ univ → (fun j ↦ M i j) k * (fun j_1 ↦ N j_1 j) k = 0
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 α
⊢ A⁻¹.det = A.det⁻¹ʳ

Tactic:
by
  by_cases h : IsUnit A.det
  · cases h.nonempty_invertible
    let := invertibleOfDetInvertible A
    rw [Ring.inverse_invertible, ← invOf_eq_nonsing_inv, det_invOf]
  cases isEmpty_or_nonempty n
  · rw [det_isEmpty, det_isEmpty, Ring.inverse_one]
  · rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit _ h, det_zero]

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

Goal state before:
pp: case pos
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : M.IsTwoBlockDiagonal
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

pp: case neg
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬M.IsTwoBlockDiagonal
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
· refine ⟨List.nil, List.nil, by simpa using H⟩

Goal state after:
case neg
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬M.IsTwoBlockDiagonal
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case neg
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : ¬IsUnit A
⊢ (A.submatrix ⇑e₁ ⇑e₂)⁻¹ = A⁻¹.submatrix ⇑e₂ ⇑e₁

Tactic:
have := (isUnit_submatrix_equiv e₁ e₂).not.mpr h

Goal state after:
case neg
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : ¬IsUnit A
this : ¬IsUnit (A.submatrix ⇑e₁ ⇑e₂)
⊢ (A.submatrix ⇑e₁ ⇑e₂)⁻¹ = A⁻¹.submatrix ⇑e₂ ⇑e₁
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
i j : n
p : R[X]
k : ℕ
⊢ ∀ (n_1 : ℕ) (a : R), (matPolyEquiv (single i j ((monomial n_1) a))).coeff k = single i j (((monomial n_1) a).coeff k)

Tactic:
intro k

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
⊢ ∀ (a : R), (matPolyEquiv (single i j ((monomial k) a))).coeff k✝ = single i j (((monomial k) a).coeff k✝)
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
⊢ (m i j).support ⊆ (matPolyEquiv m).support

Tactic:
intro k

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 : ℕ
⊢ k ∈ (m i j).support → k ∈ (matPolyEquiv m).support
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
PD : P (diagonal D)
L₁ L₂ : List (TransvectionStruct n 𝕜)
⊢ ∀ (E : Matrix n n 𝕜), P E → P ((List.map toMatrix L₁).prod * E * (List.map toMatrix L₂).prod)

Tactic:
E

Goal state after:
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
PD : P (diagonal D)
L₁ L₂ : List (TransvectionStruct n 𝕜)
E : Matrix n n 𝕜
⊢ P E → P ((List.map toMatrix L₁).prod * E * (List.map toMatrix L₂).prod)
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
⊢ (A + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det

Tactic:
← Matrix.mul_one A

Goal state after:
m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
⊢ (A * 1 + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
⊢ (A * 1 + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det

Tactic:
← Matrix.mul_nonsing_inv_cancel_left A (replicateCol ι u * replicateRow ι v),

Goal state after:
m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
⊢ (A * 1 + A * (A⁻¹ * (replicateCol ι u * replicateRow ι v))).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det

m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
⊢ IsUnit A.det
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: 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 α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
⊢ (A + U * V).det = A.det * (1 + V * A⁻¹ * U).det

Tactic:
← Matrix.mul_one A

Goal state after:
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 α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
⊢ (A * 1 + U * V).det = A.det * (1 + V * A⁻¹ * U).det
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (f.sum fun e a ↦ a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(polyBinomAux1 x y e a) * y ^ 2)) =
    ((f.sum fun e a ↦ a * x ^ e) + f.sum fun e a ↦ a * ↑e * x ^ (e - 1) * y) +
      f.sum fun e a ↦ a * ↑(polyBinomAux1 x y e a) * y ^ 2

Tactic:
simp [left_distrib, sum_add, mul_assoc]

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 ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : (PiToModule.fromMatrix R b) A = (PiToModule.fromEnd R b) f
h' : (PiToModule.fromMatrix R b) A' = (PiToModule.fromEnd R b) f'
⊢ (PiToModule.fromMatrix R b) A + (PiToModule.fromMatrix R b) A' =
    (PiToModule.fromEnd R b) f + (PiToModule.fromEnd R b) f'

Tactic:
h,

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 ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : (PiToModule.fromMatrix R b) A = (PiToModule.fromEnd R b) f
h' : (PiToModule.fromMatrix R b) A' = (PiToModule.fromEnd R b) f'
⊢ (PiToModule.fromEnd R b) f + (PiToModule.fromMatrix R b) A' = (PiToModule.fromEnd R b) f + (PiToModule.fromEnd R b) f'
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case refine_1
R : Type u_6
A : Type u_7
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : (aeval x) f = 0
a✝ : Nontrivial A
hf1 : f ≠ 1
s : A
hs : s ∈ ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range f.natDegree))
⊢ s ∈ ↑(Subalgebra.toSubmodule R[x])

pp: case refine_2
R : Type u_6
A : Type u_7
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : (aeval x) f = 0
a✝ : Nontrivial A
hf1 : f ≠ 1
r : A
hr : r ∈ Subalgebra.toSubmodule R[x]
⊢ r ∈ span R ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range f.natDegree))

Tactic:
· rcases Finset.mem_image.1 (SetLike.mem_coe.mp hs) with ⟨k, -, rfl⟩
    exact (Algebra.adjoin R {x}).pow_mem (Algebra.subset_adjoin rfl) k

Goal state after:
case refine_2
R : Type u_6
A : Type u_7
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : (aeval x) f = 0
a✝ : Nontrivial A
hf1 : f ≠ 1
r : A
hr : r ∈ Subalgebra.toSubmodule R[x]
⊢ r ∈ span R ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range f.natDegree))
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case refine_2
R : Type u_6
A : Type u_7
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : (aeval x) f = 0
a✝ : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : (aeval x) p ∈ (aeval x).range
⊢ (aeval x) (p %ₘ f) ∈ span R ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range f.natDegree))

Tactic:
← sum_C_mul_X_pow_eq (p %ₘ f),

Goal state after:
case refine_2
R : Type u_6
A : Type u_7
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : (aeval x) f = 0
a✝ : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : (aeval x) p ∈ (aeval x).range
⊢ (aeval x) ((p %ₘ f).sum fun n a ↦ C a * X ^ n) ∈ span R ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range f.natDegree))
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : CommRing T
inst✝² : Ring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
⊢ eval (ψ a) (Polynomial.map ((algebraMap T U).comp φ) p) = 0

Tactic:
h,

Goal state after:
R : Type u_5
S : Type u_6
T : Type u_7
U : Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : CommRing T
inst✝² : Ring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
a : S
ha : IsIntegral R a
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) a p = 0
⊢ eval (ψ a) (Polynomial.map (ψ.comp (algebraMap R S)) p) = 0
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]
n : ℕ
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
⊢ ∀ (n_1 : ℕ), (erase n p).coeff n_1 ∈ f.rangeS

Tactic:
intro k

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
k : ℕ
⊢ (erase n p).coeff k ∈ f.rangeS
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
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : 2 < i
⊢ M.charpoly.natDegree < i

Tactic:
simpa [charpoly_natDegree_eq_dim, hn] using hi

Goal state after:
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]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k) (g k)
hq : map f q = p
k : ℕ
h : g k = 0
⊢ f (g k) = 0

Tactic:
h,

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k) (g k)
hq : map f q = p
k : ℕ
h : g k = 0
⊢ f 0 = 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
k : ℕ
⊢ eval r ((hasseDeriv k) f) = coeff 0 k

Tactic:
h,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0
k : ℕ
⊢ 0 = 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 ∈ p.support, f s ^ p.natDegree * (f (p.coeff i) * a ^ i) = f s ^ p.natDegree * eval₂ f a p

Tactic:
by simp [← Finset.mul_sum, eval₂_eq_sum, sum_def]

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

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

Tactic:
by
  induction n with
  | zero => simp
  | succ n IH =>
    rw [pow_succ, mul_scaleRoots', IH, pow_succ]
    · refine mt (by simp +contextual [pow_succ]) hp
    · rwa [leadingCoeff_pow' (mt (by simp +contextual [pow_succ]) hp), ← pow_succ]

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

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

Tactic:
(monic_multiset_prod_of_monic _ _ fun a _ ↦ monic_X_add_C _).leadingCoeff

Goal state after:
case inr.inr.h
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ (C p.leadingCoeff).leadingCoeff * 1 ≠ 0
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
h : p.coeff n = 0
⊢ 0 = ↑(p.coeff n)

Tactic:
h,

Goal state after:
R : Type u_1
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
h : p.coeff n = 0
⊢ 0 = ↑0
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 0
| (Multiset.map (fun x ↦ X - C x) f.roots).prod.natDegree

Tactic:
natDegree_multiset_prod_X_sub_C_eq_card

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 0
| f.roots.card
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: case e
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : (algebraMap R B) r * y = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ eval₂ (algebraMap R B) x = ⇑(aeval ((algebraMap R B) r * (x * y)))

Tactic:
rw [Algebra.commutes] at hr ⊢

Goal state after:
case e
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : y * (algebraMap R B) r = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ eval₂ (algebraMap R B) x = ⇑(aeval (x * y * (algebraMap R B) r))
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: case right
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
this : p ≠ 0
⊢ f p.leadingCoeff ^ (p.natDegree - 1) * eval₂ f x p = 0

Tactic:
h,

Goal state after:
case right
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ p.natDegree
this : p ≠ 0
⊢ f p.leadingCoeff ^ (p.natDegree - 1) * 0 = 0
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : f (p.coeff 0) = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
⊢ C (f (p.coeff 0)) = 0

Tactic:
h,

Goal state after:
case neg
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : f (p.coeff 0) = 0
h' : p.natDegree = 0
hp : ¬Polynomial.map f p = 0
⊢ C 0 = 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case mp.refine_1
A : Type u_3
K : Type u_4
C : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
p : A[X]
hp : p ≠ 0
px : (aeval x) p = 0
h : Polynomial.map (algebraMap A K) p = 0
i : ℕ
⊢ p.coeff i = coeff 0 i

Tactic:
have : algebraMap A K (p.coeff i) = 0 :=
        _root_.trans (Polynomial.coeff_map _ _).symm (by simp [h])
      exact to_map_eq_zero_iff.mp this

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

Goal state before:
pp: A : Type u_3
inst✝⁹ : CommRing A
L : Type u_5
inst✝⁸ : Field L
inst✝⁷ : Algebra A L
C : Type u_6
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : Algebra.IsAlgebraic A L
inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
h : (algebraMap A C) x = 0
⊢ (algebraMap C L) ((algebraMap A C) x) = 0

Tactic:
h,

Goal state after:
A : Type u_3
inst✝⁹ : CommRing A
L : Type u_5
inst✝⁸ : Field L
inst✝⁷ : Algebra A L
C : Type u_6
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : Algebra.IsAlgebraic A L
inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
h : (algebraMap A C) x = 0
⊢ (algebraMap C L) 0 = 0
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst✝ : NoZeroDivisors S
h : Function.Injective ⇑(algebraMap R S)
⊢ Algebra.IsAlgebraic R[X] S[X]

pp: case neg
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst✝ : NoZeroDivisors S
h : ¬Function.Injective ⇑(algebraMap R S)
⊢ Algebra.IsAlgebraic R[X] S[X]

Tactic:
· have := h.noZeroDivisors _ (map_zero _) (map_mul _); infer_instance

Goal state after:
case neg
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst✝ : NoZeroDivisors S
h : ¬Function.Injective ⇑(algebraMap R S)
⊢ Algebra.IsAlgebraic R[X] S[X]
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
z : A
z' : S
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst✝ : NoZeroDivisors S
h : Function.Injective ⇑(algebraMap R S)
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)

pp: case neg
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
z : A
z' : S
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst✝ : NoZeroDivisors S
h : ¬Function.Injective ⇑(algebraMap R S)
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)

Tactic:
· have := h.noZeroDivisors _ (map_zero _) (map_mul _); infer_instance

Goal state after:
case neg
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
z : A
z' : S
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst✝ : NoZeroDivisors S
h : ¬Function.Injective ⇑(algebraMap R S)
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
I : Ideal R
inst✝ : I.IsPrime
x s : R
hs : s ∈ I.primeCompl
⊢ (IsLocalRing.residue (Localization.AtPrime I)) (IsLocalization.mk' (Localization.AtPrime I) x ⟨s, hs⟩) *
      (algebraMap (R ⧸ I) I.ResidueField) ↑((Ideal.Quotient.mk I) x, ⟨(Ideal.Quotient.mk I) s, ⋯⟩).2 =
    (algebraMap (R ⧸ I) I.ResidueField) ((Ideal.Quotient.mk I) x, ⟨(Ideal.Quotient.mk I) s, ⋯⟩).1

Tactic:
· simp [IsScalarTower.algebraMap_eq R (Localization.AtPrime I) I.ResidueField, ← map_mul]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ (mapPiLocalization ↑f.symm).comp (mapPiLocalization ↑f) = RingHom.id (PiLocalization R)

Tactic:
· rw [← mapPiLocalization_comp, RingEquiv.symm_comp, mapPiLocalization_id]

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ ↑L = univ ↔ L = ⊤

Tactic:
← coe_top,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ ↑L = ↑⊤ ↔ L = ⊤
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ IsOpen[inst✝] (range f) ↔ ∀ (x : ι), IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' range f)

Tactic:
exact hU.isOpen_iff_coe_preimage

Goal state after: