mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
p : PrimeSpectrum R
tfae_1_to_2 : IsOpen {p} → IsClopen {p}
tfae_2_to_3 : IsClopen {p} → IsClosed {p} ∧ StableUnderGeneralization {p}
h₁ : IsMax p
h₂ : StableUnderGeneralization {p}
i✝ : PrimeSpectrum R
a✝ : IsMin i✝
⊢ i✝ ≤ p → i✝ = p

Tactic:
rw [stableUnderGeneralization_singleton, ← isMin_iff] at h₂

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
p : PrimeSpectrum R
tfae_1_to_2 : IsOpen {p} → IsClopen {p}
tfae_2_to_3 : IsClopen {p} → IsClosed {p} ∧ StableUnderGeneralization {p}
h₁ : IsMax p
h₂ : IsMin p
i✝ : PrimeSpectrum R
a✝ : IsMin i✝
⊢ i✝ ≤ p → i✝ = p
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
⊢ nilradical R = IsLocalRing.maximalIdeal R ↔ IsLocalRing.maximalIdeal R ≤ nilradical R

Tactic:
le_antisymm_iff,

Goal state after:
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
⊢ nilradical R ≤ IsLocalRing.maximalIdeal R ∧ IsLocalRing.maximalIdeal R ≤ nilradical R ↔
    IsLocalRing.maximalIdeal R ≤ nilradical R
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
p q : Submodule B M
h : p ⋖ q
⊢ length A ↥q = length A ↥p + length (ResidueField A) (ResidueField B)

Tactic:
let f : p →ₗ[B] q := inclusion h.le

Goal state after:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
p q : Submodule B M
h : p ⋖ q
f : ↥p →ₗ[B] ↥q := inclusion ⋯
⊢ length A ↥q = length A ↥p + length (ResidueField A) (ResidueField B)
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : IsDedekindDomain S
h₁ : map f p ≠ ⊤
h₂ : map f p ≠ ⊥
h : map f p ≤ map f p ^ (1 + 1)
this✝ : map f p ^ 1 = map f p ^ 2
this : 1 = 2
⊢ False

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h2
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
⊢ Submodule.map (Submodule.subtype (Q.comp P).toExtension.ker) ((Q.comp P).toExtension.Ring ∙ z) ≤
    Submodule.map (Submodule.subtype (Q.comp P).toExtension.ker)
      (Submodule.comap Extension.Cotangent.mk
        (Submodule.restrictScalars (Q.comp P).Ring
          (Submodule.span T ↑(Extension.Cotangent.map (Q.toComp P).toExtensionHom).range)))

Tactic:
Submodule.map_subtype_span_singleton,

Goal state after:
case h2
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
⊢ (Q.comp P).toExtension.Ring ∙ ↑z ≤
    Submodule.map (Submodule.subtype (Q.comp P).toExtension.ker)
      (Submodule.comap Extension.Cotangent.mk
        (Submodule.restrictScalars (Q.comp P).Ring
          (Submodule.span T ↑(Extension.Cotangent.map (Q.toComp P).toExtensionHom).range)))
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝¹ : Module.Finite K A
this✝ : IsArtinianRing A
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A :=
  let __spread.0 := ofId K (A ⧸ IsLocalRing.maximalIdeal A);
  let __spread.1 := Equiv.ofBijective ⇑(algebraMap K (A ⧸ IsLocalRing.maximalIdeal A)) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  (TensorProduct.congr AlgEquiv.refl e.symm).trans (TensorProduct.rid K A A)
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := e'.toLinearMap ∘ₗ sec K A (A ⧸ IsLocalRing.maximalIdeal A)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A
hf₃ : IsIdempotentElem (1 - f 1)
n : ℕ
hn : IsLocalRing.maximalIdeal A ^ n = 0
this : (1 - f 1) ^ n = 0
⊢ f 1 = 1

Tactic:
rw [eq_comm, ← sub_eq_zero, ← hf₃.pow_succ_eq n, pow_succ, this, zero_mul]

Goal state after:
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: A : Type u_2
inst✝⁵ : CommRing A
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : EssFiniteType A B
inst✝¹ : FormallyUnramified A B
p : Ideal A
inst✝ : p.IsMaximal
this : Field (A ⧸ p) := Ideal.Quotient.field p
⊢ (Ideal.map (algebraMap A B) p).IsRadical

Tactic:
rw [Ideal.isRadical_iff_quotient_reduced]

Goal state after:
A : Type u_2
inst✝⁵ : CommRing A
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : EssFiniteType A B
inst✝¹ : FormallyUnramified A B
p : Ideal A
inst✝ : p.IsMaximal
this : Field (A ⧸ p) := Ideal.Quotient.field p
⊢ IsReduced (B ⧸ Ideal.map (algebraMap A B) p)
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this : ExpChar (L ⊗[K] L) (ringExpChar K)
⊢ 1 ⊗ₜ[K] (x ^ ringExpChar K ^ n) - (x ^ ringExpChar K ^ n) ⊗ₜ[K] 1 = 0

Tactic:
obtain ⟨r, hr⟩ := hn

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
this : ExpChar (L ⊗[K] L) (ringExpChar K)
r : K
hr : (algebraMap K L) r = x ^ ringExpChar K ^ n
⊢ 1 ⊗ₜ[K] (x ^ ringExpChar K ^ n) - (x ^ ringExpChar K ^ n) ⊗ₜ[K] 1 = 0
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case tmul.tmul
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
h₂ : ↑b • Cotangent.mk d = 0
⊢ a • (c • 1) ⊗ₜ[S] (↑b • Cotangent.mk d) = 0

Tactic:
h₂,

Goal state after:
case tmul.tmul
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
h₂ : ↑b • Cotangent.mk d = 0
⊢ a • (c • 1) ⊗ₜ[S] 0 = 0
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
J : Ideal A
hD : IsCoprime I J
this : ∀ (n : ℕ), Disjoint (torsionBySet A M ↑(I ^ n)) (torsionBySet A M ↑J)
x : M
⊢ x = 0 → (∃ n, ∀ a ∈ I ^ n, a • x = 0) ∧ ∀ a ∈ J, a • x = 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case pos
s : Set ℝ
hn : s.Nonempty
hb : BddBelow s
⊢ sSup (-s) = -sInf s

pp: case neg
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
⊢ sSup (-s) = -sInf s

Tactic:
· rw [csSup_neg hn hb]

Goal state after:
case neg
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
⊢ sSup (-s) = -sInf s
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
⊢ (x * y⁻¹).toNNReal = x.toNNReal * y.toNNReal⁻¹

Tactic:
← Real.toNNReal_inv,

Goal state after:
x y : ℝ
hx : 0 ≤ x
⊢ (x * y⁻¹).toNNReal = x.toNNReal * y⁻¹.toNNReal
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inl
motive : ℝ → Prop
nonneg : ∀ (x : ℝ≥0), motive ↑x
nonpos : ∀ (x : ℝ≥0), motive ↑x → motive (-↑x)
r : ℝ≥0
⊢ motive ↑r

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inr
motive : ℝ → Prop
nonneg : ∀ (x : ℝ≥0), motive ↑x
nonpos : ∀ (x : ℝ≥0), motive ↑x → motive (-↑x)
r : ℝ≥0
⊢ motive (-↑r)

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
h : ∀ (i : HeightOneSpectrum R), ¬i.maxPowDividing I = ⊤ → x ∈ i.maxPowDividing I
i : HeightOneSpectrum R
h✝ : i.maxPowDividing I = ⊤
⊢ x ∈ i.maxPowDividing I

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
h : ∀ (i : HeightOneSpectrum R), ¬i.maxPowDividing I = ⊤ → x ∈ i.maxPowDividing I
i : HeightOneSpectrum R
h✝ : ¬i.maxPowDividing I = ⊤
⊢ x ∈ i.maxPowDividing I

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inl
motive : ℝ → Prop
zero : motive 0
pos : ∀ (x : ℝ≥0), 0 < x → motive ↑x
neg : ∀ (x : ℝ≥0), 0 < x → motive ↑x → motive (-↑x)
⊢ motive 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inr.inl
motive : ℝ → Prop
zero : motive 0
pos : ∀ (x : ℝ≥0), 0 < x → motive ↑x
neg : ∀ (x : ℝ≥0), 0 < x → motive ↑x → motive (-↑x)
r : ℝ≥0
hr : 0 < r
⊢ motive ↑r

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inr.inr
motive : ℝ → Prop
zero : motive 0
pos : ∀ (x : ℝ≥0), 0 < x → motive ↑x
neg : ∀ (x : ℝ≥0), 0 < x → motive ↑x → motive (-↑x)
r : ℝ≥0
hr : 0 < r
⊢ motive (-↑r)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case neg
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
a : A
ha : a ∈ A⁰
ha0 : span {a} ≠ ⊥
this✝ : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
this : ⨅ i, i.maxPowDividing (span {a}) = ⨅ i ∈ S, i.maxPowDividing (span {a})
hPairwise : (↑S).Pairwise fun i j ↦ i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤
P : HeightOneSpectrum A
x : M
hxmem : x ∈ ⨆ (_ : P ∈ S), torsionBySet A M ↑(P.maxPowDividing (span {a}))
hPS : P ∉ S
⊢ x ∈ primaryComponent M P.asIdeal

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: ⊢ ⋂ n, Ici ↑n = {∞}

Tactic:
simp only [← compl_Iio, ← compl_iUnion, iUnion_Iio_coe_nat, compl_compl]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : α
hx : x ∈ s.ordConnectedSection
hy : y ∈ s.ordConnectedSection
h : [[x, y]] ⊆ s
⊢ x = y

Tactic:
by
  rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
  exact
    ordConnectedProj_eq.2
      (mem_ordConnectedComponent_trans
        (mem_ordConnectedComponent_trans (ordConnectedProj_mem_ordConnectedComponent _ _) h)
        (mem_ordConnectedComponent_ordConnectedProj _ _))

Goal state after:
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case mpr
a b : ℝ≥0∞
⊢ a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0 → a * b < ∞

Tactic:
· rintro (⟨ha, hb⟩ | rfl | rfl) <;> [exact mul_lt_top ha hb; simp; simp]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
⊢ spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * (↑J * (spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J')) =
    spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')

Tactic:
mul_comm (J : FractionalIdeal R⁰ K),

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
⊢ spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * (spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J' * ↑J) =
    spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case neg
x : EReal
h : x ≠ ⊥
h' : ¬x = ⊤
⊢ ↑x.toReal ≤ x

Tactic:
simp only [le_refl, coe_toReal h' h]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ≥0∞
⊢ ↑x = 0 ↔ x = 0

Tactic:
← coe_ennreal_eq_coe_ennreal_iff,

Goal state after:
x : ℝ≥0∞
⊢ ↑x = 0 ↔ ↑x = ↑0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ≥0∞
⊢ ↑x = 1 ↔ x = 1

Tactic:
← coe_ennreal_eq_coe_ennreal_iff,

Goal state after:
x : ℝ≥0∞
⊢ ↑x = 1 ↔ ↑x = ↑1
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
⊢ x.toENNReal = 0 ↔ x ≤ 0

Tactic:
induction x <;> simp [toENNReal]

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inl
b : ℝ≥0∞
ha₀ : 0 = 0 → b = 0
ha : 0 = ∞ → b = 0
⊢ 0⁻¹ * (0 * b) = b

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inl
b : ℝ≥0∞
ha₀✝ : ∞ = 0 → b = 0
ha : ∞ = ∞ → b = 0
ha₀ : ∞ ≠ 0
⊢ ∞⁻¹ * (∞ * b) = b

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inl
b : ℝ≥0∞
ha₀ : 0 = 0 → b = 0
ha : 0 = ∞ → b = 0
⊢ 0 * (0⁻¹ * b) = b

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inl
b : ℝ≥0∞
ha₀✝ : ∞ = 0 → b = 0
ha : ∞ = ∞ → b = 0
ha₀ : ∞ ≠ 0
⊢ ∞ * (∞⁻¹ * b) = b

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inl
a : ℝ≥0∞
hb₀ : 0 = 0 → a = 0
hb : 0 = ∞ → a = 0
⊢ a * 0 * 0⁻¹ = a

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inl
a : ℝ≥0∞
hb₀✝ : ∞ = 0 → a = 0
hb : ∞ = ∞ → a = 0
hb₀ : ∞ ≠ 0
⊢ a * ∞ * ∞⁻¹ = a

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inl
a : ℝ≥0∞
hb₀ : 0 = 0 → a = 0
hb : 0 = ∞ → a = 0
⊢ a * 0⁻¹ * 0 = a

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inl
a : ℝ≥0∞
hb₀✝ : ∞ = 0 → a = 0
hb : ∞ = ∞ → a = 0
hb₀ : ∞ ≠ 0
⊢ a * ∞⁻¹ * ∞ = a

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot.bot
hx hy : 0 ≤ ⊥
⊢ ⊥.toENNReal = ⊥.toENNReal ↔ ⊥ = ⊥

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot.coe
hx : 0 ≤ ⊥
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ ⊥.toENNReal = (↑a✝).toENNReal ↔ ⊥ = ↑a✝

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot.top
hx : 0 ≤ ⊥
hy : 0 ≤ ⊤
⊢ ⊥.toENNReal = ⊤.toENNReal ↔ ⊥ = ⊤

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case coe.bot
a✝ : ℝ
hx : 0 ≤ ↑a✝
hy : 0 ≤ ⊥
⊢ (↑a✝).toENNReal = ⊥.toENNReal ↔ ↑a✝ = ⊥

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹).toENNReal = (↑a✝).toENNReal ↔ ↑a✝¹ = ↑a✝

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case coe.top
a✝ : ℝ
hx : 0 ≤ ↑a✝
hy : 0 ≤ ⊤
⊢ (↑a✝).toENNReal = ⊤.toENNReal ↔ ↑a✝ = ⊤

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case top.bot
hx : 0 ≤ ⊤
hy : 0 ≤ ⊥
⊢ ⊤.toENNReal = ⊥.toENNReal ↔ ⊤ = ⊥

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case top.coe
hx : 0 ≤ ⊤
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ ⊤.toENNReal = (↑a✝).toENNReal ↔ ⊤ = ↑a✝

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case top.top
hx hy : 0 ≤ ⊤
⊢ ⊤.toENNReal = ⊤.toENNReal ↔ ⊤ = ⊤

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case top
y : EReal
h : ⊤ ≤ y
⊢ ⊤.toENNReal ≤ y.toENNReal

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case ofNat
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
n : ℕ
⊢ count K v (I ^ ofNat n) = ofNat n * count K v I

pp: case negSucc
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
n : ℕ
⊢ count K v (I ^ -[n+1]) = -[n+1] * count K v I

Tactic:
· rw [ofNat_eq_natCast, zpow_natCast]
    exact count_pow K v n I

Goal state after:
case negSucc
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
n : ℕ
⊢ count K v (I ^ -[n+1]) = -[n+1] * count K v I
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case mpr.left
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < x

Tactic:
apply lt_of_lt_of_le _ hn

Goal state after:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < y ^ n
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ofNat.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ Int.ofNat a ≤ x ^ Int.ofNat b

Tactic:
simp only [Int.ofNat_eq_natCast, zpow_natCast]
    exact pow_right_mono₀ hx (Int.le_of_ofNat_le_ofNat h)

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case mpr
α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | dist p.1 p.2 ≤ f i} ⊆ s) → ∃ i, 0 < i ∧ {p | dist p.1 p.2 < i} ⊆ s

Tactic:
· exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, fun x (hx : _ < _) => H (mem_ofPred.2 hx.le)⟩

Goal state after:
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf 0 = 0

Tactic:
exact csInf_singleton 0

Goal state after:
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf 0 = 0

Tactic:
exact csInf_singleton 0

Goal state after:
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
f : ι → ℕ
⊢ BddAbove (range fun x ↦ ↑(f x)) ↔ BddAbove (range f)

Tactic:
← bddAbove_natCast_image_iff,

Goal state after:
ι : Sort u_3
f : ι → ℕ
⊢ BddAbove (range fun x ↦ ↑(f x)) ↔ BddAbove (Nat.cast '' range f)
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: ι : Sort u_1
r : ℝ
ha : r ≤ 0
f : ι → ℝ
⊢ (⨆ i, f i) * r = ⨅ i, f i * r

Tactic:
simp only [Real.mul_iSup_of_nonpos ha, mul_comm]

Goal state after:
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ ⨆ i, a * f i = ⨆ i, f i * a

Tactic:
simp_rw [mul_comm]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
e : p = ⊥
⊢ I = 0

Tactic:
simp_all

Goal state after: