mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (1 - f 1) ^ n = 0

Tactic:
← Ideal.mem_bot,

Goal state after:
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
⊢ (1 - f 1) ^ n ∈ ⊥
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: 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 σ
r : S
hr : C r ∈ Q.ker
⊢ (δ Q P) ⟨Extension.Cotangent.mk ⟨C r, hr⟩, ⋯⟩ = 1 ⊗ₜ[S] (D R S) r

Tactic:
by
  rw [δ_eq_δAux, δAux_C]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
mR : Ideal S := Ideal.map (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this✝⁴ : Algebra (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun x1 x2 ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯, commutes' := ⋯,
    smul_def' := ⋯ }
this✝³ : IsScalarTower R (ResidueField R) (S ⧸ mR)
this✝² : FormallyUnramified (ResidueField R) (S ⧸ mR)
this✝¹ : EssFiniteType (ResidueField R) (S ⧸ mR)
this✝ : Module.Finite (ResidueField R) (S ⧸ mR)
this : IsReduced (S ⧸ mR)
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
have : IsArtinianRing (S ⧸ mR) := isArtinian_of_tower (ResidueField R) inferInstance

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
mR : Ideal S := Ideal.map (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this✝⁵ : Algebra (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun x1 x2 ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯, commutes' := ⋯,
    smul_def' := ⋯ }
this✝⁴ : IsScalarTower R (ResidueField R) (S ⧸ mR)
this✝³ : FormallyUnramified (ResidueField R) (S ⧸ mR)
this✝² : EssFiniteType (ResidueField R) (S ⧸ mR)
this✝¹ : Module.Finite (ResidueField R) (S ⧸ mR)
this✝ : IsReduced (S ⧸ mR)
this : IsArtinianRing (S ⧸ mR)
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
mR : Ideal S := Ideal.map (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this✝⁷ : Algebra (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun x1 x2 ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯, commutes' := ⋯,
    smul_def' := ⋯ }
this✝⁶ : IsScalarTower R (ResidueField R) (S ⧸ mR)
this✝⁵ : FormallyUnramified (ResidueField R) (S ⧸ mR)
this✝⁴ : EssFiniteType (ResidueField R) (S ⧸ mR)
this✝³ : Module.Finite (ResidueField R) (S ⧸ mR)
this✝² : IsReduced (S ⧸ mR)
this✝¹ : IsArtinianRing (S ⧸ mR)
this✝ : Nontrivial (S ⧸ mR)
this : IsLocalRing (S ⧸ mR)
⊢ Ideal.radical 0 = 0

Tactic:
← nilradical,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
mR : Ideal S := Ideal.map (algebraMap R S) (maximalIdeal R)
hmR : mR ≤ maximalIdeal S
this✝⁷ : Algebra (ResidueField R) (S ⧸ mR) :=
  { smul := Quotient.lift₂ (fun x1 x2 ↦ ⟦x1 • x2⟧) ⋯,
    algebraMap := Ideal.quotientMap (Ideal.map (algebraMap R S) (maximalIdeal R)) (algebraMap R S) ⋯, commutes' := ⋯,
    smul_def' := ⋯ }
this✝⁶ : IsScalarTower R (ResidueField R) (S ⧸ mR)
this✝⁵ : FormallyUnramified (ResidueField R) (S ⧸ mR)
this✝⁴ : EssFiniteType (ResidueField R) (S ⧸ mR)
this✝³ : Module.Finite (ResidueField R) (S ⧸ mR)
this✝² : IsReduced (S ⧸ mR)
this✝¹ : IsArtinianRing (S ⧸ mR)
this✝ : Nontrivial (S ⧸ mR)
this : IsLocalRing (S ⧸ mR)
⊢ nilradical (S ⧸ mR) = 0
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
⊢ Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S

Tactic:
apply eq_maximalIdeal
  rw [Ideal.Quotient.maximal_ideal_iff_isField_quotient]
  exact isField_quotient_map_maximalIdeal

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
x : Localization.AtPrime p
hx : (localRingHom p q (algebraMap R S) ⋯) x = 0
⊢ x = 0

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq p.primeCompl x

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
x : R
s : ↥p.primeCompl
hx : (localRingHom p q (algebraMap R S) ⋯) (IsLocalization.mk' (Localization.AtPrime p) x s) = 0
⊢ IsLocalization.mk' (Localization.AtPrime p) x s = 0
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case pos
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
q : Ideal S
r : Ideal T
inst✝¹ : r.LiesOver q
inst✝ : Module.Flat S T
hr : r.IsPrime
⊢ r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S

Tactic:
have : q.IsPrime := isPrime_of_liesOver r q

Goal state after:
case pos
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
q : Ideal S
r : Ideal T
inst✝¹ : r.LiesOver q
inst✝ : Module.Flat S T
hr : r.IsPrime
this : q.IsPrime
⊢ r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : CommRing A
I : Ideal A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module A M
inst✝¹ : Module A M₁
inst✝ : Module A M₂
φ : M₁ →ₗ[A] M₂
c : ↥(primaryComponent M₁ I)
⊢ (φ.domRestrict (primaryComponent M₁ I)) c ∈ primaryComponent M₂ I

Tactic:
by simpa only [LinearMap.domRestrict_apply] using primaryComponent_map_mem I φ c

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ t, (-1) ^ #↑t • ∑ a ∈ (↑t).inf' ⋯ S, f a + ∑ t ∈ s.powerset with ¬t.Nonempty, (-1) ^ #t • ∑ a ∈ s.biUnion S, f a =
    ∑ t ∈ s.powerset, (-1) ^ #t • if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a

Tactic:
rw [← sum_attach (filter ..)]; simp [sum_dite]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a, f a - ∑ a ∈ s.biUnion S, f a =
    ∑ t ∈ s.powerset with ¬t.Nonempty, (-1) ^ #t • ∑ a ∈ t.inf S, f a +
      ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ #t • ∑ a ∈ t.inf S, f a

Tactic:
simp [← sum_attach (filter ..), inclusion_exclusion_sum_biUnion, inf'_eq_inf, filter_eq',
        sub_eq_add_neg, pow_succ]

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

Goal state before:
pp: s : Set ℝ
h₁ : s.Nonempty
h₂ : BddBelow s
⊢ IsLUB (-s) (sSup (-s))

Tactic:
exact Real.isLUB_sSup h₁.neg h₂.neg

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

Goal state before:
pp: f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
⊢ ∃ x, f ≈ const abs x

Tactic:
have lb : ∃ x, x ∈ s := exists_lt f

Goal state after:
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
⊢ ∃ x, f ≈ const abs x
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
    (Associates.mk v.asIdeal).count (Associates.mk I).factors

Tactic:
have h_ne_zero := Associates.finprod_ne_zero I

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
    (Associates.mk v.asIdeal).count (Associates.mk I).factors
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this✝ : a * x⁻¹ < 1
this : a * (x⁻¹ * x) ≤ y
⊢ a ≤ y

Tactic:
inv_mul_cancel₀ hx,

Goal state after:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this✝ : a * x⁻¹ < 1
this : a * 1 ≤ y
⊢ a ≤ y
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inl
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : x.toNNReal ≤ z ∧ z ≤ y.toNNReal
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s

Tactic:
Real.toNNReal_of_nonpos hy₀,

Goal state after:
case inl
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : x.toNNReal ≤ z ∧ z ≤ 0
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q f g : GroupSeminorm E
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q g : GroupSeminorm E
toFun✝ : E → ℝ
map_one'✝ : toFun✝ 1 = 0
mul_le'✝ : ∀ (x y : E), toFun✝ (x * y) ≤ toFun✝ x + toFun✝ y
inv'✝ : ∀ (x : E), toFun✝ x⁻¹ = toFun✝ x
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ } = (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ } = g
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: a : ℝ≥0∞
h : ENNReal.ofReal a.toReal = a
⊢ a ≠ ∞

Tactic:
by
    rw [← h]
    exact ofReal_ne_top

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

Goal state before:
pp: case inr
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

Tactic:
refine ENNReal.eq_sub_of_add_eq ofReal_ne_top ?_

Goal state after:
case inr
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
⊢ ENNReal.ofReal (p - q) + ENNReal.ofReal q = ENNReal.ofReal p
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: p : EReal → Prop
⊢ (∃ r, p r) → p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r

Tactic:
rintro ⟨r, hr⟩

Goal state after:
p : EReal → Prop
r : EReal
hr : p r
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r
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
h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')
⊢ count K v (I * I') = count K v I + count K v I'

Tactic:
rw [count_well_defined K v hI haJ, count_well_defined K v hI' haJ',
    count_well_defined K v (mul_ne_zero hI hI') h_prod, ← Associates.mk_mul_mk,
    Associates.count_mul hJ_ne_zero hJ'_ne_zero hv, ← Ideal.span_singleton_mul_span_singleton,
    ← Associates.mk_mul_mk, Associates.count_mul ha_ne_zero ha'_ne_zero hv]

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
h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors +
          (Associates.mk v.asIdeal).count (Associates.mk J').factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors +
          (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a'})).factors) =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) +
      (↑((Associates.mk v.asIdeal).count (Associates.mk J').factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a'})).factors))
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case succ
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 : ℕ
h : count K v (I ^ n) = ↑n * count K v I
⊢ count K v (I ^ (n + 1)) = ↑(n + 1) * count K v I

Tactic:
classical rw [pow_succ, count_mul']
    by_cases hI : I = 0
    · have h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0) := by order
      rw [if_neg h_neg, hI, count_zero, mul_zero]
    · rw [if_pos (And.intro (pow_ne_zero n hI) hI), h, Nat.cast_add,
        Nat.cast_one]
      ring

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

Goal state before:
pp: a b c : ℝ≥0∞
h₁ : a ≠ 0 ∨ b ≠ ∞
h₂ : a ≠ ∞ ∨ b ≠ 0
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ c ≤ a * b

Tactic:
by
  rw [← ENNReal.inv_le_inv, ENNReal.mul_inv h₁ h₂]
  exact mul_le_of_forall_lt fun a' ha' b' hb' ↦ ENNReal.le_inv_iff_le_inv.1 <|
    (h _ (ENNReal.lt_inv_iff_lt_inv.1 ha') _ (ENNReal.lt_inv_iff_lt_inv.1 hb')).trans_eq
    (ENNReal.mul_inv (Or.inr hb'.ne_top) (Or.inl ha'.ne_top)).symm

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

Goal state before:
pp: case pos
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 J : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : J = 0
⊢ count K v J ≤ count K v I

Tactic:
exact (hI (FractionalIdeal.le_zero_iff.mp (h.trans hJ.le))).elim

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
⊢ ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε

Tactic:
by
  rw [ContinuousAt, tendsto_nhds_nhds]

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
s : Set β
hs : ∀ x ∈ s, ∃ ε > 0, Metric.eball x ε ⊆ s
x : α
hx : f x ∈ s
ε : ℝ≥0∞
hε : ε > 0
hεs : Metric.eball (f x) ε ⊆ s
⊢ ∃ ε > 0, Metric.eball x ε ⊆ f ⁻¹' s

Tactic:
exact ⟨ε, hε, fun y hy ↦ hεs hy⟩

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
I : FractionalIdeal R⁰ K
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, count K v I = 0

Tactic:
by
  by_cases hI : I = 0
  · simp only [hI, count_zero, Filter.eventually_cofinite, not_true_eq_false, ofPred_false,
      finite_empty]
  · convert! finite_factors' hI (choose_spec (choose_spec (exists_eq_spanSingleton_mul I))).2
    rw [count_ne_zero K _ hI]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 < ε
⊢ x ∈ ball x ε

Tactic:
rwa [mem_ball, dist_self]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ↔ ∀ x ∈ s, ∃ ε > 0, ball x ε ⊆ s

Tactic:
simp only [isOpen_iff_mem_nhds, mem_nhds_iff]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
⊢ ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε

Tactic:
by
  rw [ContinuousAt, tendsto_nhds_nhds]

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

Goal state before:
pp: X : Type u_2
inst✝ : PseudoMetricSpace X
s : Set X
ε : ℝ
hs : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
hε : 0 < ε
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, ball x ε

Tactic:
obtain ⟨t, hst⟩ := hs.elim_finite_subcover (fun x : s ↦ ball x ε) (fun _ ↦ isOpen_ball) fun x hx ↦
    let ⟨y, hy, hxy⟩ := Metric.mem_closure_iff.1 hx _ hε; mem_iUnion.2 ⟨⟨y, hy⟩, hxy⟩
  refine ⟨t.map ⟨Subtype.val, Subtype.val_injective⟩, by simp, Finset.finite_toSet _, ?_⟩
  simpa using subset_closure.trans hst

Goal state after:
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : α
⊢ interior (Ico a b) = Ioo a b

Tactic:
rw [← Ici_inter_Iio, interior_inter, interior_Ici, interior_Iio, Ioi_inter_Iio]

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
⊢ upperBounds (f '' S) ⊆ upperBounds (closure[inst✝³] (f '' S))

Tactic:
intro x hx i hi

Goal state after:
γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
x : α
hx : x ∈ upperBounds (f '' S)
i : α
hi : i ∈ closure[inst✝³] (f '' S)
⊢ i ≤ x
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✝
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
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
hb' : b = 1
⊢ ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * b = c

Tactic:
subst hb'

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✝
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
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
⊢ ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * 1 = c
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✝
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
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
⊢ ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * 1 = c

Tactic:
have H : Ideal.span {c.den.1} * a.num ≤ c.num * Ideal.span {a.den.1} := by
    rw [← FractionalIdeal.coeIdeal_le_coeIdeal K]
    simp only [FractionalIdeal.coeIdeal_mul, FractionalIdeal.coeIdeal_span_singleton, ←
      FractionalIdeal.den_mul_self_eq_num']
    ring_nf
    gcongr

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✝
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
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
H : Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}
⊢ ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * 1 = c