mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

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
T : Type u_2
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Module.Finite R T
Q : Ideal T
inst✝² : P.LiesOver p
inst✝¹ : Q.LiesOver P
inst✝ : p.IsPrime
this : Q.LiesOver p
⊢ ∀ (x : R ⧸ p), (algebraMap (R ⧸ p) (T ⧸ Q)) x = (algebraMap (S ⧸ P) (T ⧸ Q)) ((algebraMap (R ⧸ p) (S ⧸ P)) x)

Tactic:
rintro ⟨x⟩

Goal state after:
case mk
R : Type u
inst✝¹⁰ : CommRing R
S : Type v
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
p : Ideal R
P : Ideal S
T : Type u_2
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Module.Finite R T
Q : Ideal T
inst✝² : P.LiesOver p
inst✝¹ : Q.LiesOver P
inst✝ : p.IsPrime
this : Q.LiesOver p
x✝ : R ⧸ p
x : R
⊢ (algebraMap (R ⧸ p) (T ⧸ Q)) (Quot.mk (⇑(Submodule.quotientRel p)) x) =
    (algebraMap (S ⧸ P) (T ⧸ Q)) ((algebraMap (R ⧸ p) (S ⧸ P)) (Quot.mk (⇑(Submodule.quotientRel p)) x))
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
I J : Ideal S
coprime : IsCoprime I J
⊢ cardQuot (I * J) = cardQuot I * cardQuot J

Tactic:
cardQuot_apply,

Goal state after:
S : Type u_1
inst✝ : CommRing S
I J : Ideal S
coprime : IsCoprime I J
⊢ Nat.card (S ⧸ I * J) = cardQuot I * cardQuot J
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
I J : Ideal S
coprime : IsCoprime I J
⊢ Nat.card (S ⧸ I * J) = cardQuot I * cardQuot J

Tactic:
cardQuot_apply,

Goal state after:
S : Type u_1
inst✝ : CommRing S
I J : Ideal S
coprime : IsCoprime I J
⊢ Nat.card (S ⧸ I * J) = Nat.card (S ⧸ I) * cardQuot J
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
I J : Ideal S
coprime : IsCoprime I J
⊢ Nat.card (S ⧸ I * J) = Nat.card (S ⧸ I) * cardQuot J

Tactic:
cardQuot_apply,

Goal state after:
S : Type u_1
inst✝ : CommRing S
I J : Ideal S
coprime : IsCoprime I J
⊢ Nat.card (S ⧸ I * J) = Nat.card (S ⧸ I) * Nat.card (S ⧸ J)
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: 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 S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
this✝¹ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap ⋯
this✝ : Algebra (S ⧸ P) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
this : Algebra (R ⧸ p) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
⊢ ∀ (x : R ⧸ p), (algebraMap (R ⧸ p) (T ⧸ I)) x = (algebraMap (S ⧸ P) (T ⧸ I)) ((algebraMap (R ⧸ p) (S ⧸ P)) x)

Tactic:
rintro ⟨x⟩

Goal state after:
case mk
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 S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
this✝¹ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap ⋯
this✝ : Algebra (S ⧸ P) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
this : Algebra (R ⧸ p) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
x✝ : R ⧸ p
x : R
⊢ (algebraMap (R ⧸ p) (T ⧸ I)) (Quot.mk (⇑(Submodule.quotientRel p)) x) =
    (algebraMap (S ⧸ P) (T ⧸ I)) ((algebraMap (R ⧸ p) (S ⧸ P)) (Quot.mk (⇑(Submodule.quotientRel p)) x))
Module: Mathlib.RingTheory.FiniteStability

Goal state before:
pp: R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
⊢ FinitePresentation B (B ⊗[R] A)

Tactic:
have hker_eq : RingHom.ker g = Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker f) :=
    Algebra.TensorProduct.lTensor_ker f hsurj

Goal state after:
R : Type w₁
inst✝⁵ : CommRing R
A : Type w₂
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w₃
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj : Function.Surjective ⇑f
hfg : (RingHom.ker f.toRingHom).FG
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj : Function.Surjective ⇑g
hker_eq : RingHom.ker g = Ideal.map TensorProduct.includeRight (RingHom.ker f)
⊢ FinitePresentation B (B ⊗[R] A)
Module: Mathlib.RingTheory.Finiteness.NilpotentKer

Goal state before:
pp: case succ.refine_2
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✝ : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective ⇑f
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this : Module.Finite R (S ⧸ I)
n : ℕ
IH : Module.Finite R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective ⇑φ
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
⊢ (⊤ ⊓ (↑R φ.toLinearMap).ker).FG

Tactic:
· have : Module.Finite R ((S ⧸ I) ⊗[S] ↑(I ^ n)) := by
        have : Module.Finite S ↑(I ^ n) := .of_fg (.pow hf₃ _)
        exact .trans (S ⧸ I) _
      let ψ : (S ⧸ I) ⊗[S] ↑(I ^ n) →ₗ[S] (S ⧸ I ^ (n + 1)) := by
        refine ?_ ∘ₗ (TensorProduct.quotTensorEquivQuotSMul _ I).toLinearMap
        refine Submodule.liftQ _ ((Submodule.mkQ _).comp (I ^ n).subtype) ?_
        rw [LinearMap.ker_comp, ← Submodule.map_le_map_iff_of_injective (I ^ n).subtype_injective,
          Submodule.map_smul'', Submodule.map_comap_eq]
        simpa [pow_succ'] using Ideal.mul_le_right (I := I) (J := I ^ n)
      convert! Module.Finite.fg_top.map (ψ.restrictScalars R) using 1
      suffices LinearMap.ker φ.toLinearMap = Submodule.map (I ^ (n + 1)).mkQ (I ^ n) by
        simpa [LinearMap.range_restrictScalars, ψ, LinearMap.range_comp, Submodule.range_liftQ]
      apply Submodule.comap_injective_of_surjective (I ^ (n + 1)).mkQ_surjective
      simpa [← LinearMap.ker_comp, hφ'] using Ideal.pow_le_pow_right n.le_succ

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
n : ℕ
⊢ absNorm (span {↑n}) = n ^ finrank ℤ S

Tactic:
by
  simp [absNorm_span_singleton, Algebra.norm_natCast]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
x : S
h : x ∈ I
⊢ ↑(absNorm I) ∣ ↑((Algebra.norm ℤ) x).natAbs

Tactic:
← absNorm_span_singleton x,

Goal state after:
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
x : S
h : x ∈ I
⊢ ↑(absNorm I) ∣ ↑(absNorm (span {x}))
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case h₁
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝ : IsAddTorsionFree S
this : CharZero S
hpMax : (span {p}).IsMaximal
hI : p ∣ ↑(absNorm 0)
⊢ ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ 0

Tactic:
obtain ⟨Q, hQ, e⟩ := Ideal.exists_ideal_over_maximal_of_isIntegral (S := S) (Ideal.span {p})
      (fun x ↦ by simp +contextual)

Goal state after:
case h₁
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝ : IsAddTorsionFree S
this : CharZero S
hpMax : (span {p}).IsMaximal
hI : p ∣ ↑(absNorm 0)
Q : Ideal S
hQ : Q.IsMaximal
e : comap (algebraMap ℤ S) Q = span {p}
⊢ ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ 0
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsOpenEmbedding f
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Tactic:
obtain ⟨_, ⟨x, hx, rfl⟩, hx'⟩ := nonempty_inter_closedPoints
    (hZ.image f) (hZ'.image hf.isInducing hf.isOpen_range.isLocallyClosed)

Goal state after:
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsOpenEmbedding f
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
x : X
hx : x ∈ Z
hx' : f x ∈ closedPoints Y
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty
Module: Mathlib.RingTheory.RamificationInertia.Inertia

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✝² : q.LiesOver p
inst✝¹ : p.IsMaximal
inst✝ : q.IsMaximal
⊢ q.inertiaDeg R = Module.finrank (R ⧸ p) (S ⧸ q)

Tactic:
let : Field (R ⧸ p) := Quotient.field p
  let : Field (S ⧸ q) := Quotient.field q
  exact inertiaDeg_eq_of_isFractionRing p q (R ⧸ p) (S ⧸ q)

Goal state after:
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 σ
x : ↥Q.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
⊢ (δ Q P) ⟨Extension.Cotangent.mk x, hx⟩ = (δAux R Q) ↑x

Tactic:
let y := Extension.Cotangent.mk (P := (Q.comp P).toExtension) (Q.kerCompPreimage P x)

Goal state after:
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.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
⊢ (δ Q P) ⟨Extension.Cotangent.mk x, hx⟩ = (δAux R Q) ↑x
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
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
s : S
t : P
⊢ s •
      (derivationQuotKerSq R P S).liftKaehlerDifferential
        ((D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)) ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) t)) =
    s ⊗ₜ[P] (D R P) t

Tactic:
simp [smul_tmul']

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
⊢ (Ideal.map (algebraMap R S) (maximalIdeal R)).IsMaximal

Tactic:
rw [Ideal.Quotient.maximal_ideal_iff_isField_quotient]

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
⊢ 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✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
x : S
hx : x ∈ RingHom.ker (algebraMap S (ResidueField S))
⊢ x ∈ Ideal.map (algebraMap R S) (maximalIdeal R)

Tactic:
simpa [H] using hx

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

Goal state before:
pp: case mem
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✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
x✝ x : S
h : x ∈ ⇑(algebraMap R S) '' ↑(maximalIdeal R)
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) x = 0

Tactic:
obtain ⟨x, hx, rfl⟩ := h; simp

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

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
Sq : Type u_1 := Localization.AtPrime q
⊢ 0 < q.ramificationIdx R

Tactic:
rw [ramificationIdx_def]

Goal state after:
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
Sq : Type u_1 := Localization.AtPrime q
⊢ 0 <
    (Module.length (Localization.AtPrime q)
        (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q))).toNat
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: 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
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝² : FormallySmooth R P.Ring
this✝¹ : FormallySmooth P.Ring (Localization M')
this✝ : FormallySmooth R Q.Ring
this : Module.Flat S T
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T

Tactic:
letI : Algebra P.Ring Q.Ring := (inferInstance : Algebra P.Ring (Localization M'))

Goal state after:
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
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝³ : FormallySmooth R P.Ring
this✝² : FormallySmooth P.Ring (Localization M')
this✝¹ : FormallySmooth R Q.Ring
this✝ : Module.Flat S T
this : Algebra P.Ring Q.Ring := inferInstance
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T
Module: Mathlib.Data.NNReal.Defs

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

Tactic:
← coe_one,

Goal state after:
r : ℝ≥0
⊢ ↑r = ↑1 ↔ r = 1
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
hf : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
h_ne_zero : v.maxPowDividing I ≠ 0
⊢ ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I

Tactic:
← mul_finprod_cond_ne v hf,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
h_ne_zero : v.maxPowDividing I ≠ 0
⊢ ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
      v.maxPowDividing I * ∏ᶠ (i : HeightOneSpectrum R) (_ : i ≠ v), i.maxPowDividing I
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: a b c : ℝ≥0
h : a ≠ 0
⊢ a * b = a * c ↔ b = c

Tactic:
mul_eq_mul_left_iff,

Goal state after:
a b c : ℝ≥0
h : a ≠ 0
⊢ b = c ∨ a = 0 ↔ b = c
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inl
x : ℝ
hx : 0 ≤ x
⊢ (↑x.toNNReal⁻¹).toNNReal = x.toNNReal⁻¹

Tactic:
Real.toNNReal_coe

Goal state after:
case inl
x : ℝ
hx : 0 ≤ x
⊢ x.toNNReal⁻¹ = x.toNNReal⁻¹
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: α : Sort u_2
⊢ ⨅ x, 0 = 0

Tactic:
rw [← coe_inj, coe_iInf]

Goal state after:
α : Sort u_2
⊢ ⨅ i, ↑0 = ↑0
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: r : ℝ≥0
⊢ ↑r = ↑(↑r).toNNReal

Tactic:
Real.toNNReal_coe

Goal state after:
r : ℝ≥0
⊢ ↑r = ↑r
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1

Tactic:
rw [if_neg hx]

Goal state after:
case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ 1 + if y = 0 then 0 else 1
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ (if x * y = 1 then 0 else 1) ≤ (if x = 1 then 0 else 1) + if y = 1 then 0 else 1

Tactic:
rw [if_neg hx]

Goal state after:
case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ (if x * y = 1 then 0 else 1) ≤ 1 + if y = 1 then 0 else 1
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 : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)

Tactic:
h_a₁J₁,

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 : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁ = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b : ℝ≥0∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a * b = b ↔ a = 1

Tactic:
by
  simpa using ENNReal.mul_left_inj hb₀ hb (b := 1)

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

Goal state before:
pp: case h₁
ι : Type u_2
inst✝¹ : Preorder ι
inst✝ : IsCodirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
⊢ f _k ≤ f i

Tactic:
apply_rules

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

Goal state before:
pp: case h₂
ι : Type u_2
inst✝¹ : Preorder ι
inst✝ : IsCodirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
⊢ g _k ≤ g j

Tactic:
apply_rules

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 : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ ¬choose ⋯ = 0

Tactic:
exact h_J₁_ne_zero

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

Goal state before:
pp: case h₁
ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ f i ≤ f _k

Tactic:
apply_rules

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

Goal state before:
pp: case h₂
ι : Type u_3
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ g j ≤ g _k

Tactic:
apply_rules

Goal state after: