-- Mathlib/NumberTheory/NumberField/FinitePlaces.lean
theorem mulSupport_finite_int {x : 𝓞 K} (h_x_nezero : x ≠ 0) :
    (Function.mulSupport fun w : FinitePlace K ↦ w x).Finite

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this : ∀ (w : FinitePlace K), w ↑x ≠ 1 ↔ w ↑x < 1
⊢ {x_1 | x_1.maximalIdeal.asIdeal ∣ span {x}}.Finite

Tactic:
have h : {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span {x}}.Finite := by
  apply Ideal.finite_factors
  simp only [Submodule.zero_eq_bot, ne_eq, span_singleton_eq_bot, h_x_nezero, not_false_eq_true]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this : ∀ (w : FinitePlace K), w ↑x ≠ 1 ↔ w ↑x < 1
h : {v | v.asIdeal ∣ span {x}}.Finite
⊢ {x_1 | x_1.maximalIdeal.asIdeal ∣ span {x}}.Finite

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this : ∀ (w : FinitePlace K), w ↑x ≠ 1 ↔ w ↑x < 1
h : {v | v.asIdeal ∣ span {x}}.Finite
h_inj : Set.InjOn maximalIdeal {w | w.maximalIdeal.asIdeal ∣ span {x}}
⊢ {x_1 | x_1.maximalIdeal.asIdeal ∣ span {x}}.Finite

Tactic:
refine (h.subset ?_).of_finite_image h_inj

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this : ∀ (w : FinitePlace K), w ↑x ≠ 1 ↔ w ↑x < 1
h : {v | v.asIdeal ∣ span {x}}.Finite
h_inj : Set.InjOn maximalIdeal {w | w.maximalIdeal.asIdeal ∣ span {x}}
⊢ maximalIdeal '' {x_1 | x_1.maximalIdeal.asIdeal ∣ span {x}} ⊆ {v | v.asIdeal ∣ span {x}}

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this : ∀ (w : FinitePlace K), w ↑x ≠ 1 ↔ w ↑x < 1
⊢ (Function.mulSupport fun w => w ↑x).Finite

Tactic:
simp_rw [Function.mulSupport, this, ← norm_embedding_eq, norm_lt_one_iff_mem,
  ← Ideal.dvd_span_singleton]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this : ∀ (w : FinitePlace K), w ↑x ≠ 1 ↔ w ↑x < 1
⊢ {x_1 | x_1.maximalIdeal.asIdeal ∣ span {x}}.Finite

Proof state:
case hI
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this : ∀ (w : FinitePlace K), w ↑x ≠ 1 ↔ w ↑x < 1
⊢ span {x} ≠ 0

Tactic:
simp only [Submodule.zero_eq_bot, ne_eq, span_singleton_eq_bot, h_x_nezero, not_false_eq_true]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this : ∀ (w : FinitePlace K), w ↑x ≠ 1 ↔ w ↑x < 1
h : {v | v.asIdeal ∣ span {x}}.Finite
h_inj : Set.InjOn maximalIdeal {w | w.maximalIdeal.asIdeal ∣ span {x}}
⊢ maximalIdeal '' {x_1 | x_1.maximalIdeal.asIdeal ∣ span {x}} ⊆ {v | v.asIdeal ∣ span {x}}

Tactic:
simp only [dvd_span_singleton, Set.image_subset_iff, Set.preimage_setOf_eq, subset_refl]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
⊢ (Function.mulSupport fun w => w ↑x).Finite

Tactic:
have (w : FinitePlace K) : w x ≠ 1 ↔ w x < 1 :=
  ne_iff_lt_iff_le.mpr <| norm_embedding_eq w x ▸ norm_le_one w.maximalIdeal x

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this : ∀ (w : FinitePlace K), w ↑x ≠ 1 ↔ w ↑x < 1
⊢ (Function.mulSupport fun w => w ↑x).Finite

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this : ∀ (w : FinitePlace K), w ↑x ≠ 1 ↔ w ↑x < 1
h : {v | v.asIdeal ∣ span {x}}.Finite
⊢ {x_1 | x_1.maximalIdeal.asIdeal ∣ span {x}}.Finite

Tactic:
have h_inj : Set.InjOn FinitePlace.maximalIdeal {w | w.maximalIdeal.asIdeal ∣ span {x}} :=
  Function.Injective.injOn maximalIdeal_injective

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this : ∀ (w : FinitePlace K), w ↑x ≠ 1 ↔ w ↑x < 1
h : {v | v.asIdeal ∣ span {x}}.Finite
h_inj : Set.InjOn maximalIdeal {w | w.maximalIdeal.asIdeal ∣ span {x}}
⊢ {x_1 | x_1.maximalIdeal.asIdeal ∣ span {x}}.Finite

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this : ∀ (w : FinitePlace K), w ↑x ≠ 1 ↔ w ↑x < 1
⊢ {v | v.asIdeal ∣ span {x}}.Finite

Tactic:
apply Ideal.finite_factors

Result:
case hI
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
this : ∀ (w : FinitePlace K), w ↑x ≠ 1 ↔ w ↑x < 1
⊢ span {x} ≠ 0