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

Proof state:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb : b ∈ nonZeroDivisors (𝓞 K)
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
⊢ (Function.mulSupport fun w => w ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b)).Finite

Tactic:
simp_all only [ne_eq, div_eq_zero_iff, FaithfulSMul.algebraMap_eq_zero_iff, not_or, map_div₀]

Result:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb : b ∈ nonZeroDivisors (𝓞 K)
h_x_nezero : ¬a = 0 ∧ ¬b = 0
⊢ (Function.mulSupport fun w => w ((algebraMap (𝓞 K) K) a) / w ((algebraMap (𝓞 K) K) b)).Finite

Proof state:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb✝ : b ∈ nonZeroDivisors (𝓞 K)
ha : ¬a = 0
hb : ¬b = 0
w : FinitePlace K
⊢ w ↑a = 1 ∧ w ↑b = 1 → w ↑a / w ↑b = 1

Tactic:
simp +contextual only [ne_eq, one_ne_zero, not_false_eq_true, div_self, implies_true]

Result:
no goals

Proof state:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb✝ : b ∈ nonZeroDivisors (𝓞 K)
ha : ¬a = 0
hb : ¬b = 0
⊢ (Function.mulSupport fun w => w ((algebraMap (𝓞 K) K) a) / w ((algebraMap (𝓞 K) K) b)).Finite

Tactic:
simp_rw [← RingOfIntegers.coe_eq_algebraMap]

Result:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb✝ : b ∈ nonZeroDivisors (𝓞 K)
ha : ¬a = 0
hb : ¬b = 0
⊢ (Function.mulSupport fun w => w ↑a / w ↑b).Finite

Proof state:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb✝ : b ∈ nonZeroDivisors (𝓞 K)
ha : ¬a = 0
hb : ¬b = 0
⊢ (Function.mulSupport fun w => w ↑a / w ↑b) ⊆ (Function.mulSupport fun w => w ↑a) ∪ Function.mulSupport fun w => w ↑b

Tactic:
intro w

Result:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb✝ : b ∈ nonZeroDivisors (𝓞 K)
ha : ¬a = 0
hb : ¬b = 0
w : FinitePlace K
⊢ (w ∈ Function.mulSupport fun w => w ↑a / w ↑b) →
    w ∈ (Function.mulSupport fun w => w ↑a) ∪ Function.mulSupport fun w => w ↑b

Proof state:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb : b ∈ nonZeroDivisors (𝓞 K)
h_x_nezero : ¬a = 0 ∧ ¬b = 0
⊢ (Function.mulSupport fun w => w ((algebraMap (𝓞 K) K) a) / w ((algebraMap (𝓞 K) K) b)).Finite

Tactic:
obtain ⟨ha, hb⟩ := h_x_nezero

Result:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb✝ : b ∈ nonZeroDivisors (𝓞 K)
ha : ¬a = 0
hb : ¬b = 0
⊢ (Function.mulSupport fun w => w ((algebraMap (𝓞 K) K) a) / w ((algebraMap (𝓞 K) K) b)).Finite

Proof state:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb✝ : b ∈ nonZeroDivisors (𝓞 K)
ha : ¬a = 0
hb : ¬b = 0
⊢ (Function.mulSupport fun w => w ↑a / w ↑b).Finite

Tactic:
apply ((mulSupport_finite_int ha).union (mulSupport_finite_int hb)).subset

Result:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb✝ : b ∈ nonZeroDivisors (𝓞 K)
ha : ¬a = 0
hb : ¬b = 0
⊢ (Function.mulSupport fun w => w ↑a / w ↑b) ⊆ (Function.mulSupport fun w => w ↑a) ∪ Function.mulSupport fun w => w ↑b

Proof state:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb✝ : b ∈ nonZeroDivisors (𝓞 K)
ha : ¬a = 0
hb : ¬b = 0
w : FinitePlace K
⊢ ¬w ↑a / w ↑b = 1 → ¬w ↑a = 1 ∨ ¬w ↑b = 1

Tactic:
contrapose!

Result:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb✝ : b ∈ nonZeroDivisors (𝓞 K)
ha : ¬a = 0
hb : ¬b = 0
w : FinitePlace K
⊢ w ↑a = 1 ∧ w ↑b = 1 → w ↑a / w ↑b = 1

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:
rcases IsFractionRing.div_surjective (A := 𝓞 K) x with ⟨a, b, hb, rfl⟩

Result:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb : b ∈ nonZeroDivisors (𝓞 K)
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
⊢ (Function.mulSupport fun w => w ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b)).Finite

Proof state:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb✝ : b ∈ nonZeroDivisors (𝓞 K)
ha : ¬a = 0
hb : ¬b = 0
w : FinitePlace K
⊢ (w ∈ Function.mulSupport fun w => w ↑a / w ↑b) →
    w ∈ (Function.mulSupport fun w => w ↑a) ∪ Function.mulSupport fun w => w ↑b

Tactic:
simp only [Function.mem_mulSupport, ne_eq, Set.mem_union]

Result:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb✝ : b ∈ nonZeroDivisors (𝓞 K)
ha : ¬a = 0
hb : ¬b = 0
w : FinitePlace K
⊢ ¬w ↑a / w ↑b = 1 → ¬w ↑a = 1 ∨ ¬w ↑b = 1