mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: case neg.mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
h : ∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1
⊢ ∀ i ∈ p.support, (v.intAdicAbv hb) (p.coeff i) < 1

Tactic:
]

Goal state after:
case neg.mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
h : ∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1
⊢ ∀ i ∈ p.support, (v.intAdicAbv hb) (p.coeff i) < 1
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: case neg.mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
h : ∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1
n : ℕ
hn : p.coeff n ≠ 0
⊢ (v.intAdicAbv hb) (p.coeff n) < 1

Tactic:
]

Goal state after:
case neg.mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
h : ∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1
n : ℕ
hn : p.coeff n ≠ 0
⊢ (v.intAdicAbv hb) (p.coeff n) < 1
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
hR : ¬IsField R
b : NNReal
hb : 1 < b
p : R[X]
⊢ (∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1) ↔
    ∀ (v : HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
hx : IsGroupLikeElem R x
h : x ∉ Set.range fun x ↦ single x 1
this✝ : LinearIndepOn R id (insert x (Set.range fun x ↦ single x 1))
this : x.coeff.sum single ∉ span R (Set.range fun x ↦ single x 1)
g : M
hg : g ∈ x.coeff.support
⊢ x.coeff g • single g 1 ∈ span R (Set.range fun x ↦ single x 1)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
hx : IsGroupLikeElem R x
h : x ∉ Set.range fun x ↦ single x 1
this✝ : LinearIndepOn R id (insert x (Set.range fun x ↦ single x 1))
this : x.coeff.sum single ∉ span R (Set.range fun x ↦ single x 1)
g : M
hg : g ∈ x.coeff.support
⊢ x.coeff g • single g 1 ∈ span R (Set.range fun x ↦ single x 1)
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : R[G] →ₐc[R] R[H]
g₁ g₂ : G
⊢ f (single g₁ 1) * f (single g₂ 1) = single (mapDomainOfBialgHomFun f g₁) 1 * single (mapDomainOfBialgHomFun f g₂) 1

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : R[G] →ₐc[R] R[H]
g₁ g₂ : G
⊢ f (single g₁ 1) * f (single g₂ 1) = single (mapDomainOfBialgHomFun f g₁) 1 * single (mapDomainOfBialgHomFun f g₂) 1
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
g : G
r : R
⊢ r • single ((mapDomainOfBialgHom f) g) 1 = r • f (single g 1)

Tactic:
]

Goal state after:
R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
g : G
r : R
⊢ r • single ((mapDomainOfBialgHom f) g) 1 = r • f (single g 1)
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: case single_one_right
R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
x : G
⊢ single ((mapDomainOfBialgHom f) x) 1 = f (single x 1)

Tactic:
]

Goal state after:
case single_one_right
R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
x : G
⊢ single ((mapDomainOfBialgHom f) x) 1 = f (single x 1)
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : R[H] →ₐc[R] R[I]
g : R[G] →ₐc[R] R[H]
⊢ mapDomainOfBialgHom (f.comp g) = mapDomainOfBialgHom (f.comp g)

Tactic:
]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ mapCycles₂ (g.comp f) (φ ≫ (resFunctor f).map ψ) =
    cyclesMap' (mapShortComplexH2 (g.comp f) (φ ≫ (resFunctor f).map ψ)) (shortComplexH2 A).moduleCatLeftHomologyData
      (shortComplexH2 C).moduleCatLeftHomologyData

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ (v.intValuation.extendToLocalization ⋯ K) ↑x = ?m.34 * ?m.36

Tactic:
]

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ (v.intValuation.extendToLocalization ⋯ K) ↑x = ?m.34 * ?m.36
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    ↑v.intValuation.toMonoidWithZeroHom ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 *
      ↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).domRestrict R⁰) ⋯)
            ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2)⁻¹

Tactic:
]

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    ↑v.intValuation.toMonoidWithZeroHom ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 *
      ↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).domRestrict R⁰) ⋯)
            ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2)⁻¹
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    ↑v.intValuation.toMonoidWithZeroHom ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 *
      (↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).domRestrict R⁰) ⋯)
            ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2))⁻¹

Tactic:
]

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    ↑v.intValuation.toMonoidWithZeroHom ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 *
      (↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).domRestrict R⁰) ⋯)
            ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2))⁻¹
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ (valuation K v) ↑1 = ↑1

Tactic:
]

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ (valuation K v) ↑1 = ↑1
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ v.valuationOfNeZeroToFun 1 = 1

Tactic:
rw [← WithZero.coe_inj, valuationOfNeZeroToFun_eq]; exact map_one _

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x✝¹ x✝ : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun (x✝¹ * x✝)) = ↑(v.valuationOfNeZeroToFun x✝¹) * ↑(v.valuationOfNeZeroToFun x✝)

Tactic:
]

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x✝¹ x✝ : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun (x✝¹ * x✝)) = ↑(v.valuationOfNeZeroToFun x✝¹) * ↑(v.valuationOfNeZeroToFun x✝)
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Rˣ
⊢ (valuation K v) (↑(algebraMap R K) ↑x) ≤ ↑1 ∧ ¬(valuation K v) (↑(algebraMap R K) ↑x) < ↑1

Tactic:
]

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Rˣ
⊢ (valuation K v) (↑(algebraMap R K) ↑x) ≤ ↑1 ∧ ¬(valuation K v) (↑(algebraMap R K) ↑x) < ↑1
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: case right
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : v.intValuation x * v.intValuation inv✝ = 1
⊢ ¬(valuation K v) ((algebraMap R K) x) < 1

Tactic:
]

Goal state after:
case right
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : v.intValuation x * v.intValuation inv✝ = 1
⊢ ¬(valuation K v) ((algebraMap R K) x) < 1
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: case right
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : v.intValuation x * v.intValuation inv✝ = 1
⊢ v.intValuation x * v.intValuation inv✝ ≤ v.intValuation x * 1

Tactic:
]

Goal state after:
case right
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : v.intValuation x * v.intValuation inv✝ = 1
⊢ v.intValuation x * v.intValuation inv✝ ≤ v.intValuation x * 1
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
n : ℕ
x : Rˣ
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
⊢ IsLocalization.mk' R' (r * (↑t * ↑s) - ↑t * r * ↑s) (s * (t * s)) = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
⊢ IsLocalization.mk' R' (r * (↑t * ↑s) - ↑t * r * ↑s) (s * (t * s)) = 0
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
a✝ b✝ : Kˣ ⧸ (powMonoidHom n).range
hx : a✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
hy : b✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
v : HeightOneSpectrum R
hv : v ∉ S
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: case h.refine_2
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' R' (↑t * r) 1 * IsLocalization.mk' R' 1 (t * s)
⊢ IsLocalization.mk' R' (↑t * r) 1 * IsLocalization.mk' R' 1 (t * s) ∈ p

Tactic:
]

Goal state after:
case h.refine_2
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' R' (↑t * r) 1 * IsLocalization.mk' R' 1 (t * s)
⊢ IsLocalization.mk' R' (↑t * r) 1 * IsLocalization.mk' R' 1 (t * s) ∈ p
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x✝¹ : HeightOneSpectrum R
x✝ : x✝¹ ∉ S
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x✝¹ : HeightOneSpectrum R
x✝ : x✝¹ ∉ S
⊢ (x✝¹.valuationOfNeZeroMod n) 1 = 1

Tactic:
by rw [map_one]

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x✝ : Kˣ ⧸ (powMonoidHom n).range
hx : x✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
v : HeightOneSpectrum R
hv : v ∉ S
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: case h.refine_2
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' R' (↑t * r) 1 * IsLocalization.mk' R' 1 (t * s)
⊢ ↑t * r ∈ (⊥.colon {x}).radical

Tactic:
]

Goal state after:
case h.refine_2
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' R' (↑t * r) 1 * IsLocalization.mk' R' 1 (t * s)
⊢ ↑t * r ∈ (⊥.colon {x}).radical
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
h : Function.Injective ⇑(DistribSMul.toLinearMap R M r)
⊢ map ((LinearMap.lsmul R M) r) ⊤ ⊓ N ≤ map ((LinearMap.lsmul R M) r) N ↔ r • ⊤ ⊓ N ≤ r • N

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
h : Function.Injective ⇑(DistribSMul.toLinearMap R M r)
⊢ map ((LinearMap.lsmul R M) r) ⊤ ⊓ N ≤ map ((LinearMap.lsmul R M) r) N ↔ r • ⊤ ⊓ N ≤ r • N
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: case h
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' R' (↑t * r) 1 * IsLocalization.mk' R' 1 (t * s)
hn : 0 < n
⊢ ↑t ^ n ∈ ⊥.colon {r ^ n • x}

Tactic:
]

Goal state after:
case h
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
this : IsLocalization.mk' R' r s = IsLocalization.mk' R' (↑t * r) 1 * IsLocalization.mk' R' 1 (t * s)
hn : 0 < n
⊢ ↑t ^ n ∈ ⊥.colon {r ^ n • x}
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M''
M''' : Type u_6
inst✝¹ : AddCommGroup M'''
inst✝ : Module R M'''
r : R
f₁ : M →ₗ[R] M'
f₂ : M' →ₗ[R] M''
f₃ : M'' →ₗ[R] M'''
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h : IsSMulRegular M''' r
this : IsSMulRegular (M'' ⧸ f₂.range) r
⊢ r • ⊤ ⊓ f₂.range ≤ r • f₂.range

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M''
M''' : Type u_6
inst✝¹ : AddCommGroup M'''
inst✝ : Module R M'''
r : R
f₁ : M →ₗ[R] M'
f₂ : M' →ₗ[R] M''
f₃ : M'' →ₗ[R] M'''
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h : IsSMulRegular M''' r
this : IsSMulRegular (M'' ⧸ f₂.range) r
⊢ r • ⊤ ⊓ f₂.range ≤ r • f₂.range
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: case mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  (powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    (Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n =
    (algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑({ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n)⁻¹ =
    (algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range

Tactic:
]

Goal state after:
case mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  (powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    (Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n =
    (algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑({ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n)⁻¹ =
    (algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range