mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
S : Type uS
M : Type uM
N : Type uN
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : AddCommGroup N
inst✝¹⁵ : Module R M
inst✝¹⁴ : Module R N
inst✝¹³ : Algebra R S
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
p : Submonoid R
inst✝¹⁰ : IsLocalization p S
f : M →ₗ[R] N
inst✝⁹ : IsLocalizedModule p f
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
hpT : Algebra.algebraMapSubmonoid T p ≤ T⁰
inst✝⁴ : StrongRankCondition (S ⊗[R] T)
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

Tactic:
rw [← lift_inj.{_, max uS uT uN}, lift_lift, lift_lift]
  let ST := S ⊗[R] T
  conv_rhs => rw [← lift_lift.{uN, max uS uT uP}, ← IsLocalizedModule.lift_rank_eq p f hp,
    ← IsLocalization.rank_eq S p hp, lift_lift, ← lift_lift.{max uS uT, max uM uP},
    ← rank_baseChange (R := ST), ← lift_id'.{max uS uT, max uS uT uN} (Module.rank ..),
    lift_lift, ← lift_lift.{max uS uT uP, uM}]
  let _ : Algebra T ST := Algebra.TensorProduct.rightAlgebra
  set pT := Algebra.algebraMapSubmonoid T p
  rw [← lift_lift.{max uS uT, max uM uN}, ← lift_umax.{uP},
    ← IsLocalizedModule.lift_rank_eq pT (mk T ST P 1) hpT,
    ← IsLocalization.rank_eq ST pT hpT, lift_id'.{uP, max uS uT},
    ← lift_id'.{max uS uT, max uS uT uP} (Module.rank ..), lift_lift,
    ← lift_lift.{max uS uT uN, uM}, lift_inj]
  exact LinearEquiv.lift_rank_eq <| AlgebraTensorModule.congr (.refl ST ST) bc.equiv.symm ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange .. ≪≫ₗ (AlgebraTensorModule.cancelBaseChange ..).symm ≪≫ₗ
    AlgebraTensorModule.congr (.refl ..) ((isLocalizedModule_iff_isBaseChange p S f).mp ‹_›).equiv

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

Goal state before:
pp: case of_succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
hn' : n < (listTransvecCol M).length
⊢ (((listTransvecCol M)[n] :: List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i

Tactic:
simpa [listTransvecCol, Matrix.mul_assoc]

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

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : (Matrix n n α)ˣ
this : Invertible ↑A := A.invertible
⊢ ↑A⁻¹ = (↑A)⁻¹

Tactic:
rw [← invOf_eq_nonsing_inv, invOf_units]

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

Goal state before:
pp: m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (M * N * M⁻¹).det = N.det

Tactic:
← h.unit_spec,

Goal state after:
m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (↑h.unit * N * (↑h.unit)⁻¹).det = N.det
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (M⁻¹ * N * M).det = N.det

Tactic:
← h.unit_spec,

Goal state after:
m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ ((↑h.unit)⁻¹ * N * ↑h.unit).det = N.det
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (M * N * M⁻¹).trace = N.trace

Tactic:
← h.unit_spec,

Goal state after:
m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (↑h.unit * N * (↑h.unit)⁻¹).trace = N.trace
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (M⁻¹ * N * M).trace = N.trace

Tactic:
← h.unit_spec,

Goal state after:
m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ ((↑h.unit)⁻¹ * N * ↑h.unit).trace = N.trace
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)
H :
  ∀ (L₁ L₂ : List (TransvectionStruct n 𝕜)) (E : Matrix n n 𝕜),
    P E → P ((List.map toMatrix L₁).prod * E * (List.map toMatrix L₂).prod)
⊢ P M

Tactic:
rw [h]
    apply H L L'
    exact PD

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

Goal state before:
pp: case nil
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 𝕜)
E : Matrix n n 𝕜
PE : P E
⊢ P (E * (List.map toMatrix L₂).prod)

Tactic:
induction L₂ generalizing E with

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:
by
  rw [Matrix.charpoly_mul_comm, ← mul_assoc]
  simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
i k : ℕ
hk : (p + C r) ^ k = 0
⊢ eval 0 p = 0

Tactic:
coeff_zero_eq_aeval_zero

Goal state after:
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : (aeval 0) p = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
i k : ℕ
hk : (p + C r) ^ k = 0
⊢ eval 0 p = 0
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Ring R
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent (-y)
⊢ IsNilpotent (x - y)

Tactic:
sub_eq_add_neg

Goal state after:
R : Type u_1
x y : R
inst✝ : Ring R
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent (-y)
⊢ IsNilpotent (x + -y)
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
hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : (fromEnd R b) x = (fromEnd R b) y
m : M
⊢ m ∈ (Fintype.linearCombination R b).range

Tactic:
rw [(Fintype.range_linearCombination R b).trans hb]

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
hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : (fromEnd R b) x = (fromEnd R b) y
m : M
⊢ m ∈ ⊤
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 : ℕ
h : Fintype.card n - 1 ≤ k
⊢ ↑(Fintype.card n - 1) ≤ ↑k

Tactic:
rw [Nat.cast_le]

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ Fintype.card n - 1 ≤ k
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case mp
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
hr : IsIntegral R r
⊢ ∃ s, s.Finite ∧ IsIntegral (↥(Subring.closure s)) r

Tactic:
rcases hr with ⟨p, hmp, hpr⟩

Goal state after:
case mp
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
p : R[X]
hmp : p.Monic
hpr : eval₂ (algebraMap R B) r p = 0
⊢ ∃ s, s.Finite ∧ IsIntegral (↥(Subring.closure s)) r
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: 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
⊢ (matPolyEquiv ((↑(expand K k)).mapMatrix (M ^ k).charmatrix)).coeff m i j =
    ((X ^ k).coeff m - if m = 0 then M ^ k else 0) i j

Tactic:
matPolyEquiv_coeff_apply,

Goal state after:
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
⊢ ((↑(expand K k)).mapMatrix (M ^ k).charmatrix i j).coeff m = ((X ^ k).coeff m - if m = 0 then M ^ k else 0) i j
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
⊢ matPolyEquiv ((↑(expand K k)).mapMatrix (M ^ k).charmatrix) = X ^ k - C (M ^ k)

Tactic:
ext m i j
  rw [coeff_sub, coeff_C, matPolyEquiv_coeff_apply, RingHom.mapMatrix_apply, Matrix.map_apply,
    AlgHom.coe_toRingHom, coeff_X_pow]
  by_cases hij : i = j
  · rw [hij, charmatrix_apply_eq, map_sub, expand_C, expand_X, coeff_sub, coeff_X_pow, coeff_C]
    split_ifs with mp m0 <;> simp
  · rw [charmatrix_apply_ne _ _ _ hij, map_neg, expand_C, coeff_neg, coeff_C]
    split_ifs with m0 mp <;> simp_all

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
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:
simp [charpolyRev, smul_eq_diagonal_mul]

Goal state after:
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 - (diagonal fun x ↦ X) * A.map ⇑C).det) =
    (-1) ^ Fintype.card n * C A.det⁻¹ʳ * (1 - (diagonal fun x ↦ X) * A.map ⇑C).det
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ ↑((k + 1) * k ! * (n + k + 1).choose (k + 1)) * f.coeff (n + k + 1) =
    ↑(k ! * (n + k + 1).choose (n + 1) * (n + 1)) * f.coeff (n + k + 1)

Tactic:
congr 2

Goal state after:
case succ.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ (k + 1) * k ! * (n + k + 1).choose (k + 1) = k ! * (n + k + 1).choose (n + 1) * (n + 1)
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ (monomial (i - (k + l))) ↑((i - l).choose k * i.choose l) =
    (monomial (i - (k + l))) ↑((k + l).choose k * i.choose (k + l))

Tactic:
congr 2

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ (((compHom (D k)).comp Φ) f) g = ((∑ x ∈ antidiagonal k, (compHom.comp ((compHom Φ) (D x.1))).flip (D x.2)) f) g

Tactic:
congr 2

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ (compHom (D k)).comp Φ = ∑ x ∈ antidiagonal k, (compHom.comp ((compHom Φ) (D x.1))).flip (D x.2)
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 : k ≤ Fintype.card n
a✝ : Nontrivial R
hnd : M.charpoly.natDegree = Fintype.card n
hrev : M.charpoly.coeff (Fintype.card n - k) = M.charpoly.reverse.coeff k
⊢ (1 + -(X • M.map ⇑C)).det = (1 + X • (-M).map ⇑C).det

Tactic:
congr 2

Goal state after:
case e_a
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : k ≤ Fintype.card n
a✝ : Nontrivial R
hnd : M.charpoly.natDegree = Fintype.card n
hrev : M.charpoly.coeff (Fintype.card n - k) = M.charpoly.reverse.coeff k
⊢ -(X • M.map ⇑C) = X • (-M).map ⇑C
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p

Tactic:
obtain rfl | hp := eq_or_ne p 0

Goal state after:
case inr.inl
R : Type u_1
inst✝ : CommRing R
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
⊢ rootMultiplicity (r * a) (scaleRoots 0 r) = rootMultiplicity a 0

case inr.inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
i : ℕ
| p.coeff i = 0

Tactic:
rw [← coeff_toSubring p T hp]

Goal state after:
R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
i : ℕ
| ↑((p.toSubring T hp).coeff i) = 0
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hR : IsField R
x : S
hx : x ≠ 0
⊢ ∃ b, x * b = 1

Tactic:
let := hR.toField
    obtain ⟨y, rfl⟩ := (Algebra.IsIntegral.isIntegral (R := R) x).isUnit hx
    exact ⟨y.inv, y.val_inv⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra.IsIntegral R A
inst✝¹ : IsDomain A
inst✝ : Nontrivial R
I : Ideal A
⊢ ¬I = ⊥ → ¬comap (algebraMap R A) I = ⊥

Tactic:
exact IsIntegral.comap_ne_bot R

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

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : y ∈ nonZeroDivisors R
h : IsAlgebraic R (y • z)
p : R[X]
hp : p ≠ 0
eval0 : (aeval (y • z)) p = 0
⊢ (aeval z) (p.comp (C y * X)) = 0

Tactic:
simpa [aeval_comp, Algebra.smul_def] using eval0

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : PrimeSpectrum R
⊢ ((primeSpectrumProd R S).symm (Sum.inl x)).asIdeal = x.asIdeal.prod ⊤

Tactic:
by
  cases x
  rfl

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : PrimeSpectrum S
⊢ ((primeSpectrumProd R S).symm (Sum.inr x)).asIdeal = ⊤.prod x.asIdeal

Tactic:
by
  cases x
  rfl

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : M = ⊤
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ ⊤

Tactic:
exact ⟨0, le_top⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
⊢ (algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))

Tactic:
have mk_yz_eq : IsLocalization.mk' L y' z' = IsLocalization.mk' L y ⟨_, hz0'⟩ := by
    rw [Algebra.smul_def, mul_comm _ y, mul_comm _ y'] at yz_eq
    exact IsLocalization.mk'_eq_of_eq (by rw [mul_comm _ y, mul_comm _ y', yz_eq])

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩
⊢ (algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case h
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
k : Type u := ⋯
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
m : Ideal (k ⊗[R] S)
hm : m.IsMaximal
⊢ (comap (algebraMap R S) (comap Algebra.TensorProduct.includeRight.toRingHom { asIdeal := m, isPrime := ⋯ })).asIdeal =
    p.asIdeal

Tactic:
← PrimeSpectrum.comap_comp_apply,

Goal state after:
case h
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
m : Ideal (k ⊗[R] S)
hm : m.IsMaximal
⊢ (comap (Algebra.TensorProduct.includeRight.comp (algebraMap R S)) { asIdeal := m, isPrime := ⋯ }).asIdeal = p.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case refine_2
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
q : PrimeSpectrum S
k : Type u := (comap (algebraMap R S) q).asIdeal.ResidueField
⊢ Nontrivial ((comap (algebraMap R S) q).asIdeal.ResidueField ⊗[R] S)

Tactic:
let f : k ⊗[R] S →ₐ[R] q.asIdeal.ResidueField :=
      Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ _ _ (Algebra.ofId _ _) rfl)
        (IsScalarTower.toAlgHom _ _ _) (fun _ _ ↦ Commute.all ..)

Goal state after:
case refine_2
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
q : PrimeSpectrum S
k : Type u := (comap (algebraMap R S) q).asIdeal.ResidueField
f : k ⊗[R] S →ₐ[R] q.asIdeal.ResidueField :=
  Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ (comap (algebraMap R S) q).asIdeal q.asIdeal (Algebra.ofId R S) ⋯)
    (IsScalarTower.toAlgHom R S q.asIdeal.ResidueField) ⋯
⊢ Nontrivial ((comap (algebraMap R S) q).asIdeal.ResidueField ⊗[R] S)
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ I.minimalPrimes = comap (Quotient.mk I) '' minimalPrimes (R ⧸ I)

Tactic:
rw [minimalPrimes, ← Ideal.comap_minimalPrimes_eq_of_surjective Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker]

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ IsCompact U ∧ IsOpen[inst✝] U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, ↑(b i)

Tactic:
apply isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis fun i : ι => (b i).1

Goal state after:
case hb
α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ IsTopologicalBasis (range fun i ↦ (b i).carrier)

case hb'
α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ ∀ (i : ι), IsCompact (b i).carrier
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ IsClosedEmbedding f ↔ ∀ (i : ι), IsClosedEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
simp_rw [isClosedEmbedding_iff, forall_and]
  apply and_congr
  · exact hU.isEmbedding_iff_restrictPreimage h
  · simp_rw [range_restrictPreimage]
    exact hU.isClosed_iff_coe_preimage

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α✝ : Type u_1
inst✝² : TopologicalSpace α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
h : ∀ t ∈ s, IsOpen[inst✝¹] t
⊢ s.Nonempty → IsCompact (⋂₀ s)

Tactic:
induction s, hf using Set.Finite.induction_on with

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
this : closure {x} ⊆ S
⊢ True ∧ S ⊆ closure {x} ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z

Tactic:
true_and,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
this : closure {x} ⊆ S
⊢ S ⊆ closure {x} ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
Module: Mathlib.RingTheory.RingHom.FaithfullyFlat

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
p : PrimeSpectrum R
this : (↑(RingEquiv.ofBijective f hf).symm).comp f = id R
⊢ PrimeSpectrum.comap f (PrimeSpectrum.comap (↑(RingEquiv.ofBijective f hf).symm) p) = p

Tactic:
← PrimeSpectrum.comap_comp_apply,

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
p : PrimeSpectrum R
this : (↑(RingEquiv.ofBijective f hf).symm).comp f = id R
⊢ PrimeSpectrum.comap ((↑(RingEquiv.ofBijective f hf).symm).comp f) p = p