mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ toENat p.spanRank = ⨅ s, ⨅ (_ : span R s = p), s.encard

Tactic:
rw [spanRank]

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ toENat (⨅ s, #↑↑s) = ⨅ s, ⨅ (_ : span R s = p), s.encard
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ p.spanRank = ↑p.spanFinrank ↔ p.FG

Tactic:
by
  rw [spanFinrank, ← spanRank_finite_iff_fg, eq_comm]
  exact cast_toNat_eq_iff_lt_aleph0

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (span R s).spanRank ≤ #↑s

Tactic:
rw [spanRank]

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ ⨅ s_1, #↑↑s_1 ≤ #↑s
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ∃ s, #↑s = p.spanRank ∧ span R s = p

Tactic:
rw [spanRank]

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ∃ s, #↑s = ⨅ s, #↑↑s ∧ span R s = p
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
⊢ ∃ s, s.encard = ↑p.spanFinrank ∧ span R s = p

Tactic:
refine ⟨s, ⟨?_, hs₂⟩⟩

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
⊢ s.encard = ↑p.spanFinrank
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)
⊢ ∑ i, (M.charmatrix (c i) i).natDegree ≤ ∑ x with c x = x, 1

Tactic:
rw [sum_filter]

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)
⊢ ∑ i, (M.charmatrix (c i) i).natDegree ≤ ∑ a, if c a = a then 1 else 0
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
⊢ ⊥.spanRank = 0

Tactic:
rw [spanRank]

Goal state after:
case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⨅ s, #↑↑s = 0
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
p : Submodule R M
hp : p.FG
⊢ Cardinal.lift.{u, v} (map f p).spanRank ≤ ↑p.spanFinrank

Tactic:
← Cardinal.lift_natCast.{v},

Goal state after:
R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
p : Submodule R M
hp : p.FG
⊢ Cardinal.lift.{u, v} (map f p).spanRank ≤ Cardinal.lift.{v, u} ↑p.spanFinrank
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R →+* T
I : Ideal R
hI : I.FG
⊢ Cardinal.lift.{u, v} (Submodule.spanRank (map f I)) ≤ ↑(Submodule.spanFinrank I)

Tactic:
← Cardinal.lift_natCast.{v},

Goal state after:
R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R →+* T
I : Ideal R
hI : I.FG
⊢ Cardinal.lift.{u, v} (Submodule.spanRank (map f I)) ≤ Cardinal.lift.{v, u} ↑(Submodule.spanFinrank 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
inst✝ : Nontrivial R
hn : Fintype.card n = 2
⊢ M.charpoly = X ^ 2 - C M.trace * X + C M.det

Tactic:
have : Nonempty n := by rw [← Fintype.card_pos_iff]; lia
  ext i
  by_cases hi : i ∈ Finset.range 3
  · fin_cases hi
    · simp [det_eq_sign_charpoly_coeff, hn]
    · simp [trace_eq_neg_charpoly_coeff, hn]
    · simpa [leadingCoeff, charpoly_natDegree_eq_dim, hn, coeff_X] using
        M.charpoly_monic.leadingCoeff
  · rw [Finset.mem_range, not_lt, Nat.succ_le_iff] at hi
    suffices M.charpoly.coeff i = 0 by
      simpa [show i ≠ 2 by lia, show 1 ≠ i by lia, show i ≠ 0 by lia, coeff_X, coeff_C]
    apply coeff_eq_zero_of_natDegree_lt
    simpa [charpoly_natDegree_eq_dim, hn] using hi

Goal state after:
Module: Mathlib.Data.Nat.Choose.Vandermonde

Goal state before:
pp: case a
n x✝ : ℕ
h : x✝ ∈ range n.succ
⊢ n.choose x✝ ^ 2 = n.choose (x✝, n - x✝).1 * n.choose (x✝, n - x✝).2

Tactic:
rw [choose_symm (Finset.mem_range_succ_iff.mp h), sq]

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
hM : IsNilpotent M
h✝ : Nonempty n
this : IsNilpotent (M.charpolyRev.coeff 1)
⊢ IsNilpotent M.trace

Tactic:
simpa using this

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
⊢ ((taylor r) p).natDegree = p.natDegree

Tactic:
refine map_natDegree_eq_natDegree _ ?_
  nontriviality R
  intro n c c0
  simp [taylor_monomial, natDegree_C_mul_of_mul_ne_zero, natDegree_pow_X_add_C, c0]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
p : R[X]
r : R
n : ℕ
hp : ¬p = 0
hn : n = 0
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n

pp: case neg
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
p : R[X]
r : R
n : ℕ
hp : ¬p = 0
hn : ¬n = 0
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n

Tactic:
· simp [hn]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
p : R[X]
r : R
n : ℕ
hp : ¬p = 0
hn : ¬n = 0
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : f = 0
⊢ f.integralNormalization.support = f.support

Tactic:
simp [hf]

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

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

Tactic:
let S : Submonoid R[X] := MonoidHom.mrange C

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
hf : f.Splits
S : Submonoid R[X] := MonoidHom.mrange C
⊢ ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
⊢ (-C 1 * f).Splits

Tactic:
← C_neg

Goal state after:
R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
⊢ (C (-1) * f).Splits
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
⊢ ⊤ ≤ integralClosure R A ↔ Algebra.IsIntegral R A

Tactic:
le_integralClosure_iff_isIntegral,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Algebra.IsIntegral R ↥⊤ ↔ Algebra.IsIntegral R A
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hm : f.Monic
⊢ f.coeff 0 = (-1) ^ f.natDegree * f.roots.prod

Tactic:
by
  simp [hf.coeff_zero_eq_leadingCoeff_mul_prod_roots, hm]

Goal state after:
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
S T : Subalgebra R A
⊢ S ⊔ T ≤ integralClosure R A ↔ S ≤ integralClosure R A ∧ T ≤ integralClosure R A

Tactic:
sup_le_iff

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

Goal state before:
pp: case neg.refine_2
R : Type u_5
S : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬1 = 0
this : Nontrivial Rₘ
b : Rₘ
hb : (algebraMap R Rₘ) ↑⟨p.leadingCoeff, hM⟩ * b = 1
⊢ eval₂ (IsLocalization.map Sₘ f ⋯) ((algebraMap S Sₘ) x) (Polynomial.map (algebraMap R Rₘ) p) = 0

Tactic:
eval₂_map,

Goal state after:
case neg.refine_2
R : Type u_5
S : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : p.leadingCoeff ∈ M
Rₘ : Type u_7
Sₘ : Type u_8
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬1 = 0
this : Nontrivial Rₘ
b : Rₘ
hb : (algebraMap R Rₘ) ↑⟨p.leadingCoeff, hM⟩ * b = 1
⊢ eval₂ ((IsLocalization.map Sₘ f ⋯).comp (algebraMap R Rₘ)) ((algebraMap S Sₘ) x) p = 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case inr.refine_3
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
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
p' : R[X]
hp'₁ : Polynomial.map (algebraMap R Rₘ) p' = p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))
hp'₂ : p'.Monic
⊢ ∃ m, IsIntegral R (m • x)

Tactic:
refine ⟨IsLocalization.commonDenom M p.support p.coeff, p', hp'₂, ?_⟩

Goal state after:
case inr.refine_3
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
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
p' : R[X]
hp'₁ : Polynomial.map (algebraMap R Rₘ) p' = p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))
hp'₂ : p'.Monic
⊢ eval₂ (algebraMap R S) (commonDenom M p.support p.coeff • x) p' = 0
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ₘ
r : S
hr : IsIntegral R r
inst✝ : Away r Sₘ
x : S
a✝ : Nontrivial S
p : R[X]
hpm : p.Monic
m : ℕ
hm : r ^ m * eval₂ (algebraMap R S) x p = 0
⊢ ∃ n, IsIntegral R (r ^ n * x)

Tactic:
have := isIntegral_trans (R := R) _ (isIntegral_leadingCoeff_smul (R := integralClosure R S)
    (C ⟨r, hr⟩ ^ m * p.map (algebraMap _ _)) x (by simpa [← aeval_def] using hm))

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ₘ
r : S
hr : IsIntegral R r
inst✝ : Away r Sₘ
x : S
a✝ : Nontrivial S
p : R[X]
hpm : p.Monic
m : ℕ
hm : r ^ m * eval₂ (algebraMap R S) x p = 0
this : IsIntegral R ((C ⟨r, hr⟩ ^ m * Polynomial.map (algebraMap R ↥(integralClosure R S)) p).leadingCoeff • x)
⊢ ∃ n, IsIntegral R (r ^ n * x)
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
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : FaithfullyFlat R M
⊢ Subsingleton (M ⊗[R] N) ↔ Subsingleton N

Tactic:
exact subsingleton_tensorProduct_iff_right R M

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 : ¬IsNilpotent y
h : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (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.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑(LinearMap.lTensor M f) ⇑0 ↔ Function.Surjective ⇑f

Tactic:
← LinearMap.exact_zero_iff_surjective Unit

Goal state after:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑(LinearMap.lTensor M f) ⇑0 ↔ Function.Exact ⇑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
⊢ FaithfullyFlat R M ↔
    ∀ {N1 : Type (max u v)} [inst : AddCommGroup N1] [inst_1 : Module R N1] {N2 : Type (max u v)}
      [inst_2 : AddCommGroup N2] [inst_3 : Module R N2] {N3 : Type (max u v)} [inst_4 : AddCommGroup N3]
      [inst_5 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
      Function.Exact ⇑l12 ⇑l23 ↔ Function.Exact ⇑(LinearMap.lTensor M l12) ⇑(LinearMap.lTensor M l23)

Tactic:
simp only [iff_exact_iff_rTensor_exact, LinearMap.rTensor_exact_iff_lTensor_exact]

Goal state after:
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
h✝ : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
h : LinearMap.lTensor M f = 0
⊢ LinearMap.rTensor M f = 0

Tactic:
ext n m; exact (TensorProduct.comm R N' M).injective <|
    (by simpa using congr($h (m ⊗ₜ n)))

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⁰
mk_yz_eq : mk' L y' z' = mk' L y ⟨(algebraMap R S) z, hz0'⟩
hy : (algebraMap S L) (a * y) ∈ Submodule.span K (⇑(algebraMap S L) '' b)
⊢ (algebraMap K L) ((algebraMap R K) z)⁻¹ * ((algebraMap S L) a * (algebraMap S L) y) ∈
    ↑(Submodule.span K (⇑(algebraMap S L) '' b))

Tactic:
←
      Algebra.smul_def,

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'⟩
hy : (algebraMap S L) (a * y) ∈ Submodule.span K (⇑(algebraMap S L) '' b)
⊢ ((algebraMap R K) z)⁻¹ • ((algebraMap S L) a * (algebraMap S L) y) ∈ ↑(Submodule.span K (⇑(algebraMap S L) '' b))
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ map (Quotient.mk I) (RingHom.ker (algebraMap R I.ResidueField)) = ⊥

Tactic:
rw [Ideal.ker_algebraMap_residueField, map_quotient_self]

Goal state after:
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✝³ : IsDomain B
inst✝² : Flat A B
inst✝¹ : Algebra.IsIntegral A B
inst✝ : FaithfulSMul A B
P✝ : PrimeSpectrum A
P : Ideal B
hP₁ : P.IsPrime
hP₂ : Ideal.comap (algebraMap A B) P = P✝.asIdeal
⊢ ∃ a, PrimeSpectrum.comap (algebraMap A B) a = P✝

Tactic:
exact ⟨⟨P, hP₁⟩, PrimeSpectrum.ext_iff.mpr hP₂⟩

Goal state after:
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✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
x : A
hx : (Quotient.mk (map (algebraMap A B) I)) ((algebraMap A B) x) = 0
⊢ (↑A ↑↑(quotIdealMapEquivTensorQuot B I).symm ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1) ((Quotient.mk I) x) = 0

Tactic:
simp [← Algebra.algebraMap_eq_smul_one, hx]

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

Goal state before:
pp: 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
inst✝⁵ : Algebra.EssFiniteType R A
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal A
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
⊢ Algebra.EssFiniteType p.ResidueField q.ResidueField

Tactic:
have : Algebra.EssFiniteType R q.ResidueField := .comp _ A _
  refine .of_comp R _ _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : FiniteRingKrullDim R
⊢ Nontrivial R

Tactic:
← PrimeSpectrum.nonempty_iff_nontrivial

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : FiniteRingKrullDim R
⊢ Nonempty (PrimeSpectrum R)
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)
⊢ ∃ I, ∃ (x : I.IsMaximal), { asIdeal := I, isPrime := ⋯ } ∉ Set.range (sigmaToPi R)

Tactic:
classical
  let J : Ideal (Π i, R i) := -- `J := Π₀ i, R i` is an ideal in `Π i, R i`
  { __ := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom
    smul_mem' := by
      rintro r _ ⟨x, rfl⟩
      refine ⟨.mk x.support fun i ↦ r i * x i, funext fun i ↦ show dite _ _ _ = _ from ?_⟩
      simp_rw +instances [DFinsupp.coeFnAddMonoidHom]
      refine dite_eq_left_iff.mpr fun h ↦ ?_
      rw [DFinsupp.notMem_support_iff.mp h, mul_zero] }
  have ⟨I, max, le⟩ := J.exists_le_maximal <| (Ideal.ne_top_iff_one _).mpr <| by
    -- take a maximal ideal I containing J
    rintro ⟨x, hx⟩
    have ⟨i, hi⟩ := x.support.exists_notMem
    simpa [DFinsupp.coeFnAddMonoidHom, DFinsupp.notMem_support_iff.mp hi] using congr_fun hx i
  refine ⟨I, max, fun ⟨⟨i, p⟩, eq⟩ ↦ ?_⟩
  -- then I is not in the range of `sigmaToPi`
  have : ⇑(DFinsupp.single i 1) ∉ (sigmaToPi R ⟨i, p⟩).asIdeal := by
    simpa using p.1.ne_top_iff_one.mp p.2.ne_top
  rw [eq] at this
  exact this (le ⟨.single i 1, rfl⟩)

Goal state after:
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
U : Set X
hUc : IsCompact U
hUo : IsOpen U
⊢ ∃ s, U = ⋃₀ (Subtype.val '' ↑s)

Tactic:
have hb' : b = range (fun i ↦ i : b → Set X) := by simp
  rw [hb'] at hb
  choose s hs hU using eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open _ hb U hUc hUo
  have : Finite s := hs
  let _ : Fintype s := Fintype.ofFinite _
  use s.toFinset
  simp [hU]

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∪ (frontier s)ᶜ = (frontier s)ᶜ ↔ IsOpen[inst✝] s

Tactic:
union_eq_right,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ s ⊆ (frontier s)ᶜ ↔ IsOpen[inst✝] s
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ t ∈ ↑S, IsClosed[inst✝¹] t
hSi : ∀ t ∈ ↑S, IsIrreducible t
hSU : Set.univ = ⋃₀ ↑S
t : Set α
htS : t ∈ S
ht : s ⊆ t
⊢ s ∈ ↑S

Tactic:
rwa [ht.antisymm (hs.2 (hSi _ htS) ht)]

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsOpen[inst✝] s
⊢ IsQuasiSeparated s ↔ IsQuasiSeparated univ

Tactic:
convert! (hs.isOpenEmbedding_subtypeVal.isQuasiSeparated_iff (s := Set.univ)).symm

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsOpen[inst✝] s
⊢ s = Subtype.val '' univ
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
aux : ∀ (U : Set α), IsCompact U ∧ IsOpen[inst✝] U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
s : Set ι
hs : s.Finite
hUopen : IsOpen[inst✝] (⋃ i ∈ s, b i)
hUcomp : IsCompact (⋃ i ∈ s, b i)
t : Set ι
ht : t.Finite
hVopen : IsOpen[inst✝] (⋃ i ∈ t, b i)
hVcomp : IsCompact (⋃ i ∈ t, b i)
⊢ IsCompact (⋃ i₁ ∈ s, ⋃ j₁ ∈ t, b i₁ ∩ b j₁)

Tactic:
exact hs.isCompact_biUnion fun i hi ↦ ht.isCompact_biUnion fun j hj ↦ isCompact_inter ..

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : a ∉ s
h : ↑(s.sup f) = s.sup fun i ↦ ↑(f i)
⊢ ↑(f a) ∪ ↑(s.sup f) = ↑(f a) ⊔ s.sup fun i ↦ ↑(f i)

Tactic:
sup_eq_union

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : a ∉ s
h : ↑(s.sup f) = s.sup fun i ↦ ↑(f i)
⊢ ↑(f a) ∪ ↑(s.sup f) = ↑(f a) ∪ s.sup fun i ↦ ↑(f i)
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst✝¹] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst✝²] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst✝¹] (T ∩ range f))
hxT : x ∈ T
⊢ ∃ x, IsGenericPoint x (f ⁻¹' T)

Tactic:
obtain ⟨y, rfl⟩ : x ∈ range f := by
      rw [hx.mem_open_set_iff hf.isOpen_range]
      refine Nonempty.mono ?_ hS''.1
      simpa using subset_closure

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed[inst✝¹] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst✝²] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure[inst✝¹] (T ∩ range f))
hxT : f y ∈ T
⊢ ∃ x, IsGenericPoint x (f ⁻¹' T)