-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem adjust_f {w₁ : InfinitePlace K} (B : ℝ≥0) (hf : ∀ w, w ≠ w₁ → f w ≠ 0) :
    ∃ g : InfinitePlace K → ℝ≥0, (∀ w, w ≠ w₁ → g w = f w) ∧ ∏ w, (g w) ^ mult w = B

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ↑(if w₁.IsReal then 1 else 2) ≠ 0

Tactic:
split_ifs <;> norm_num

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
w : InfinitePlace K
hw : w ∈ Finset.univ.erase w₁
⊢ Function.update f w₁ ((B * S⁻¹) ^ (↑w₁.mult)⁻¹) w ^ w.mult = ?m.45999 w

Tactic:
rw [Function.update_of_ne (Finset.ne_of_mem_erase hw)]

Result:
no goals

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ S ≠ 0

Tactic:
rw [Finset.prod_ne_zero_iff]

Result:
case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ∀ a ∈ Finset.univ.erase w₁, f a ^ a.mult ≠ 0

Proof state:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
⊢ ∃ g, (∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w) ∧ ∏ w : InfinitePlace K, g w ^ w.mult = B

Tactic:
let S := ∏ w ∈ Finset.univ.erase w₁, (f w) ^ mult w

Result:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ∃ g, (∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w) ∧ ∏ w : InfinitePlace K, g w ^ w.mult = B

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ∀ a ∈ Finset.univ.erase w₁, f a ^ a.mult ≠ 0

Tactic:
exact fun w hw => pow_ne_zero _ (hf w (Finset.ne_of_mem_erase hw))

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ∃ g, (∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w) ∧ ∏ w : InfinitePlace K, g w ^ w.mult = B

Tactic:
refine ⟨Function.update f w₁ ((B * S⁻¹) ^ (mult w₁ : ℝ)⁻¹), ?_, ?_⟩

Result:
case refine_1
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ∀ (w : InfinitePlace K), w ≠ w₁ → Function.update f w₁ ((B * S⁻¹) ^ (↑w₁.mult)⁻¹) w = f w

case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ∏ w : InfinitePlace K, Function.update f w₁ ((B * S⁻¹) ^ (↑w₁.mult)⁻¹) w ^ w.mult = B

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ∏ w : InfinitePlace K, Function.update f w₁ ((B * S⁻¹) ^ (↑w₁.mult)⁻¹) w ^ w.mult = B

Tactic:
rw [← Finset.mul_prod_erase Finset.univ _ (Finset.mem_univ w₁), Function.update_self,
  Finset.prod_congr rfl fun w hw => by rw [Function.update_of_ne (Finset.ne_of_mem_erase hw)],
  ← NNReal.rpow_natCast, ← NNReal.rpow_mul, inv_mul_cancel₀, NNReal.rpow_one, mul_assoc,
  inv_mul_cancel₀, mul_one]

Result:
case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ S ≠ 0

case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ↑w₁.mult ≠ 0

Proof state:
case refine_1
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ∀ (w : InfinitePlace K), w ≠ w₁ → Function.update f w₁ ((B * S⁻¹) ^ (↑w₁.mult)⁻¹) w = f w

Tactic:
exact fun w hw => Function.update_of_ne hw _ f

Result:
no goals

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ↑w₁.mult ≠ 0

Tactic:
rw [mult]

Result:
case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ↑(if w₁.IsReal then 1 else 2) ≠ 0