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

Goal state before:
pp: case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
⊢ (-1) ^ ↑i * (eval 0 (derivative 0) + M 0 i) * 0 = 0

pp: case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
⊢ ∀ (i_1 : Fin (n + 1)), submatrix 1 Fin.succ i.succAbove i_1 0 = 0

Tactic:
mul_zero

Goal state after:
case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
⊢ 0 = 0

case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
⊢ ∀ (i_1 : Fin (n + 1)), submatrix 1 Fin.succ i.succAbove i_1 0 = 0
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case empty
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
his : ∀ x ∈ ∅, IsIntegral R x
⊢ (Subalgebra.toSubmodule R[]).FG

Tactic:
refine ⟨{1}, Submodule.ext fun x => ?_⟩
    rw [Algebra.adjoin_empty, Finset.coe_singleton, ← one_eq_span, Algebra.toSubmodule_bot]

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

Goal state before:
pp: case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
⊢ ((expand K k) (X - C ((M ^ k) j j))).coeff m = ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) j j

Tactic:
map_sub,

Goal state after:
case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
⊢ ((expand K k) X - (expand K k) (C ((M ^ k) j j))).coeff m =
    ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) j j
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 : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
this : Function.Injective ⇑f
⊢ Module.Finite R ↥N

Tactic:
Module.Finite.iff_fg

Goal state after:
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 : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
this : Function.Injective ⇑f
⊢ 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
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * ((-1) ^ Fintype.card n * (1 - (scalar n) X * C.mapMatrix A).det) =
    (-1) ^ Fintype.card n * C A.det⁻¹ʳ * A.charpolyRev

Tactic:
by simp [charpolyRev, smul_eq_diagonal_mul]; ac_rfl

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

Goal state before:
pp: case inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h✝ : IsEmpty n
⊢ M.charpolyRev.coeff 1 = -M.trace

Tactic:
simp [charpolyRev, coeff_one]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : 1 - X • M.map ⇑C ∣ 1
⊢ M.charpolyRev ∣ 1

Tactic:
← det_one (R := R[X]) (n := n)

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : 1 - X • M.map ⇑C ∣ 1
⊢ M.charpolyRev ∣ det 1
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
⊢ ↑((i + k).choose k) * 0 = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
mul_zero

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0
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
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
by_cases! hkn : k ≤ n

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

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
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
⊢ (i - l).choose k * i.choose l = (k + l).choose k * 0

Tactic:
mul_zero

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
⊢ (i - l).choose k * i.choose l = 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
hil : i < l
⊢ (i - l).choose k * 0 = 0

Tactic:
mul_zero

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
hil : i < l
⊢ 0 = 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 : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
| (D ((fun i ↦ (X • M.map ⇑C) i) + fun i ↦ 1 i)).coeff k

Tactic:
rw [D.map_add_univ]

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
| (∑ s, D (s.piecewise (fun i ↦ (X • M.map ⇑C) i) fun i ↦ 1 i)).coeff k
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : i + 1 ≤ n
⊢ 0 = r ^ (i - n) * 0

Tactic:
mul_zero

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : i + 1 ≤ n
⊢ 0 = 0
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r s : R
⊢ (X + C r).scaleRoots s = X + C (r * s)

Tactic:
by
  nontriviality R
  ext (_ | _ | i) <;> simp

Goal state after:
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₂)
⊢ eval₂ f (f s * a) (p.scaleRoots s) =
    ∑ i ∈ (p.scaleRoots s).support, f (p.coeff i * s ^ (p.natDegree - i)) * (f s * a) ^ i

Tactic:
simp [eval₂_eq_sum, sum_def]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring S
inst✝ : CommSemiring R
p : S[X]
f : S →+* R
r : R
s : S
hr : eval₂ f r p = 0
⊢ f s ^ p.natDegree * 0 = 0

Tactic:
mul_zero

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring S
inst✝ : CommSemiring R
p : S[X]
f : S →+* R
r : R
s : S
hr : eval₂ f r p = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ (algebraMap R A) r ^ p.natDegree * 0 = 0

pp: case hsa
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ Commute ((algebraMap R A) r) a

pp: case hf
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ ∀ (s₁ s₂ : R), Commute ((algebraMap R A) s₁) ((algebraMap R A) s₂)

Tactic:
mul_zero

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ 0 = 0

case hsa
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ Commute ((algebraMap R A) r) a

case hf
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
a : A
r : R
ha : (aeval a) p = 0
⊢ ∀ (s₁ s₂ : R), Commute ((algebraMap R A) s₁) ((algebraMap R A) s₂)
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

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

Tactic:
mul_zero

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree > 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r s : R
⊢ (X - C r).scaleRoots s = X - C (r * s)

Tactic:
by
  nontriviality R
  ext (_ | _ | i) <;> simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((Polynomial.monomial n) a).Splits

Tactic:
by
  simp [← C_mul_X_pow_eq_monomial]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ ∀ f ∈ Multiset.map (fun x ↦ X + C x) m, f.Splits

Tactic:
simp [Splits.X_add_C]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : CommMonoid M
a : A
p : R[M]
a✝ : M
⊢ p.coeff a✝ • a = a * (algebraMap R A) (p.coeff a✝)

Tactic:
simp [Algebra.smul_def, Algebra.commutes]

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

Goal state before:
pp: 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
⊢ IsIntegral R x

Tactic:
refine ⟨scaleRoots p r, (monic_scaleRoots_iff r).2 p_monic, ?_⟩

Goal state after:
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 (p.scaleRoots r) = 0
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) * 0 = 0

Tactic:
mul_zero

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
⊢ 0 = 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
R' : Type u_3
inst✝ : CommRing R'
g : S →+* R'
p : S[X]
x : R'
hx : eval₂ g x p = 0
b : R
hb₁ : b ∈ M
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = b • p
⊢ g ((algebraMap R S) b) * 0 = 0

Tactic:
mul_zero

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
R' : Type u_3
inst✝ : CommRing R'
g : S →+* R'
p : S[X]
x : R'
hx : eval₂ g x p = 0
b : R
hb₁ : b ∈ M
hb₂ : Polynomial.map (algebraMap R S) (integerNormalization M p) = b • p
⊢ 0 = 0
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_mul

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
hx : IsIntegral Rₘ x
⊢ ∃ m, IsIntegral R (m • x)

Tactic:
rcases subsingleton_or_nontrivial Rₘ with _ | nontriv
  · have := (algebraMap Rₘ S).codomain_trivial
    exact ⟨1, Polynomial.X, Polynomial.monic_X, Subsingleton.elim _ _⟩
  obtain ⟨p, hp₁, hp₂⟩ := hx
  -- Porting note: obtain doesn't support side goals
  have :=
    lifts_and_natDegree_eq_and_monic (IsLocalization.scaleRoots_commonDenom_mem_lifts M p ?_) ?_
  · obtain ⟨p', hp'₁, -, hp'₂⟩ := this
    refine ⟨IsLocalization.commonDenom M p.support p.coeff, p', hp'₂, ?_⟩
    rw [IsScalarTower.algebraMap_eq R Rₘ S, ← Polynomial.eval₂_map, hp'₁, Submonoid.smul_def,
      Algebra.smul_def, IsScalarTower.algebraMap_apply R Rₘ S]
    exact Polynomial.scaleRoots_eval₂_eq_zero _ hp₂
  · rw [hp₁.leadingCoeff]
    exact one_mem _
  · rwa [Polynomial.monic_scaleRoots_iff]

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✝ : Algebra.IsIntegral R S
I : Ideal S
hI : I.IsMaximal
this : (comap (algebraMap R S) I).IsPrime
⊢ IsField (S ⧸ I)

Tactic:
rwa [← Quotient.maximal_ideal_iff_isField_quotient]

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

Goal state before:
pp: case right.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : Ideal R
hp : p.IsPrime
hI : (p.prod ⊤).IsPrime
⊢ ∃ a, primeSpectrumProdOfSum R S a = { asIdeal := p.prod ⊤, isPrime := hI }

Tactic:
exact ⟨Sum.inl ⟨p, hp⟩, rfl⟩

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

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

Tactic:
· simp [Set.mem_singleton_iff.mp h]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsLocalRing R
inst✝³ : CommRing S
inst✝² : IsLocalRing S
inst✝¹ : CommRing T
inst✝ : IsLocalRing T
f : R ≃+* S
x : ResidueField R
⊢ (map ↑f.symm) ((map ↑f) x) = x

Tactic:
simp only [map_map, RingEquiv.symm_comp, map_id, RingHom.id_apply]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : IsLocalRing R
inst✝¹² : CommRing S
inst✝¹¹ : IsLocalRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : IsLocalRing T
inst✝⁸ : Algebra R S
inst✝⁷ : IsLocalHom (algebraMap R S)
R₀ : Type u_4
inst✝⁶ : CommRing R₀
inst✝⁵ : Algebra R₀ R
inst✝⁴ : Algebra R₀ S
inst✝³ : IsScalarTower R₀ R S
inst✝² : IsLocalRing R₀
inst✝¹ : IsLocalHom (algebraMap R₀ R)
inst✝ : IsLocalHom (algebraMap R₀ S)
⊢ IsScalarTower (ResidueField R₀) (ResidueField R) (ResidueField S)

Tactic:
refine .of_algebraMap_eq fun x ↦ ?_
  obtain ⟨x, rfl⟩ := residue_surjective x
  simp [← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
y : S
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x

Tactic:
obtain ⟨a, ha⟩ := H (IsLocalization.mk' _ y (1 : P.primeCompl))

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
H : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
y : S
a : Localization.AtPrime (Ideal.comap f P)
ha : (Localization.localRingHom (Ideal.comap f P) P f ⋯) a = IsLocalization.mk' (Localization.AtPrime P) y 1
⊢ ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * y = c * f x
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FaithfullyFlat R S
inst✝ : FaithfullyFlat S M
N : Type (max u_1 u_3)
x✝³ : AddCommGroup N
x✝² : Module R N
N' : Type (max u_1 u_3)
x✝¹ : AddCommGroup N'
x✝ : Module R N'
f : N →ₗ[R] N'
aux : lTensor M f = 0
⊢ lTensor S f = 0

Tactic:
show f.lTensor S = (AlgebraTensorModule.map (A := S) LinearMap.id f).restrictScalars R by aesop,

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FaithfullyFlat R S
inst✝ : FaithfullyFlat S M
N : Type (max u_1 u_3)
x✝³ : AddCommGroup N
x✝² : Module R N
N' : Type (max u_1 u_3)
x✝¹ : AddCommGroup N'
x✝ : Module R N'
f : N →ₗ[R] N'
aux : lTensor M f = 0
⊢ ↑R (AlgebraTensorModule.map LinearMap.id f) = 0
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u_1
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FaithfullyFlat R M
⊢ FaithfullyFlat S (S ⊗[R] M)

Tactic:
rw [Module.FaithfullyFlat.iff_flat_and_rTensor_reflects_triviality]

Goal state after:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Type u_1
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FaithfullyFlat R M
⊢ Flat S (S ⊗[R] M) ∧
    ∀ (N : Type (max u_1 v)) [inst : AddCommGroup N] [inst_1 : Module S N],
      Subsingleton (N ⊗[S] (S ⊗[R] M)) → Subsingleton N
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case hy
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
x : S
s : ↥S⁰
⊢ IsIntegral K (mk' L 1 s)

Tactic:
rw [← isAlgebraic_iff_isIntegral, ← IsAlgebraic.invOf_iff, isAlgebraic_iff_isIntegral]

Goal state after:
case hy
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
x : S
s : ↥S⁰
⊢ IsIntegral K ⅟(mk' L 1 s)
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
mul_comm a.1.2,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑b).1 * (↑a).1 + (↑b).1 * ((↑b).1 * (↑a).2) = (↑b).1
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
h : i ∉ x.support
⊢ 0 = r i * 0

Tactic:
mul_zero

Goal state after:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
h : i ∉ x.support
⊢ 0 = 0
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case refine_2.refine_2
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 x' : R
hx' : x' ∈ p.asIdeal
heq : f x' = f x
⊢ f (x' - x) = 0

Tactic:
map_sub,

Goal state after:
case refine_2.refine_2
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 x' : R
hx' : x' ∈ p.asIdeal
heq : f x' = f x
⊢ f x' - f x = 0
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: 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 A
⊢ (Ideal.comap (algebraMap R A) J).minimalPrimes = Ideal.comap (algebraMap R A) '' J.minimalPrimes

Tactic:
conv_rhs => rw [← map_under S A J, minimalPrimes_map S]

Goal state after:
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 A
⊢ (Ideal.comap (algebraMap R A) J).minimalPrimes =
    Ideal.comap (algebraMap R A) '' Ideal.under R ⁻¹' (Ideal.under R J).minimalPrimes
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case refine_1
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) hf).comp (mapPiLocalization ↑f.symm ⋯) = RingHom.id (PiLocalization S)

Tactic:
rw [← mapPiLocalization_comp]
    simp_rw [RingEquiv.comp_symm, mapPiLocalization_id]

Goal state after:
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
⊢ IsOpenCover fun U ↦ ↑U

Tactic:
ext1
  simp [← hS.2]

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : IndiscreteTopology α
U : Opens α
⊢ U = ⊥ ∨ U = ⊤

Tactic:
by
  rw [← coe_eq_empty, ← coe_eq_univ, ← IndiscreteTopology.isOpen_iff]
  exact U.2

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
⊢ IsRetrocompact Set.univ

Tactic:
by
  simp +contextual [IsRetrocompact]

Goal state after: