-- Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean
theorem valuation_ker_eq :
    valuation.ker = K⟮(∅ : Set <| HeightOneSpectrum R),n⟯.subgroupOf (K⟮S,n⟯)

Proof state:
case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
hx' : ⟨val✝, hx⟩ ∈ valuation.ker
v : HeightOneSpectrum R
x✝ : v ∉ ∅
hv : v ∉ S
⊢ (v.valuationOfNeZeroMod n) (selmerGroup.subtype ⟨val✝, hx⟩) = 1

Tactic:
exact hx v hv

Result:
no goals

Proof state:
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
hx' : ⟨val✝, hx⟩ ∈ valuation.ker
v : HeightOneSpectrum R
x✝ : v ∉ ∅
hv : v ∈ S
⊢ (v.valuationOfNeZeroMod n) (selmerGroup.subtype ⟨val✝, hx⟩) = 1

Tactic:
exact congr_fun hx' ⟨v, hv⟩

Result:
no goals

Proof state:
case h.mk.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
hx' : ⟨val✝, hx⟩ ∈ valuation.ker
v : HeightOneSpectrum R
x✝ : v ∉ ∅
⊢ (v.valuationOfNeZeroMod n) (selmerGroup.subtype ⟨val✝, hx⟩) = 1

Tactic:
by_cases hv : v ∈ S

Result:
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
hx' : ⟨val✝, hx⟩ ∈ valuation.ker
v : HeightOneSpectrum R
x✝ : v ∉ ∅
hv : v ∈ S
⊢ (v.valuationOfNeZeroMod n) (selmerGroup.subtype ⟨val✝, hx⟩) = 1

case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
hx' : ⟨val✝, hx⟩ ∈ valuation.ker
v : HeightOneSpectrum R
x✝ : v ∉ ∅
hv : v ∉ S
⊢ (v.valuationOfNeZeroMod n) (selmerGroup.subtype ⟨val✝, hx⟩) = 1

Proof state:
case h.mk.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
⊢ ⟨val✝, hx⟩ ∈ valuation.ker → ⟨val✝, hx⟩ ∈ selmerGroup.subgroupOf selmerGroup

Tactic:
intro hx' v _

Result:
case h.mk.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
hx' : ⟨val✝, hx⟩ ∈ valuation.ker
v : HeightOneSpectrum R
x✝ : v ∉ ∅
⊢ (v.valuationOfNeZeroMod n) (selmerGroup.subtype ⟨val✝, hx⟩) = 1

Proof state:
case h.mk.mpr
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
⊢ ⟨val✝, hx⟩ ∈ selmerGroup.subgroupOf selmerGroup → ⟨val✝, hx⟩ ∈ valuation.ker

Tactic:
exact fun hx' => funext fun v => hx' v <| Set.not_mem_empty v

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
⊢ valuation.ker = selmerGroup.subgroupOf selmerGroup

Tactic:
ext ⟨_, hx⟩

Result:
case h.mk
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
⊢ ⟨val✝, hx⟩ ∈ valuation.ker ↔ ⟨val✝, hx⟩ ∈ selmerGroup.subgroupOf selmerGroup

Proof state:
case h.mk
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
⊢ ⟨val✝, hx⟩ ∈ valuation.ker ↔ ⟨val✝, hx⟩ ∈ selmerGroup.subgroupOf selmerGroup

Tactic:
constructor

Result:
case h.mk.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
⊢ ⟨val✝, hx⟩ ∈ valuation.ker → ⟨val✝, hx⟩ ∈ selmerGroup.subgroupOf selmerGroup

case h.mk.mpr
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
⊢ ⟨val✝, hx⟩ ∈ selmerGroup.subgroupOf selmerGroup → ⟨val✝, hx⟩ ∈ valuation.ker