-- Mathlib/NumberTheory/NumberField/FinitePlaces.lean
theorem mk_eq_iff {v₁ v₂ : HeightOneSpectrum (𝓞 K)} : mk v₁ = mk v₂ ↔ v₁ = v₂

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
H : ∀ x ∈ v₁.asIdeal, x ∈ v₂.asIdeal
⊢ False

Tactic:
exact h <| HeightOneSpectrum.ext_iff.mpr <| IsMaximal.eq_of_le (isMaximal v₁) IsPrime.ne_top' H

Result:
no goals

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : x ∈ v₁.asIdeal
hx2 : x ∉ v₂.asIdeal
⊢ ‖(embedding v₁) ↑x‖ ≠ ‖(embedding v₂) ↑x‖

Tactic:
rw [← norm_lt_one_iff_mem] at hx1

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : ‖(embedding v₁) ↑x‖ < 1
hx2 : x ∉ v₂.asIdeal
⊢ ‖(embedding v₁) ↑x‖ ≠ ‖(embedding v₂) ↑x‖

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : ‖(embedding v₁) ↑x‖ < 1
hx2 : x ∉ v₂.asIdeal
⊢ ‖(embedding v₁) ↑x‖ ≠ ‖(embedding v₂) ↑x‖

Tactic:
rw [← norm_eq_one_iff_not_mem] at hx2

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : ‖(embedding v₁) ↑x‖ < 1
hx2 : ‖(embedding v₂) ↑x‖ = 1
⊢ ‖(embedding v₁) ↑x‖ ≠ ‖(embedding v₂) ↑x‖

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
⊢ ∃ a, (mk v₁) a ≠ (mk v₂) a

Tactic:
have ⟨x, hx1, hx2⟩ : ∃ x : 𝓞 K, x ∈ v₁.asIdeal ∧ x ∉ v₂.asIdeal := by
  by_contra! H
  exact h <| HeightOneSpectrum.ext_iff.mpr <| IsMaximal.eq_of_le (isMaximal v₁) IsPrime.ne_top' H

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : x ∈ v₁.asIdeal
hx2 : x ∉ v₂.asIdeal
⊢ ∃ a, (mk v₁) a ≠ (mk v₂) a

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
⊢ mk v₁ = mk v₂ ↔ v₁ = v₂

Tactic:
refine ⟨?_, fun a ↦ by rw [a]⟩

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
⊢ mk v₁ = mk v₂ → v₁ = v₂

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
⊢ mk v₁ = mk v₂ → v₁ = v₂

Tactic:
contrapose!

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
⊢ v₁ ≠ v₂ → mk v₁ ≠ mk v₂

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
⊢ mk v₁ ≠ mk v₂

Tactic:
rw [DFunLike.ne_iff]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
⊢ ∃ a, (mk v₁) a ≠ (mk v₂) a

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : x ∈ v₁.asIdeal
hx2 : x ∉ v₂.asIdeal
⊢ ∃ a, (mk v₁) a ≠ (mk v₂) a

Tactic:
use x

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : x ∈ v₁.asIdeal
hx2 : x ∉ v₂.asIdeal
⊢ (mk v₁) ↑x ≠ (mk v₂) ↑x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
a : v₁ = v₂
⊢ mk v₁ = mk v₂

Tactic:
rw [a]

Result:
no goals

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : ‖(embedding v₁) ↑x‖ < 1
hx2 : ‖(embedding v₂) ↑x‖ = 1
⊢ ‖(embedding v₁) ↑x‖ ≠ ‖(embedding v₂) ↑x‖

Tactic:
linarith

Result:
no goals

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : x ∈ v₁.asIdeal
hx2 : x ∉ v₂.asIdeal
⊢ (mk v₁) ↑x ≠ (mk v₂) ↑x

Tactic:
simp only [mk_apply]

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
x : 𝓞 K
hx1 : x ∈ v₁.asIdeal
hx2 : x ∉ v₂.asIdeal
⊢ ‖(embedding v₁) ↑x‖ ≠ ‖(embedding v₂) ↑x‖

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
⊢ v₁ ≠ v₂ → mk v₁ ≠ mk v₂

Tactic:
intro h

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
⊢ mk v₁ ≠ mk v₂

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
⊢ ∃ x ∈ v₁.asIdeal, x ∉ v₂.asIdeal

Tactic:
by_contra! H

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
h : v₁ ≠ v₂
H : ∀ x ∈ v₁.asIdeal, x ∈ v₂.asIdeal
⊢ False