mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
M : Type u_9
N : Type u_10
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : Semiring S
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : AddCommMonoid N
inst✝¹² : Algebra R S
inst✝¹¹ : Module R M
inst✝¹⁰ : Module S M
inst✝⁹ : Module R N
inst✝⁸ : IsScalarTower R S M
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
ia : l
ja : m
ib : n
jb : p
a : M
b : N
⊢ (kroneckerTMulLinearEquiv l m n p R S M N).symm (single (ia, ib) (ja, jb) (a ⊗ₜ[R] b)) =
    single ia ja a ⊗ₜ[R] single ib jb b

Tactic:
LinearEquiv.symm_apply_eq,

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
M : Type u_9
N : Type u_10
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : Semiring S
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : AddCommMonoid N
inst✝¹² : Algebra R S
inst✝¹¹ : Module R M
inst✝¹⁰ : Module S M
inst✝⁹ : Module R N
inst✝⁸ : IsScalarTower R S M
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
ia : l
ja : m
ib : n
jb : p
a : M
b : N
⊢ single (ia, ib) (ja, jb) (a ⊗ₜ[R] b) =
    (kroneckerTMulLinearEquiv l m n p R S M N) (single ia ja a ⊗ₜ[R] single ib jb b)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case hmul
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : M.det ≠ 0
hdiag : ∀ (D : n → 𝕜), (diagonal D).det ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)
Q : Matrix n n 𝕜 → Prop := fun N ↦ N.det ≠ 0 ∧ P N
A : Matrix n n 𝕜
⊢ ∀ (B : Matrix n n 𝕜), Q A → Q B → Q (A * B)

Tactic:
B

Goal state after:
case hmul
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : M.det ≠ 0
hdiag : ∀ (D : n → 𝕜), (diagonal D).det ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)
Q : Matrix n n 𝕜 → Prop := fun N ↦ N.det ≠ 0 ∧ P N
A B : Matrix n n 𝕜
⊢ Q A → Q B → Q (A * B)
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
⊢ (A * B).charpoly = X ^ (Fintype.card m - Fintype.card n) * (B * A).charpoly

Tactic:
by
  rw [← (isRegular_X_pow _).left.eq_iff, ← mul_assoc, ← pow_add,
    Nat.add_sub_cancel' hle, charpoly_mul_comm']

Goal state after:
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
M : (Matrix n n R)ˣ
N : Matrix n n R
⊢ ((↑M)⁻¹ * N * ↑M).charpoly = N.charpoly

Tactic:
simpa using charpoly_units_conj M⁻¹ N

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 n m α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible (D - C * ⅟A * B)
⊢ Invertible (fromBlocks A B C D)

Tactic:
letI := fromBlocks₂₂Invertible D C B A

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 α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible (D - C * ⅟A * B)
this : Invertible (fromBlocks D C B A) := D.fromBlocks₂₂Invertible C B A
⊢ Invertible (fromBlocks A B C D)
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case neg.refine_2
R : Type u_1
inst✝ : CommRing R
k : ℕ
hind :
  ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : ¬P.natDegree = 0
P₁ : R[X] := P.eraseLead
hP₁ : P₁ = P.eraseLead
hdeg₂ : P.eraseLead.natDegree < P.natDegree
⊢ IsUnit (P₁.coeff 0)

Tactic:
simp_rw [P₁, eraseLead_coeff_of_ne _ (Ne.symm hdeg), hunit]

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

Goal state before:
pp: case neg.refine_3
R : Type u_1
inst✝ : CommRing R
k : ℕ
hind :
  ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : ¬P.natDegree = 0
P₁ : R[X] := P.eraseLead
hP₁ : P₁ = P.eraseLead
hdeg₂ : P.eraseLead.natDegree < P.natDegree
i : ℕ
hi : i ≠ 0
⊢ IsNilpotent (P₁.coeff i)

Tactic:
by_cases! H : i ≤ P₁.natDegree

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
k : ℕ
hind :
  ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : ¬P.natDegree = 0
P₁ : R[X] := P.eraseLead
hP₁ : P₁ = P.eraseLead
hdeg₂ : P.eraseLead.natDegree < P.natDegree
i : ℕ
hi : i ≠ 0
H : i ≤ P₁.natDegree
⊢ IsNilpotent (P₁.coeff i)

case neg
R : Type u_1
inst✝ : CommRing R
k : ℕ
hind :
  ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : ¬P.natDegree = 0
P₁ : R[X] := P.eraseLead
hP₁ : P₁ = P.eraseLead
hdeg₂ : P.eraseLead.natDegree < P.natDegree
i : ℕ
hi : i ≠ 0
H : P₁.natDegree < i
⊢ IsNilpotent (P₁.coeff i)
Module: Mathlib.RingTheory.Finiteness.Subalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
hm : M.FG
hn : N.FG
⊢ (M * N).FG

Tactic:
mul_eq_map₂

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
hm : M.FG
hn : N.FG
⊢ (Submodule.map₂ (LinearMap.mul R A) M N).FG
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
c : n ≃ n
hc : c ∈ univ.erase (Equiv.refl n)
⊢ ↑↑(Equiv.Perm.sign c) * ∏ i, M.charmatrix (c i) i ∈ degreeLT R (Fintype.card n - 1)

Tactic:
rw [← C_eq_intCast, C_mul']

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ univ.erase (Equiv.refl n)
⊢ ↑↑(Equiv.Perm.sign c) • ∏ i, M.charmatrix (c i) i ∈ degreeLT R (Fintype.card n - 1)
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⨅ s, #↑↑s = 0

Tactic:
exact Cardinal.iInf_eq_zero_iff.mpr (Or.inr ⟨⟨∅, by simp⟩, by simp⟩)

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
h✝ : Nonempty n
a✝ : Nontrivial R
⊢ M.trace = -M.charpoly.nextCoeff

Tactic:
simp [trace_eq_neg_charpoly_coeff, nextCoeff]

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

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

pp: 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

Tactic:
· let : Algebra R T := φ.toRingHom.toAlgebra
    let : IsScalarTower R T S :=
      ⟨fun r t s ↦ by simp only [Algebra.smul_def, map_mul, ← h, mul_assoc]; rfl⟩
    exact IsIntegral.tower_top ha

Goal state after:
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.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑l !) * (↑i ! / (↑(k + l)! * ↑(i - l - k)!))

Tactic:
field

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
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
⊢ ∑ s, (X ^ #s • D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i)).coeff k =
    ∑ x ∈ powersetCard k univ, detRowAlternating (M.submatrix Subtype.val Subtype.val)

Tactic:
simp_rw [h_det, smul_eq_mul, mul_comm (X ^ _) (C _)]

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
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
⊢ ∑ x, (C (det (x.piecewise M 1)) * X ^ #x).coeff k =
    ∑ x ∈ powersetCard k univ, detRowAlternating (M.submatrix Subtype.val Subtype.val)
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
hi' : i ∉ (p.scaleRoots s).support
⊢ p.coeff i * s ^ (p.natDegree - i) = 0

Tactic:
by simpa using hi'

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
A : Type u_1
inst✝ : Semiring A
h : 1 ≤ p.natDegree
f : R →+* A
x : A
h₁ : Commute (f p.leadingCoeff) x
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
⊢ eval₂ f (f p.leadingCoeff * x) p.integralNormalization = f p.leadingCoeff ^ (p.natDegree - 1) * eval₂ f x p

Tactic:
by
  rw [eval₂_eq_sum_range, eval₂_eq_sum_range, Finset.mul_sum]
  apply Finset.sum_congr
  · rw [natDegree_eq_of_degree_eq p.degree_integralNormalization]
  intro n _hn
  rw [h₁.mul_pow, ← mul_assoc, ← f.map_pow, ← f.map_mul,
    integralNormalization_coeff_mul_leadingCoeff_pow _ h, f.map_mul, h₂.eq, f.map_pow, mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : CommSemiring A
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra S A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : Algebra S B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : IsPushout R S A B
x : A[M]
⊢ ↑((rTensorEquivAlgEquiv R S S A).trans (mapAlgEquiv S M (IsPushout.equiv R S A B))) (1 ⊗ₜ[R] x) =
    (IsScalarTower.toAlgHom R A[M] B[M]).toLinearMap x

Tactic:
by
    induction x using induction_linear <;> simp_all [IsPushout.equiv_tmul]

Goal state after:
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
⊢ Polynomial.map f p = 0

Tactic:
rw [eq_C_of_natDegree_eq_zero h', map_C, h, C_eq_zero]

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
⊢ eval₂ ((Ideal.Quotient.mk I).comp (algebraMap S S[X])) ((Ideal.Quotient.mk I) X) g = 0

Tactic:
by
  rw [← (Ideal.Quotient.eq_zero_iff_mem.mpr h), eval₂_eq_sum_range]
  nth_rw 3 [(as_sum_range_C_mul_X_pow g)]
  simp only [map_sum, algebraMap_eq, RingHom.coe_comp, Function.comp_apply, map_mul, map_pow]

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
this✝ : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
  IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
this : Algebra.IsIntegral Rₚ Sₚ
Qₚ_max : (comap (algebraMap Rₚ Sₚ) Qₚ).IsMaximal
⊢ comap (algebraMap R S) (comap (algebraMap S Sₚ) Qₚ) = P

Tactic:
convert! Localization.AtPrime.under_maximalIdeal (I := P)

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
this✝ : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
  IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
this : Algebra.IsIntegral Rₚ Sₚ
Qₚ_max : (comap (algebraMap Rₚ Sₚ) Qₚ).IsMaximal
⊢ comap (algebraMap R S) (comap (algebraMap S Sₚ) Qₚ) = under R (IsLocalRing.maximalIdeal (Localization P.primeCompl))
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ₘ
x : S
inst✝ : Away x Sₘ
p : R[X]
hpm : p.Monic
hp : eval₂ (algebraMap R Sₘ) ((algebraMap S Sₘ) x) p = 0
⊢ IsIntegral R x

Tactic:
simp only [IsScalarTower.algebraMap_eq R S Sₘ, IsLocalization.map_eq_zero_iff (.powers x),
    Subtype.exists, Submonoid.mem_powers_iff, ← hom_eval₂, exists_prop, exists_exists_eq_and] at hp

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ₘ
x : S
inst✝ : Away x Sₘ
p : R[X]
hpm : p.Monic
hp : ∃ a, x ^ a * eval₂ (algebraMap R S) x p = 0
⊢ IsIntegral R x
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
⊢ 1 ∈ ↑⊤

Tactic:
trivial

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

Goal state before:
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:
← Polynomial.map_injective_iff

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 (map (algebraMap R S))
⊢ Algebra.IsAlgebraic R[X] S[X]
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ ∃ a, (Localization.localRingHom (Ideal.comap f P) P f ⋯) a = Localization.mk y ⟨t, h⟩

Tactic:
refine ⟨Localization.mk (yx * ts) ⟨ys * tx, Submonoid.mul_mem _ hy ?_⟩, ?_⟩

Goal state after:
case mpr.refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ tx ∈ (Ideal.comap f P).primeCompl

case mpr.refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
y✝ : Localization.AtPrime P
x✝ : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : f ys ∉ P
ey : yc * f ys * y = yc * f yx
tx ts : R
yt : S
hyt : yt ∉ P
ht : f ts ∉ P
et : yt * f ts * t = yt * f tx
⊢ (Localization.localRingHom (Ideal.comap f P) P f ⋯) (Localization.mk (yx * ts) ⟨ys * tx, ⋯⟩) =
    Localization.mk y ⟨t, h⟩
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑a).2 + (↑a).1 = 1

pp: case refine_3
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑a).2 + (↑b).1 = 1

Tactic:
· rw [add_comm, a.2.2]

Goal state after:
case refine_3
R : Type u_1
inst✝ : CommSemiring R
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑a).2 + (↑b).1 = 1
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ Function.Injective ⇑((TensorProduct.mk A B M) 1)

Tactic:
← Module.FaithfullyFlat.lTensor_injective_iff_injective A B

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ Function.Injective ⇑(lTensor B ((TensorProduct.mk A B M) 1))
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: case refine_1
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
⊢ (Ideal.Quotient.mk I) s ∈ (R ⧸ I)⁰

Tactic:
mem_nonZeroDivisors_iff_ne_zero,

Goal state after:
case refine_1
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
⊢ (Ideal.Quotient.mk I) s ≠ 0
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : FaithfullyFlat A B
⊢ FaithfulSMul A B

Tactic:
constructor
  intro a₁ a₂ ha
  apply Module.FaithfullyFlat.tensorProduct_mk_injective (A := A) (B := B) A
  simp only [TensorProduct.mk_apply]
  rw [← mul_one a₁, ← mul_one a₂]
  simp only [← smul_eq_mul, ← TensorProduct.smul_tmul, ha (1 : B)]

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

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
x : K
⊢ x ∈ (mapToFractionRing K S B hS).range → ∃ a s, ∃ (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩

Tactic:
rintro ⟨x, rfl⟩

Goal state after:
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
x : B
⊢ ∃ a s, ∃ (hs : s ∈ S), (mapToFractionRing K S B hS).toRingHom x = IsLocalization.mk' K a ⟨s, ⋯⟩
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
⊢ comap f '' Set.univ = zeroLocus ↑(ker f)

Tactic:
convert! image_comap_zeroLocus_eq_zeroLocus_comap _ _ hf _

Goal state after:
case e'_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
⊢ Set.univ = zeroLocus ↑⊥
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: case h
X : Type u_1
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis (range fun i ↦ ↑i)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun i ↦ ↑i
s : Set ↑b
hs : s.Finite
hU : U = ⋃ i ∈ s, ↑i
this : Finite ↑s
x✝ : Fintype ↑s := ⋯
⊢ U = ⋃₀ (Subtype.val '' ↑s.toFinset)

Tactic:
simp [hU]

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

Goal state before:
pp: ι : Type u_5
R : ι → Type u_4
inst✝¹ : (i : ι) → CommSemiring (R i)
inst✝ : ∀ (i : ι), Nontrivial (R i)
h : Infinite ι
⊢ ¬Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))

Tactic:
exact toPiLocalization_not_surjective_of_infinite _

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
h : IsInducing f
⊢ IsInducing (Subtype.val ∘ s.restrictPreimage f)

Tactic:
isInducing_iff_nhds,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
h : ∀ (x : α), 𝓝 x = comap f (𝓝 (f x))
⊢ ∀ (x : ↑(f ⁻¹' s)), 𝓝 x = comap (Subtype.val ∘ s.restrictPreimage f) (𝓝 ((Subtype.val ∘ s.restrictPreimage f) x))
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
h : IsInducing f
⊢ IsInducing (s.restrictPreimage f)

Tactic:
simp_rw [← IsInducing.subtypeVal.of_comp_iff, isInducing_iff_nhds, restrictPreimage,
    MapsTo.coe_restrict, domRestrict_eq, ← @Filter.comap_comap _ _ _ _ _ f,
    Function.comp_apply] at h ⊢
  intro a
  rw [← h, ← IsInducing.subtypeVal.nhds_eq_comap]

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
hs : IsLocallyClosed s
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ IsLocallyClosed (f ⁻¹' s)

Tactic:
obtain ⟨U, Z, hU, hZ, rfl⟩ := hs
  exact ⟨_, _, hU.preimage hf, hZ.preimage hf, preimage_inter⟩

Goal state after: