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

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
M✝ : Matrix n n α
⊢ f' (g M✝).adjugate = M✝.adjugate

Tactic:
rw [RingHom.map_adjugate, f'_inv]

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

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : B * A = 1
⊢ A.det * B.det = 1

Tactic:
rw [mul_comm, ← det_mul, h, det_one]

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

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A * B = 1
⊢ B.det * A.det = 1

Tactic:
rw [mul_comm, ← det_mul, h, det_one]

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

Goal state before:
pp: α : Type u_1
m' : α → Type u_6
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : (i : α) → Matrix (m' i) (m' i) R
⊢ (blockDiagonal' d).BlockTriangular Sigma.fst

Tactic:
rintro ⟨i, i'⟩ ⟨j, j'⟩ h

Goal state after:
α : Type u_1
m' : α → Type u_6
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : (i : α) → Matrix (m' i) (m' i) R
i : α
i' : m' i
j : α
j' : m' j
h : ⟨j, j'⟩.fst < ⟨i, i'⟩.fst
⊢ blockDiagonal' d ⟨i, i'⟩ ⟨j, j'⟩ = 0
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : α → Matrix m m R
⊢ (blockDiagonal d).BlockTriangular Prod.snd

Tactic:
rintro ⟨i, i'⟩ ⟨j, j'⟩ h

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ blockDiagonal d (i, i') (j, j') = 0
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ v i * (⅟(diagonal v).det * ∏ j ∈ univ.erase i, v j) = 1

Tactic:
rw [mul_left_comm, mul_prod_erase _ _ (Finset.mem_univ _), ← det_diagonal]

Goal state after:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ ⅟(diagonal v).det * (diagonal v).det = 1
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₁ : List (TransvectionStruct n 𝕜)
⊢ ∀ (L₂ : List (TransvectionStruct n 𝕜)) (E : Matrix n n 𝕜),
    P E → P ((List.map toMatrix L₁).prod * E * (List.map toMatrix L₂).prod)

Tactic:
L₂

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.RingTheory.MatrixAlgebra

Goal state before:
pp: 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
M : Matrix n n A
⊢ (toFunAlgHom n R A) (invFun n R A M) = M

Tactic:
simp only [invFun, map_sum, toFunAlgHom_apply]

Goal state after:
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
M : Matrix n n A
⊢ ∑ x, M x.1 x.2 • (single x.1 x.2 1).map ⇑(algebraMap R A) = M
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: case pos.intro
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 α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
val✝ : Invertible A
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹

Tactic:
cases hD.nonempty_invertible

Goal state after:
case pos.intro.intro
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 α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
val✝¹ : Invertible A
val✝ : Invertible D
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: case pos.intro
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 α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
val✝ : Invertible A
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹

Tactic:
cases hD.nonempty_invertible

Goal state after:
case pos.intro.intro
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 α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : IsUnit A
hD : IsUnit D
val✝¹ : Invertible A
val✝ : Invertible D
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
x y : R
hy : IsRadical y
h0 : y ≠ 0
hxy : x ∣ y
⊢ ∀ (x_1 : R), x ∣ x_1 ^ 2 → x ∣ x_1

Tactic:
by
  obtain ⟨z, rfl⟩ := hxy
  refine fun w dvd ↦ ((mul_dvd_mul_iff_right <| right_ne_zero_of_mul h0).mp <| hy 2 _ ?_)
  rw [mul_pow]
  gcongr
  exact dvd_pow_self _ two_ne_zero

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
hf : ∀ (b : ι), IsNilpotent (f b)
h_comm : ∀ (i j : ι), Commute (f i) (f j)
h : HasFiniteSupport f
⊢ IsNilpotent (if h : HasFiniteSupport f then ∑ i ∈ Finite.toFinset h, f i else 0)

Tactic:
dif_pos h

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
hf : ∀ (b : ι), IsNilpotent (f b)
h_comm : ∀ (i j : ι), Commute (f i) (f j)
h : HasFiniteSupport f
⊢ IsNilpotent (∑ i ∈ Finite.toFinset h, f i)
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
N : Submodule S M
s : Set M
hs : Cardinal.mk ↑s = (restrictScalars R N).spanRank
e : span R s = restrictScalars R N
⊢ N.spanRank ≤ (restrictScalars R N).spanRank

Tactic:
obtain rfl : span S s = N :=
    le_antisymm (span_le.mpr (span_le.mp e.le :)) (e.ge.trans (span_le_restrictScalars R S s))

Goal state after:
R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
s : Set M
hs : Cardinal.mk ↑s = (restrictScalars R (span S s)).spanRank
e : span R s = restrictScalars R (span S s)
⊢ (span S s).spanRank ≤ (restrictScalars R (span S s)).spanRank
Module: Mathlib.Algebra.Polynomial.Eval.Subring

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ f (p.coeff n) ∈ f.rangeS

Tactic:
exact Set.mem_range_self _

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

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ ↑p.coeffs ⊆ Set.range ⇑f → ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f

Tactic:
intro h n

Goal state after:
case mpr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ↑p.coeffs ⊆ Set.range ⇑f
n : ℕ
⊢ p.coeff n ∈ Set.range ⇑f
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case zero
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x, 1 = Fintype.card n
i : n
⊢ (M.charmatrix (c i) i).coeff 0 ∈ I ^ 1

Tactic:
pow_one,

Goal state after:
case zero
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x, 1 = Fintype.card n
i : n
⊢ (M.charmatrix (c i) i).coeff 0 ∈ I
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
⊢ eval 0 M.charpolyRev = 1

Tactic:
rw [charpolyRev, ← coe_evalRingHom, RingHom.map_det, ← det_one (R := R) (n := n)]
  have : (1 - (X : R[X]) • M.map C).map (eval 0) = 1 := by
    ext i j; rcases eq_or_ne i j with hij | hij <;> simp [hij, one_apply]
  congr

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ((hasseDeriv k) f).coeff n = ↑((n + k).choose k) * f.coeff (n + k)

Tactic:
by
  rw [hasseDeriv_apply, coeff_sum, sum_def, Finset.sum_eq_single (n + k), coeff_monomial]
  · simp
  · #adaptation_note
    /-- Prior to nightly-2025-08-14, this was working as
    `grind [coeff_monomial, Nat.choose_eq_zero_of_lt, Nat.cast_zero, zero_mul]` -/
    intro i _hi hink
    rw [coeff_monomial]
    by_cases hik : i < k
    · simp only [Nat.choose_eq_zero_of_lt hik, ite_self, Nat.cast_zero, zero_mul]
    · grind
  · intro h
    simp only [notMem_support_iff.mp h, monomial_zero_right, mul_zero, coeff_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
⊢ p.integralNormalization.coeff i * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
integralNormalization_coeff

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
⊢ (if p.degree = ↑i then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) * p.leadingCoeff ^ i =
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

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

Tactic:
integralNormalization_coeff

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
⊢ (if p.degree = ↑i then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) * p.leadingCoeff =
    (p.scaleRoots p.leadingCoeff).coeff i
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↥(integralClosure R A)
p : R[X]
hpm : p.Monic
hpx : eval₂ (algebraMap R A) (↑x) p = 0
⊢ ↑(eval₂ (algebraMap R ↥(integralClosure R A)) x p) = ↑0

Tactic:
by
      rwa [← aeval_def, ← Subalgebra.val_apply, aeval_algHom_apply] at hpx

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

Goal state before:
pp: case h
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
⊢ p.integralNormalization.Monic ∧ eval₂ f (f p.leadingCoeff * x) p.integralNormalization = 0

Tactic:
have : p ≠ 0 := fun h'' => by
      rw [h'', natDegree_zero] at h'
      exact Nat.not_succ_le_zero 0 h'

Goal state after:
case h
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
⊢ p.integralNormalization.Monic ∧ eval₂ f (f p.leadingCoeff * x) p.integralNormalization = 0
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ (Multiset.map (fun ij ↦ ij.1 - ij.2) (g.roots ×ˢ s)).prod =
    (Multiset.map (fun ij ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)).prod

Tactic:
← Multiset.map_swap_product,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ (Multiset.map (fun ij ↦ ij.1 - ij.2) (Multiset.map Prod.swap (s ×ˢ g.roots))).prod =
    (Multiset.map (fun ij ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)).prod
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ p.coeff n *
      ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n - 1) *
        (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ 1) ∈
    Set.range ⇑(algebraMap R Rₘ)

Tactic:
pow_one,

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : ¬n = p.natDegree
this : n + 1 ≤ p.natDegree
⊢ p.coeff n *
      ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n - 1) *
        (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff)) ∈
    Set.range ⇑(algebraMap R Rₘ)
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
I J : Ideal S
inst✝ : Algebra R S
hI : I.IsPrime
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : p.Monic
hpx : eval₂ (algebraMap R S) x p = 0
⊢ comap (algebraMap R S) I < comap (algebraMap R S) J

Tactic:
refine comap_lt_comap_of_root_mem_sdiff hIJ mem (map_monic_ne_zero p_monic) ?_

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
I J : Ideal S
inst✝ : Algebra R S
hI : I.IsPrime
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : p.Monic
hpx : eval₂ (algebraMap R S) x p = 0
⊢ eval₂ (algebraMap R S) x p ∈ I
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
σ : Type u
⊢ Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = Cardinal.lift.{u, u_2} (Module.rank R S)

Tactic:
have := Algebra.isPushout_iff R (MvPolynomial σ R) S (MvPolynomial σ S)
    |>.mp inferInstance |>.lift_rank_eq

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
σ : Type u
this :
  Cardinal.lift.{u_2, max u u_2} (Module.rank (MvPolynomial σ R) (MvPolynomial σ S)) =
    Cardinal.lift.{max u u_2, u_2} (Module.rank R S)
⊢ Module.rank (MvPolynomial σ R) (MvPolynomial σ S) = Cardinal.lift.{u, u_2} (Module.rank R S)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
x : R
⊢ (algebraMap R (Localization.AtPrime I)) x ∈ IsLocalRing.maximalIdeal (Localization.AtPrime I) ↔ x ∈ I

Tactic:
exact IsLocalization.AtPrime.to_map_mem_maximal_iff _ _ _

Goal state after:
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)⁰

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, ?refine_1⟩).2 =
    (algebraMap (R ⧸ I) I.ResidueField) ((Ideal.Quotient.mk I) x, ⟨(Ideal.Quotient.mk I) s, ?refine_1⟩).1

Tactic:
· rwa [mem_nonZeroDivisors_iff_ne_zero, ne_eq, Ideal.Quotient.eq_zero_iff_mem]

Goal state after:
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
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case mp
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) →
    x ∈ range ⇑(algebraMap R K)

pp: case mpr
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∈ range ⇑(algebraMap R K) → ∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯

Tactic:
· contrapose
    intro hrange hlocal
    let denom : Ideal R := (1 : Submodule R K).comap (LinearMap.toSpanSingleton R K x)
    have hdenom : (1 : R) ∉ denom := by simpa [denom] using hrange
    rcases denom.exists_le_maximal (denom.ne_top_iff_one.mpr hdenom) with ⟨max, hmax, hle⟩
    rcases hlocal ⟨max, hmax⟩ with ⟨n, d, hd, rfl⟩
    exact hd (hle ⟨n, by simp [Algebra.smul_def, mul_left_comm, mul_inv_cancel₀ <|
      (map_ne_zero_iff _ <| IsFractionRing.injective R K).mpr fun h ↦ hd (h ▸ max.zero_mem :)]⟩)

Goal state after:
case mpr
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∈ range ⇑(algebraMap R K) → ∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj✝ : Function.Surjective ⇑(toPiLocalization R)
surj : Function.Surjective (⇑(mapPiLocalization (toPiLocalization R).toRingHom ⋯) ∘ ⇑(toPiLocalization R))
⊢ Finite (MaximalSpectrum R)

Tactic:
rw [← AlgHom.coe_toRingHom,
    ← RingHom.coe_comp, mapPiLocalization_naturality, RingHom.coe_comp] at surj

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
surj✝ : Function.Surjective ⇑(toPiLocalization R)
surj : Function.Surjective (⇑(toPiLocalization (PiLocalization R)).toRingHom ∘ ⇑(toPiLocalization R).toRingHom)
⊢ Finite (MaximalSpectrum R)
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI✝ : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
hI : 1 = 0 I
⊢ False

pp: case h
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI✝ : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
hI : 1 = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
⊢ I ≠ { asIdeal := J, isPrime := ⋯ }

pp: case hg
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
⊢ ∀ (y : ↥J.primeCompl), IsUnit ((algebraMap R (Localization I.asIdeal.primeCompl)) ↑y)

Tactic:
· exact one_ne_zero hI

Goal state after:
case h
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI✝ : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
hI : 1 = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
⊢ I ≠ { asIdeal := J, isPrime := ⋯ }

case hg
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
⊢ ∀ (y : ↥J.primeCompl), IsUnit ((algebraMap R (Localization I.asIdeal.primeCompl)) ↑y)
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case hg
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr : (toPiLocalization R) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1
h : ¬I.asIdeal.IsMaximal
hJ : (algebraMap R (Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)) r = 1
hI : (algebraMap R (Localization I.asIdeal.primeCompl)) r = Function.update 0 { asIdeal := J, isPrime := ⋯ } 1 I
⊢ ∀ (y : ↥J.primeCompl), IsUnit ((algebraMap R (Localization I.asIdeal.primeCompl)) ↑y)

Tactic:
· exact fun ⟨s, hs⟩ ↦ IsLocalization.map_units (M := I.1.primeCompl) _ ⟨s, fun h ↦ hs (le h)⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective (⇑(mapPiLocalization (toPiLocalization R).toRingHom) ∘ ⇑(toPiLocalization R))
⊢ Finite (PrimeSpectrum R)

Tactic:
rw [← AlgHom.coe_toRingHom,
    ← RingHom.coe_comp, mapPiLocalization_naturality, RingHom.coe_comp] at surj

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective (⇑(toPiLocalization (PiLocalization R)).toRingHom ∘ ⇑(toPiLocalization R).toRingHom)
⊢ Finite (PrimeSpectrum R)