mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
⊢ f (a * b) = f a * f b

Tactic:
by_cases hf1 : f 1 = 0

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : f 1 = 0
⊢ f (a * b) = f a * f b

case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
⊢ f (a * b) = f a * f b
Module: Mathlib.RingTheory.Artinian.Ring

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
⊢ Function.Surjective ⇑(algebraMap R L)

Tactic:
intro r'

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r' : L
⊢ ∃ a, (algebraMap R L) a = r'
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
⊢ cardQuot 1 = 1

Tactic:
by rw [Ideal.one_eq_top, cardQuot_top]

Goal state after:
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : s.Finite
span : Submodule.span R (⋃ i, {↑i}) = ⊤
⊢ IsNoetherian R M

Tactic:
Submodule.span_iUnion

Goal state after:
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : s.Finite
span : ⨆ i, R ∙ ↑i = ⊤
⊢ IsNoetherian R M
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
P : Ideal S
h : ¬map f p ≤ P
⊢ ¬map f p ≤ P ^ (0 + 1)

Tactic:
by simpa using h

Goal state after:
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✝ : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot : RelSeries.head s = ⊥
hs_top : RelSeries.last s = ⊤
this :
  ∀ (k : Fin (s.length + 1)),
    length B ↥(Submodule.baseChange B (s.toFun k)) = ↑↑k * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
⊢ length B (B ⊗[A] M) = ↑s.length * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
by
      rw [← Fin.val_last s.length, ← this, ← RelSeries.last, hs_top, baseChange_top, length_top]

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
⊢ emultiplicity P (map f p) = ↑(p.ramificationIdx' P)

Tactic:
ramificationIdx'_eq_normalizedFactors_count hp hP hP₂,

Goal state after:
case neg
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
⊢ emultiplicity P (map f p) = ↑(Multiset.count P (normalizedFactors (map f p)))
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
⊢ emultiplicity P (map f p) = ↑(p.ramificationIdx' P)

Tactic:
rw [ramificationIdx'_eq_normalizedFactors_count hp hP hP₂, ← normalize_eq P,
    ← UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors _ hp, normalize_eq]

Goal state after:
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
⊢ Irreducible P
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
inst✝ : QuasiFiniteAt R Q
⊢ QuasiFiniteAt R P

Tactic:
by
  let f : Localization.AtPrime Q →ₐ[R] Localization.AtPrime P :=
    IsLocalization.liftAlgHom (M := Q.primeCompl) (f := IsScalarTower.toAlgHom _ _ _) <| by
      simp only [IsScalarTower.coe_toAlgHom', Subtype.forall, Ideal.mem_primeCompl_iff]
      exact fun a ha ↦ IsLocalization.map_units (M := P.primeCompl) _ ⟨a, fun h ↦ ha (h₁ h)⟩
  refine .of_forall_exists_mul_mem_range f fun x ↦ ?_
  obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq P.primeCompl x
  exact ⟨algebraMap _ _ s, by simpa [f] using IsLocalization.map_units _ ⟨s, hs⟩,
    algebraMap _ _ x, by simp [f]⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsArtinianRing R
p : PrimeSpectrum S
inst✝ : FiniteType R S
H : IsClopen {p}
this✝ : IsNoetherianRing S
this : IsJacobsonRing S
⊢ QuasiFiniteAt R p.asIdeal

Tactic:
obtain ⟨e, he, H⟩ := PrimeSpectrum.isClopen_iff.mp H

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsArtinianRing R
p : PrimeSpectrum S
inst✝ : FiniteType R S
H✝ : IsClopen {p}
this✝ : IsNoetherianRing S
this : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H : {p} = ↑(PrimeSpectrum.basicOpen e)
⊢ QuasiFiniteAt R p.asIdeal
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
x : M
⊢ (_root_.TensorProduct.lift (↑R (↑R (lsmul S S M).toLinearMap.flip).flip))
      ((TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip x)) (elem R S)) =
    (TensorProduct.lmul' R) (elem R S) • x

pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
x : M
⊢ (TensorProduct.lmul' R) (elem R S) • x = x

Tactic:
· induction elem R S using TensorProduct.induction_on with
    | zero => simp
    | tmul r s => simp [mul_smul, smul_comm r s]
    | add y z hy hz => simp [hy, hz, add_smul]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
x : M
⊢ (TensorProduct.lmul' R) (elem R S) • x = x
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case monomial.monomial
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₁
Q : Generators S T ι
n : ι →₀ ℕ
r : S
m : ι →₀ ℕ
s : S
⊢ ((algebraMap S T) r * (n + m).prod fun x1 x2 ↦ Q.val x1 ^ x2) ⊗ₜ[S] (D R S) s +
      ((algebraMap S T) s * (n + m).prod fun x1 x2 ↦ Q.val x1 ^ x2) ⊗ₜ[S] (D R S) r =
    ((algebraMap S T) r * ((n.prod fun x1 x2 ↦ Q.val x1 ^ x2) * m.prod fun x1 x2 ↦ Q.val x1 ^ x2)) ⊗ₜ[S] (D R S) s +
      ((algebraMap S T) s * ((m.prod fun x1 x2 ↦ Q.val x1 ^ x2) * n.prod fun x1 x2 ↦ Q.val x1 ^ x2)) ⊗ₜ[S] (D R S) r

Tactic:
rw [mul_comm (m.prod _) (n.prod _)]

Goal state after:
case monomial.monomial
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₁
Q : Generators S T ι
n : ι →₀ ℕ
r : S
m : ι →₀ ℕ
s : S
⊢ ((algebraMap S T) r * (n + m).prod fun x1 x2 ↦ Q.val x1 ^ x2) ⊗ₜ[S] (D R S) s +
      ((algebraMap S T) s * (n + m).prod fun x1 x2 ↦ Q.val x1 ^ x2) ⊗ₜ[S] (D R S) r =
    ((algebraMap S T) r * ((n.prod fun x1 x2 ↦ Q.val x1 ^ x2) * m.prod fun x1 x2 ↦ Q.val x1 ^ x2)) ⊗ₜ[S] (D R S) s +
      ((algebraMap S T) s * ((n.prod fun x1 x2 ↦ Q.val x1 ^ x2) * m.prod fun x1 x2 ↦ Q.val x1 ^ x2)) ⊗ₜ[S] (D R S) r
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
⊢ σ 1 - ↑(l (1 ⊗ₜ[P] (D R P) (σ 1))) = 1

Tactic:
simp [sectionOfRetractionKerToTensorAux_prop l hl (σ 1) 1 (by simp [hσ])]

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)
this✝¹ : IsArtinianRing (S ⧸ mR)
this✝ : Nontrivial (S ⧸ mR)
this : IsLocalRing (S ⧸ mR)
⊢ ⊥.jacobson = ⊥

Tactic:
IsArtinianRing.jacobson_eq_radical,

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)
⊢ ⊥.radical = ⊥
Module: Mathlib.RingTheory.RamificationInertia.Ramification

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
q : Ideal S
inst✝² : IsDedekindDomain S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
hp : map (algebraMap R S) p ≠ ⊥
hq : q ≠ ⊥
⊢ Multiset.count q (normalizedFactors (map (algebraMap R S) p)) = multiplicity q (map (algebraMap R S) p)

Tactic:
multiplicity_eq_of_emultiplicity_eq_some (emultiplicity_eq_count_normalizedFactors
      (prime_of_isPrime hq inferInstance).irreducible hp),

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
q : Ideal S
inst✝² : IsDedekindDomain S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
hp : map (algebraMap R S) p ≠ ⊥
hq : q ≠ ⊥
⊢ Multiset.count q (normalizedFactors (map (algebraMap R S) p)) =
    Multiset.count (normalize q) (normalizedFactors (map (algebraMap R S) p))
Module: Mathlib.RingTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
p : Ideal R
inst✝⁶ : p.IsPrime
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : Module.Finite R S
inst✝¹ : Module.Flat R S
inst✝ : Fintype ↑(p.primesOver S)
⊢ ∑ q, (↑q).ramificationIdx R * (↑q).inertiaDeg R = Module.finrank R S

Tactic:
rw [sum_ramification_inertia_eq_finrank_fiber, finrank_fiber_eq_finrank]

Goal state after:
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:
by simp_all

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 ∈ s.powerset, (-1) ^ #t • if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a) =
    ∑ y ∈ s.powerset, ∑ x ∈ s.biUnion S, ((-1) ^ #y * ((∏ i ∈ s \ y, 1) * ∏ i ∈ y, (↑(S i)).indicator 1 x)) • f x

Tactic:
congr! with t

Goal state after:
case a
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
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) =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x
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
⊢ ∑ a ∈ s.biUnion S, (∏ i ∈ s, (1 - (↑(S i)).indicator 1 a)) • f a =
    ∑ a ∈ s.biUnion S, (∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a)) • f a

Tactic:
congr! with t

Goal state after:
case a.a
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : α
a✝¹ : t ∈ s.biUnion S
x✝ : ι
a✝ : x✝ ∈ s
⊢ 1 = (↑(s.biUnion S)).indicator 1 t
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
h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd : v.maxPowDividing I ∣ ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I
h_not_dvd :
  ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I
⊢ (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
    (Associates.mk v.asIdeal).count (Associates.mk I).factors

Tactic:
simp only [IsDedekindDomain.HeightOneSpectrum.maxPowDividing] at h_dvd h_ne_zero h_not_dvd

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.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠
    0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors ∣
    ∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors
h_not_dvd :
  ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors
⊢ (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 : ℝ
h : 0 ≤ x
⊢ nnabs x = x.toNNReal

Tactic:
by
  ext
  rw [coe_toNNReal x h, coe_nnabs, abs_of_nonneg h]

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
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors) =
    ↑(span {a})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors)) =
    (∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)) *
      ∏ᶠ (x : HeightOneSpectrum R),
        (↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk (span {a})).factors))⁻¹

Tactic:
← zpow_neg

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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors) =
    ↑(span {a})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors)) =
    (∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)) *
      ∏ᶠ (x : HeightOneSpectrum R),
        ↑x.asIdeal ^ (-↑((Associates.mk x.asIdeal).count (Associates.mk (span {a})).factors))
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: a b : ℝ≥0∞
h : b < a
⊢ ∃ ε, 0 < ε ∧ b < ∞ ∧ b + ↑ε < a

Tactic:
rcases lt_iff_exists_add_pos_lt.1 h with ⟨r, hr0, hr⟩

Goal state after:
a b : ℝ≥0∞
h : b < a
r : ℝ≥0
hr0 : 0 < r
hr : b + ↑r < a
⊢ ∃ ε, 0 < ε ∧ b < ∞ ∧ b + ↑ε < a
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: t : Set ℝ≥0
h : t.OrdConnected
x : ℝ≥0
hx : x ∈ t
y : ℝ≥0
hy : y ∈ t
z : ℝ≥0∞
hz : z ∈ Icc ↑x ↑y
⊢ z ∈ ofNNReal '' t

Tactic:
rcases ENNReal.le_coe_iff.1 hz.2 with ⟨z, rfl, -⟩

Goal state after:
t : Set ℝ≥0
h : t.OrdConnected
x : ℝ≥0
hx : x ∈ t
y : ℝ≥0
hy : y ∈ t
z : ℝ≥0
hz : ↑z ∈ Icc ↑x ↑y
⊢ ↑z ∈ ofNNReal '' t
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a : ℝ
b : ℝ≥0
⊢ ENNReal.ofReal a ≤ ↑b ↔ a ≤ ↑b

Tactic:
by
  simp [← ofReal_le_ofReal_iff]

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

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
⊢ a < a + b

Tactic:
rwa [← pos_iff_ne_zero, ← ENNReal.add_lt_add_iff_left ha, add_zero] at hb

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝 a

Tactic:
by
  rw [← nhdsLE_sup_nhdsGE, mem_sup]
  exact ⟨compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE hd ha,
    compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE hd ha⟩

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a ≤ ⨆ b, ⨆ (_ : b < a), b

Tactic:
refine le_of_forall_lt fun c hca ↦ ?_

Goal state after:
a c : ℝ≥0∞
hca : c < a
⊢ c < ⨆ b, ⨆ (_ : b < a), b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ 0 < b → b < a → c⁻¹ ≠ ∞

Tactic:
by simpa using h

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

Goal state before:
pp: case neg
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
n : ℤ
I : FractionalIdeal R⁰ K
hI : ¬I = 0
⊢ count K v 1 = 0

Tactic:
exact count_one K v

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

Goal state before:
pp: case hp₀
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
exps : HeightOneSpectrum R → ℤ
⊢ count K v 1 = 0

Tactic:
exact count_one K v

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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : I ≠ 0 ∧ I' ≠ 0
⊢ count K v (I * I') = 0

Tactic:
count_mul' K v,

Goal state after:
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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : I ≠ 0 ∧ I' ≠ 0
⊢ (if I ≠ 0 ∧ I' ≠ 0 then count K v I + count K v I' else 0) = 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : ¬(I ≠ 0 ∧ I' ≠ 0)
⊢ count K v (I * I') = 0

Tactic:
count_mul' K v,

Goal state after:
case neg
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
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : ¬(I ≠ 0 ∧ I' ≠ 0)
⊢ (if I ≠ 0 ∧ I' ≠ 0 then count K v I + count K v I' else 0) = 0
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ y ∈ eball x ε ↔ edist x y < ε

Tactic:
edist_comm,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ y ∈ eball x ε ↔ edist y x < ε
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ y ∈ closedEBall x ε ↔ edist x y ≤ ε

Tactic:
edist_comm,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ y ∈ closedEBall x ε ↔ edist y x ≤ ε