[GOAL]
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
⊢ (∑ x in s, f x) ^ (n + 1) / ↑(card s) ^ n ≤ ∑ x in s, f x ^ (n + 1)
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | hs)
[GOAL]
case inl
ι : Type u
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ ∅ → 0 ≤ f a
⊢ (∑ x in ∅, f x) ^ (n + 1) / ↑(card ∅) ^ n ≤ ∑ x in ∅, f x ^ (n + 1)
[PROOFSTEP]
simp_rw [Finset.sum_empty, zero_pow' _ (Nat.succ_ne_zero n), zero_div]
[GOAL]
case inl
ι : Type u
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ ∅ → 0 ≤ f a
⊢ 0 ≤ 0
[PROOFSTEP]
rfl
[GOAL]
case inr
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
⊢ (∑ x in s, f x) ^ (n + 1) / ↑(card s) ^ n ≤ ∑ x in s, f x ^ (n + 1)
[PROOFSTEP]
have hs0 : 0 < (s.card : ℝ) := Nat.cast_pos.2 hs.card_pos
[GOAL]
case inr
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
⊢ (∑ x in s, f x) ^ (n + 1) / ↑(card s) ^ n ≤ ∑ x in s, f x ^ (n + 1)
[PROOFSTEP]
suffices (∑ x in s, f x / s.card) ^ (n + 1) ≤ ∑ x in s, f x ^ (n + 1) / s.card by
  rwa [← Finset.sum_div, ← Finset.sum_div, div_pow, pow_succ' (s.card : ℝ), ← div_div, div_le_iff hs0, div_mul,
    div_self hs0.ne', div_one] at this
[GOAL]
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
this : (∑ x in s, f x / ↑(card s)) ^ (n + 1) ≤ ∑ x in s, f x ^ (n + 1) / ↑(card s)
⊢ (∑ x in s, f x) ^ (n + 1) / ↑(card s) ^ n ≤ ∑ x in s, f x ^ (n + 1)
[PROOFSTEP]
rwa [← Finset.sum_div, ← Finset.sum_div, div_pow, pow_succ' (s.card : ℝ), ← div_div, div_le_iff hs0, div_mul,
  div_self hs0.ne', div_one] at this
[GOAL]
case inr
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
⊢ (∑ x in s, f x / ↑(card s)) ^ (n + 1) ≤ ∑ x in s, f x ^ (n + 1) / ↑(card s)
[PROOFSTEP]
have :=
  @ConvexOn.map_sum_le ℝ ℝ ℝ ι _ _ _ _ _ _ (Set.Ici 0) (fun x => x ^ (n + 1)) s (fun _ => 1 / s.card) ((↑) ∘ f)
    (convexOn_pow (n + 1)) ?_ ?_ fun i hi => Set.mem_Ici.2 (hf i hi)
[GOAL]
case inr.refine_3
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
this :
  (fun x => x ^ (n + 1)) (∑ i in s, (fun x => 1 / ↑(card s)) i • ((fun x => x) ∘ f) i) ≤
    ∑ i in s, (fun x => 1 / ↑(card s)) i • (fun x => x ^ (n + 1)) (((fun x => x) ∘ f) i)
⊢ (∑ x in s, f x / ↑(card s)) ^ (n + 1) ≤ ∑ x in s, f x ^ (n + 1) / ↑(card s)
[PROOFSTEP]
simpa only [inv_mul_eq_div, one_div, Algebra.id.smul_eq_mul] using this
[GOAL]
case inr.refine_1
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
⊢ ∀ (i : ι), i ∈ s → 0 ≤ (fun x => 1 / ↑(card s)) i
[PROOFSTEP]
simp only [one_div, inv_nonneg, Nat.cast_nonneg, imp_true_iff]
[GOAL]
case inr.refine_2
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
⊢ ∑ i in s, (fun x => 1 / ↑(card s)) i = 1
[PROOFSTEP]
simpa only [one_div, Finset.sum_const, nsmul_eq_mul] using mul_inv_cancel hs0.ne'
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
⊢ ∑ i in s, w i * z i ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
[PROOFSTEP]
have : 0 < p := by positivity
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
⊢ 0 < p
[PROOFSTEP]
positivity
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ ∑ i in s, w i * z i ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
[PROOFSTEP]
rw [← rpow_le_rpow_iff _ _ this, ← rpow_mul, one_div_mul_cancel (ne_of_gt this), rpow_one]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i ^ p
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
[PROOFSTEP]
exact rpow_arith_mean_le_arith_mean_rpow s w z hw hw' hz hp
[GOAL]
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i ^ p
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
[PROOFSTEP]
all_goals
  apply_rules [sum_nonneg, rpow_nonneg_of_nonneg]
  intro i hi
  apply_rules [mul_nonneg, rpow_nonneg_of_nonneg, hw i hi, hz i hi]
[GOAL]
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
apply_rules [sum_nonneg, rpow_nonneg_of_nonneg]
[GOAL]
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hw'_symm : 1 = ∑ i in s, w i
⊢ ∀ (i : ι), i ∈ s → 0 ≤ w i * z i ^ p
[PROOFSTEP]
intro i hi
[GOAL]
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hw'_symm : 1 = ∑ i in s, w i
i : ι
hi : i ∈ s
⊢ 0 ≤ w i * z i ^ p
[PROOFSTEP]
apply_rules [mul_nonneg, rpow_nonneg_of_nonneg, hw i hi, hz i hi]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i
[PROOFSTEP]
apply_rules [sum_nonneg, rpow_nonneg_of_nonneg]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hw'_symm : 1 = ∑ i in s, w i
⊢ ∀ (i : ι), i ∈ s → 0 ≤ w i * z i
[PROOFSTEP]
intro i hi
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hw'_symm : 1 = ∑ i in s, w i
i : ι
hi : i ∈ s
⊢ 0 ≤ w i * z i
[PROOFSTEP]
apply_rules [mul_nonneg, rpow_nonneg_of_nonneg, hw i hi, hz i hi]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
[PROOFSTEP]
apply_rules [sum_nonneg, rpow_nonneg_of_nonneg]
[GOAL]
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hw'_symm : 1 = ∑ i in s, w i
⊢ ∀ (i : ι), i ∈ s → 0 ≤ w i * z i ^ p
[PROOFSTEP]
intro i hi
[GOAL]
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hw'_symm : 1 = ∑ i in s, w i
i : ι
hi : i ∈ s
⊢ 0 ≤ w i * z i ^ p
[PROOFSTEP]
apply_rules [mul_nonneg, rpow_nonneg_of_nonneg, hw i hi, hz i hi]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : ∑ i in s, w i = 1
n : ℕ
⊢ (∑ i in s, w i * z i) ^ n ≤ ∑ i in s, w i * z i ^ n
[PROOFSTEP]
exact_mod_cast
  Real.pow_arith_mean_le_arith_mean_pow s _ _ (fun i _ => (w i).coe_nonneg) (by exact_mod_cast hw')
    (fun i _ => (z i).coe_nonneg) n
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : ∑ i in s, w i = 1
n : ℕ
⊢ ∑ i in s, ↑(w i) = 1
[PROOFSTEP]
exact_mod_cast hw'
[GOAL]
ι : Type u
s : Finset ι
f : ι → ℝ≥0
n : ℕ
⊢ ↑((∑ x in s, f x) ^ (n + 1)) / ↑(card s) ^ n ≤ ↑(∑ x in s, f x ^ (n + 1))
[PROOFSTEP]
simpa only [← NNReal.coe_le_coe, NNReal.coe_sum, Nonneg.coe_div, NNReal.coe_pow] using
  @Real.pow_sum_div_card_le_sum_pow ι s (((↑) : ℝ≥0 → ℝ) ∘ f) n fun _ _ => NNReal.coe_nonneg _
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
exact_mod_cast
  Real.rpow_arith_mean_le_arith_mean_rpow s _ _ (fun i _ => (w i).coe_nonneg) (by exact_mod_cast hw')
    (fun i _ => (z i).coe_nonneg) hp
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i in s, ↑(w i) = 1
[PROOFSTEP]
exact_mod_cast hw'
[GOAL]
ι : Type u
s : Finset ι
w₁ w₂ z₁ z₂ : ℝ≥0
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
[PROOFSTEP]
have h := rpow_arith_mean_le_arith_mean_rpow univ ![w₁, w₂] ![z₁, z₂] ?_ hp
[GOAL]
case refine_2
ι : Type u
s : Finset ι
w₁ w₂ z₁ z₂ : ℝ≥0
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
h :
  (∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons w₁ ![w₂] i * Matrix.vecCons z₁ ![z₂] i) ^ p ≤
    ∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons w₁ ![w₂] i * Matrix.vecCons z₁ ![z₂] i ^ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
[PROOFSTEP]
simpa [Fin.sum_univ_succ] using h
[GOAL]
case refine_1
ι : Type u
s : Finset ι
w₁ w₂ z₁ z₂ : ℝ≥0
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons w₁ ![w₂] i = 1
[PROOFSTEP]
simp [hw', Fin.sum_univ_succ]
[GOAL]
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
[PROOFSTEP]
rcases eq_or_lt_of_le hp with (rfl | h'p)
[GOAL]
case inl
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0
hp : 1 ≤ 1
⊢ (z₁ + z₂) ^ 1 ≤ 2 ^ (1 - 1) * (z₁ ^ 1 + z₂ ^ 1)
[PROOFSTEP]
simp only [rpow_one, sub_self, rpow_zero, one_mul]
[GOAL]
case inl
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0
hp : 1 ≤ 1
⊢ z₁ + z₂ ≤ z₁ + z₂
[PROOFSTEP]
rfl
[GOAL]
case inr
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
[PROOFSTEP]
convert rpow_arith_mean_le_arith_mean2_rpow (1 / 2) (1 / 2) (2 * z₁) (2 * z₂) (add_halves 1) hp using 1
[GOAL]
case h.e'_3
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ (z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p
[PROOFSTEP]
simp only [one_div, inv_mul_cancel_left₀, Ne.def, mul_eq_zero, two_ne_zero, one_ne_zero, not_false_iff]
[GOAL]
case h.e'_4
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
[PROOFSTEP]
have A : p - 1 ≠ 0 := ne_of_gt (sub_pos.2 h'p)
[GOAL]
case h.e'_4
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
A : p - 1 ≠ 0
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
[PROOFSTEP]
simp only [mul_rpow, rpow_sub' _ A, div_eq_inv_mul, rpow_one, mul_one]
[GOAL]
case h.e'_4
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
A : p - 1 ≠ 0
⊢ 2⁻¹ * 2 ^ p * (z₁ ^ p + z₂ ^ p) = 2⁻¹ * (2 ^ p * z₁ ^ p) + 2⁻¹ * (2 ^ p * z₂ ^ p)
[PROOFSTEP]
ring
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i in s, w i * z i ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
[PROOFSTEP]
exact_mod_cast
  Real.arith_mean_le_rpow_mean s _ _ (fun i _ => (w i).coe_nonneg) (by exact_mod_cast hw') (fun i _ => (z i).coe_nonneg)
    hp
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i in s, ↑(w i) = 1
[PROOFSTEP]
exact_mod_cast hw'
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ 1
[PROOFSTEP]
have h_le_one : ∀ x : ℝ≥0, x ≤ 1 → x ^ p ≤ x := fun x hx => rpow_le_self_of_le_one hx hp1
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ (x : ℝ≥0), x ≤ 1 → x ^ p ≤ x
⊢ a ^ p + b ^ p ≤ 1
[PROOFSTEP]
have ha : a ≤ 1 := (self_le_add_right a b).trans hab
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ (x : ℝ≥0), x ≤ 1 → x ^ p ≤ x
ha : a ≤ 1
⊢ a ^ p + b ^ p ≤ 1
[PROOFSTEP]
have hb : b ≤ 1 := (self_le_add_left b a).trans hab
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ (x : ℝ≥0), x ≤ 1 → x ^ p ≤ x
ha : a ≤ 1
hb : b ≤ 1
⊢ a ^ p + b ^ p ≤ 1
[PROOFSTEP]
exact (add_le_add (h_le_one a ha) (h_le_one b hb)).trans hab
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
have hp_pos : 0 < p := by positivity
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ 0 < p
[PROOFSTEP]
positivity
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
by_cases h_zero : a + b = 0
[GOAL]
case pos
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : a + b = 0
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
simp [add_eq_zero_iff.mp h_zero, hp_pos.ne']
[GOAL]
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
have h_nonzero : ¬(a = 0 ∧ b = 0) := by rwa [add_eq_zero_iff] at h_zero
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
⊢ ¬(a = 0 ∧ b = 0)
[PROOFSTEP]
rwa [add_eq_zero_iff] at h_zero
[GOAL]
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
have h_add : a / (a + b) + b / (a + b) = 1 := by rw [div_add_div_same, div_self h_zero]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
⊢ a / (a + b) + b / (a + b) = 1
[PROOFSTEP]
rw [div_add_div_same, div_self h_zero]
[GOAL]
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
have h := add_rpow_le_one_of_add_le_one (a / (a + b)) (b / (a + b)) h_add.le hp1
[GOAL]
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : (a / (a + b)) ^ p + (b / (a + b)) ^ p ≤ 1
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
rw [div_rpow a (a + b), div_rpow b (a + b)] at h
[GOAL]
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
have hab_0 : (a + b) ^ p ≠ 0 := by simp [hp_pos, h_nonzero]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
⊢ (a + b) ^ p ≠ 0
[PROOFSTEP]
simp [hp_pos, h_nonzero]
[GOAL]
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
have hab_0' : 0 < (a + b) ^ p := zero_lt_iff.mpr hab_0
[GOAL]
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
hab_0' : 0 < (a + b) ^ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
have h_mul : (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p :=
  by
  nth_rw 4 [← mul_one ((a + b) ^ p)]
  exact (mul_le_mul_left hab_0').mpr h
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
hab_0' : 0 < (a + b) ^ p
⊢ (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p
[PROOFSTEP]
nth_rw 4 [← mul_one ((a + b) ^ p)]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
hab_0' : 0 < (a + b) ^ p
⊢ (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p * 1
[PROOFSTEP]
exact (mul_le_mul_left hab_0').mpr h
[GOAL]
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
hab_0' : 0 < (a + b) ^ p
h_mul : (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
rwa [div_eq_mul_inv, div_eq_mul_inv, mul_add, mul_comm (a ^ p), mul_comm (b ^ p), ← mul_assoc, ← mul_assoc,
  mul_inv_cancel hab_0, one_mul, one_mul] at h_mul
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b
[PROOFSTEP]
rw [← @NNReal.le_rpow_one_div_iff _ _ (1 / p) (by simp [lt_of_lt_of_le zero_lt_one hp1])]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ 0 < 1 / p
[PROOFSTEP]
simp [lt_of_lt_of_le zero_lt_one hp1]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ (1 / (1 / p))
[PROOFSTEP]
rw [one_div_one_div]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
exact add_rpow_le_rpow_add _ _ hp1
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
[PROOFSTEP]
have h_rpow : ∀ a : ℝ≥0, a ^ q = (a ^ p) ^ (q / p) := fun a => by
  rw [← NNReal.rpow_mul, div_eq_inv_mul, ← mul_assoc, _root_.mul_inv_cancel hp_pos.ne.symm, one_mul]
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a✝ b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0
⊢ a ^ q = (a ^ p) ^ (q / p)
[PROOFSTEP]
rw [← NNReal.rpow_mul, div_eq_inv_mul, ← mul_assoc, _root_.mul_inv_cancel hp_pos.ne.symm, one_mul]
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
[PROOFSTEP]
have h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p :=
  by
  refine' rpow_add_rpow_le_add (a ^ p) (b ^ p) _
  rwa [one_le_div hp_pos]
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
[PROOFSTEP]
refine' rpow_add_rpow_le_add (a ^ p) (b ^ p) _
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
⊢ 1 ≤ q / p
[PROOFSTEP]
rwa [one_le_div hp_pos]
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
[PROOFSTEP]
rw [h_rpow a, h_rpow b, NNReal.le_rpow_one_div_iff hp_pos, ← NNReal.rpow_mul, mul_comm, mul_one_div]
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p
[PROOFSTEP]
rwa [one_div_div] at h_rpow_add_rpow_le_add
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rcases hp.eq_or_lt with (rfl | hp_pos)
[GOAL]
case inl
ι : Type u
s : Finset ι
a b : ℝ≥0
hp : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ (a + b) ^ 0 ≤ a ^ 0 + b ^ 0
[PROOFSTEP]
simp
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
have h := rpow_add_rpow_le a b hp_pos hp1
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ (1 / 1) ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [one_div_one] at h
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ 1 ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
repeat' rw [NNReal.rpow_one] at h
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ 1 ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [NNReal.rpow_one] at h
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a ^ 1 + b ^ 1 ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [NNReal.rpow_one] at h
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ^ 1 ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [NNReal.rpow_one] at h
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [NNReal.rpow_one] at h
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
exact (NNReal.le_rpow_one_div_iff hp_pos).mp h
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
have hp_pos : 0 < p
[GOAL]
case hp_pos
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ 0 < p
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
positivity
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
have hp_nonneg : 0 ≤ p
[GOAL]
case hp_nonneg
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ 0 ≤ p
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
positivity
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
have hp_not_neg : ¬p < 0 := by simp [hp_nonneg]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
⊢ ¬p < 0
[PROOFSTEP]
simp [hp_nonneg]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
have h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤) := by
  simp [ENNReal.mul_eq_top, hp_pos, hp_nonneg, hp_not_neg]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
⊢ ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
[PROOFSTEP]
simp [ENNReal.mul_eq_top, hp_pos, hp_nonneg, hp_not_neg]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
refine' le_of_top_imp_top_of_toNNReal_le _ _
[GOAL]
case refine'_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
⊢ (∑ i in s, w i * z i) ^ p = ⊤ → ∑ i in s, w i * z i ^ p = ⊤
[PROOFSTEP]
rw [rpow_eq_top_iff, sum_eq_top_iff, sum_eq_top_iff]
[GOAL]
case refine'_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
⊢ ∑ i in s, w i * z i = 0 ∧ p < 0 ∨ (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p → ∃ a, a ∈ s ∧ w a * z a ^ p = ⊤
[PROOFSTEP]
intro h
[GOAL]
case refine'_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h : ∑ i in s, w i * z i = 0 ∧ p < 0 ∨ (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p
⊢ ∃ a, a ∈ s ∧ w a * z a ^ p = ⊤
[PROOFSTEP]
simp only [and_false_iff, hp_not_neg, false_or_iff] at h
[GOAL]
case refine'_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h : (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p
⊢ ∃ a, a ∈ s ∧ w a * z a ^ p = ⊤
[PROOFSTEP]
rcases h.left with ⟨a, H, ha⟩
[GOAL]
case refine'_1.intro.intro
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h : (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p
a : ι
H : a ∈ s
ha : w a * z a = ⊤
⊢ ∃ a, a ∈ s ∧ w a * z a ^ p = ⊤
[PROOFSTEP]
use a, H
[GOAL]
case right
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h : (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p
a : ι
H : a ∈ s
ha : w a * z a = ⊤
⊢ w a * z a ^ p = ⊤
[PROOFSTEP]
rwa [← h_top_iff_rpow_top a H]
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
⊢ (∑ i in s, w i * z i) ^ p ≠ ⊤ →
    ∑ i in s, w i * z i ^ p ≠ ⊤ →
      ENNReal.toNNReal ((∑ i in s, w i * z i) ^ p) ≤ ENNReal.toNNReal (∑ i in s, w i * z i ^ p)
[PROOFSTEP]
intro h_top_rpow_sum
  _
    -- show hypotheses needed to put the `.toNNReal` inside the sums.
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
⊢ ENNReal.toNNReal ((∑ i in s, w i * z i) ^ p) ≤ ENNReal.toNNReal (∑ i in s, w i * z i ^ p)
[PROOFSTEP]
have h_top : ∀ a : ι, a ∈ s → w a * z a ≠ ⊤ :=
  haveI h_top_sum : ∑ i : ι in s, w i * z i ≠ ⊤ := by
    intro h
    rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum
    exact h_top_rpow_sum rfl
  fun a ha => (lt_top_of_sum_ne_top h_top_sum ha).ne
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
⊢ ∑ i in s, w i * z i ≠ ⊤
[PROOFSTEP]
intro h
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h : ∑ i in s, w i * z i = ⊤
⊢ False
[PROOFSTEP]
rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : ⊤ ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h : ∑ i in s, w i * z i = ⊤
⊢ False
[PROOFSTEP]
exact h_top_rpow_sum rfl
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
⊢ ENNReal.toNNReal ((∑ i in s, w i * z i) ^ p) ≤ ENNReal.toNNReal (∑ i in s, w i * z i ^ p)
[PROOFSTEP]
have h_top_rpow : ∀ a : ι, a ∈ s → w a * z a ^ p ≠ ⊤ :=
  by
  intro i hi
  specialize h_top i hi
  rwa [Ne.def, ← h_top_iff_rpow_top i hi]
    -- put the `.toNNReal` inside the sums.
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
⊢ ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
[PROOFSTEP]
intro i hi
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
i : ι
hi : i ∈ s
⊢ w i * z i ^ p ≠ ⊤
[PROOFSTEP]
specialize h_top i hi
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
i : ι
hi : i ∈ s
h_top : w i * z i ≠ ⊤
⊢ w i * z i ^ p ≠ ⊤
[PROOFSTEP]
rwa [Ne.def, ← h_top_iff_rpow_top i hi]
  -- put the `.toNNReal` inside the sums.
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ ENNReal.toNNReal ((∑ i in s, w i * z i) ^ p) ≤ ENNReal.toNNReal (∑ i in s, w i * z i ^ p)
[PROOFSTEP]
simp_rw [toNNReal_sum h_top_rpow, ← toNNReal_rpow, toNNReal_sum h_top, toNNReal_mul, ← toNNReal_rpow]
  -- use corresponding nnreal result
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ (∑ x in s, ENNReal.toNNReal (w x) * ENNReal.toNNReal (z x)) ^ p ≤
    ∑ x in s, ENNReal.toNNReal (w x) * ENNReal.toNNReal (z x) ^ p
[PROOFSTEP]
refine' NNReal.rpow_arith_mean_le_arith_mean_rpow s (fun i => (w i).toNNReal) (fun i => (z i).toNNReal) _ hp
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ ∑ i in s, (fun i => ENNReal.toNNReal (w i)) i = 1
[PROOFSTEP]
have h_sum_nnreal : ∑ i in s, w i = ↑(∑ i in s, (w i).toNNReal) :=
  by
  rw [coe_finset_sum]
  refine' sum_congr rfl fun i hi => (coe_toNNReal _).symm
  refine' (lt_top_of_sum_ne_top _ hi).ne
  exact hw'.symm ▸ ENNReal.one_ne_top
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ ∑ i in s, w i = ↑(∑ i in s, ENNReal.toNNReal (w i))
[PROOFSTEP]
rw [coe_finset_sum]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ ∑ i in s, w i = ∑ a in s, ↑(ENNReal.toNNReal (w a))
[PROOFSTEP]
refine' sum_congr rfl fun i hi => (coe_toNNReal _).symm
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
i : ι
hi : i ∈ s
⊢ w i ≠ ⊤
[PROOFSTEP]
refine' (lt_top_of_sum_ne_top _ hi).ne
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
i : ι
hi : i ∈ s
⊢ ∑ x in s, w x ≠ ⊤
[PROOFSTEP]
exact hw'.symm ▸ ENNReal.one_ne_top
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
h_sum_nnreal : ∑ i in s, w i = ↑(∑ i in s, ENNReal.toNNReal (w i))
⊢ ∑ i in s, (fun i => ENNReal.toNNReal (w i)) i = 1
[PROOFSTEP]
rwa [← coe_eq_coe, ← h_sum_nnreal]
[GOAL]
ι : Type u
s : Finset ι
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
[PROOFSTEP]
have h := rpow_arith_mean_le_arith_mean_rpow univ ![w₁, w₂] ![z₁, z₂] ?_ hp
[GOAL]
case refine_2
ι : Type u
s : Finset ι
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
h :
  (∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons w₁ ![w₂] i * Matrix.vecCons z₁ ![z₂] i) ^ p ≤
    ∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons w₁ ![w₂] i * Matrix.vecCons z₁ ![z₂] i ^ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
[PROOFSTEP]
simpa [Fin.sum_univ_succ] using h
[GOAL]
case refine_1
ι : Type u
s : Finset ι
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons w₁ ![w₂] i = 1
[PROOFSTEP]
simp [hw', Fin.sum_univ_succ]
[GOAL]
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
[PROOFSTEP]
rcases eq_or_lt_of_le hp with (rfl | h'p)
[GOAL]
case inl
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0∞
hp : 1 ≤ 1
⊢ (z₁ + z₂) ^ 1 ≤ 2 ^ (1 - 1) * (z₁ ^ 1 + z₂ ^ 1)
[PROOFSTEP]
simp only [rpow_one, sub_self, rpow_zero, one_mul, le_refl]
[GOAL]
case inr
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
[PROOFSTEP]
convert rpow_arith_mean_le_arith_mean2_rpow (1 / 2) (1 / 2) (2 * z₁) (2 * z₂) (ENNReal.add_halves 1) hp using 1
[GOAL]
case h.e'_3
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ (z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p
[PROOFSTEP]
simp [← mul_assoc, ENNReal.inv_mul_cancel two_ne_zero two_ne_top]
[GOAL]
case h.e'_4
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
[PROOFSTEP]
have _ : p - 1 ≠ 0 := ne_of_gt (sub_pos.2 h'p)
[GOAL]
case h.e'_4
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
x✝ : p - 1 ≠ 0
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
[PROOFSTEP]
simp only [mul_rpow_of_nonneg _ _ (zero_le_one.trans hp), rpow_sub _ _ two_ne_zero two_ne_top, ENNReal.div_eq_inv_mul,
  rpow_one, mul_one]
[GOAL]
case h.e'_4
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
x✝ : p - 1 ≠ 0
⊢ 2⁻¹ * 2 ^ p * (z₁ ^ p + z₂ ^ p) = 2⁻¹ * (2 ^ p * z₁ ^ p) + 2⁻¹ * (2 ^ p * z₂ ^ p)
[PROOFSTEP]
ring
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
have hp_pos : 0 < p := by positivity
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ 0 < p
[PROOFSTEP]
positivity
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
by_cases h_top : a + b = ⊤
[GOAL]
case pos
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : a + b = ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
rw [← @ENNReal.rpow_eq_top_iff_of_pos (a + b) p hp_pos] at h_top
[GOAL]
case pos
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : (a + b) ^ p = ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
rw [h_top]
[GOAL]
case pos
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : (a + b) ^ p = ⊤
⊢ a ^ p + b ^ p ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
obtain ⟨ha_top, hb_top⟩ := add_ne_top.mp h_top
[GOAL]
case neg.intro
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ⊤
ha_top : a ≠ ⊤
hb_top : b ≠ ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
lift a to ℝ≥0 using ha_top
[GOAL]
case neg.intro.intro
ι : Type u
s : Finset ι
p : ℝ
b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
hb_top : b ≠ ⊤
a : ℝ≥0
h_top : ¬↑a + b = ⊤
⊢ ↑a ^ p + b ^ p ≤ (↑a + b) ^ p
[PROOFSTEP]
lift b to ℝ≥0 using hb_top
[GOAL]
case neg.intro.intro.intro
ι : Type u
s : Finset ι
p : ℝ
hp1 : 1 ≤ p
hp_pos : 0 < p
a b : ℝ≥0
h_top : ¬↑a + ↑b = ⊤
⊢ ↑a ^ p + ↑b ^ p ≤ (↑a + ↑b) ^ p
[PROOFSTEP]
simpa [← ENNReal.coe_rpow_of_nonneg _ hp_pos.le] using ENNReal.coe_le_coe.2 (NNReal.add_rpow_le_rpow_add a b hp1)
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b
[PROOFSTEP]
rw [← @ENNReal.le_rpow_one_div_iff _ _ (1 / p) (by simp [lt_of_lt_of_le zero_lt_one hp1])]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ 0 < 1 / p
[PROOFSTEP]
simp [lt_of_lt_of_le zero_lt_one hp1]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ (1 / (1 / p))
[PROOFSTEP]
rw [one_div_one_div]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
exact add_rpow_le_rpow_add _ _ hp1
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
[PROOFSTEP]
have h_rpow : ∀ a : ℝ≥0∞, a ^ q = (a ^ p) ^ (q / p) := fun a => by
  rw [← ENNReal.rpow_mul, _root_.mul_div_cancel' _ hp_pos.ne']
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a✝ b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0∞
⊢ a ^ q = (a ^ p) ^ (q / p)
[PROOFSTEP]
rw [← ENNReal.rpow_mul, _root_.mul_div_cancel' _ hp_pos.ne']
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
[PROOFSTEP]
have h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p :=
  by
  refine' rpow_add_rpow_le_add (a ^ p) (b ^ p) _
  rwa [one_le_div hp_pos]
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
[PROOFSTEP]
refine' rpow_add_rpow_le_add (a ^ p) (b ^ p) _
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
⊢ 1 ≤ q / p
[PROOFSTEP]
rwa [one_le_div hp_pos]
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
[PROOFSTEP]
rw [h_rpow a, h_rpow b, ENNReal.le_rpow_one_div_iff hp_pos, ← ENNReal.rpow_mul, mul_comm, mul_one_div]
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p
[PROOFSTEP]
rwa [one_div_div] at h_rpow_add_rpow_le_add
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rcases hp.eq_or_lt with (rfl | hp_pos)
[GOAL]
case inl
ι : Type u
s : Finset ι
a b : ℝ≥0∞
hp : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ (a + b) ^ 0 ≤ a ^ 0 + b ^ 0
[PROOFSTEP]
simp
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
have h := rpow_add_rpow_le a b hp_pos hp1
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ (1 / 1) ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [one_div_one] at h
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ 1 ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
repeat' rw [ENNReal.rpow_one] at h
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ 1 ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [ENNReal.rpow_one] at h
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a ^ 1 + b ^ 1 ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [ENNReal.rpow_one] at h
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ^ 1 ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [ENNReal.rpow_one] at h
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [ENNReal.rpow_one] at h
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
exact (ENNReal.le_rpow_one_div_iff hp_pos).mp h


[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(valuationOfNeZeroToFun v x) = ↑(valuation v) ↑x
[PROOFSTEP]
rw [show v.valuation (x : K) = _ * _ by rfl]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(valuation v) ↑x = ?m.156670 * ?m.156673
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(valuationOfNeZeroToFun v x) =
    ↑↑(intValuation v).toMonoidWithZeroHom
        (Submonoid.LocalizationMap.sec (IsLocalization.toLocalizationMap R⁰ K) ↑x).fst *
      ↑(↑(IsUnit.liftRight (MonoidHom.restrict (↑(intValuation v).toMonoidWithZeroHom) R⁰)
                (_ : ∀ (s : { x // x ∈ R⁰ }), IsUnit (↑↑(intValuation v).toMonoidWithZeroHom ↑s)))
            (Submonoid.LocalizationMap.sec (IsLocalization.toLocalizationMap R⁰ K) ↑x).snd)⁻¹
[PROOFSTEP]
rw [Units.val_inv_eq_inv_val]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(valuationOfNeZeroToFun v x) =
    ↑↑(intValuation v).toMonoidWithZeroHom
        (Submonoid.LocalizationMap.sec (IsLocalization.toLocalizationMap R⁰ K) ↑x).fst *
      (↑(↑(IsUnit.liftRight (MonoidHom.restrict (↑(intValuation v).toMonoidWithZeroHom) R⁰)
                (_ : ∀ (s : { x // x ∈ R⁰ }), IsUnit (↑↑(intValuation v).toMonoidWithZeroHom ↑s)))
            (Submonoid.LocalizationMap.sec (IsLocalization.toLocalizationMap R⁰ K) ↑x).snd))⁻¹
[PROOFSTEP]
change _ = ite _ _ _ * (ite _ _ _)⁻¹
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(valuationOfNeZeroToFun v x) =
    (if (Submonoid.LocalizationMap.sec (IsLocalization.toLocalizationMap R⁰ K) ↑x).fst = 0 then 0
      else
        ↑(↑Multiplicative.ofAdd
            (-↑(Associates.count (Associates.mk v.asIdeal)
                  (Associates.factors
                    (Associates.mk
                      (Ideal.span
                        {(Submonoid.LocalizationMap.sec (IsLocalization.toLocalizationMap R⁰ K) ↑x).fst}))))))) *
      (if
            ↑(SubmonoidClass.subtype R⁰)
                (Submonoid.LocalizationMap.sec (IsLocalization.toLocalizationMap R⁰ K) ↑x).snd =
              0 then
          0
        else
          ↑(↑Multiplicative.ofAdd
              (-↑(Associates.count (Associates.mk v.asIdeal)
                    (Associates.factors
                      (Associates.mk
                        (Ideal.span
                          {↑(SubmonoidClass.subtype R⁰)
                              (Submonoid.LocalizationMap.sec (IsLocalization.toLocalizationMap R⁰ K) ↑x).snd})))))))⁻¹
[PROOFSTEP]
rw [IsLocalization.toLocalizationMap_sec]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(valuationOfNeZeroToFun v x) =
    (if (IsLocalization.sec R⁰ ↑x).fst = 0 then 0
      else
        ↑(↑Multiplicative.ofAdd
            (-↑(Associates.count (Associates.mk v.asIdeal)
                  (Associates.factors (Associates.mk (Ideal.span {(IsLocalization.sec R⁰ ↑x).fst}))))))) *
      (if ↑(SubmonoidClass.subtype R⁰) (IsLocalization.sec R⁰ ↑x).snd = 0 then 0
        else
          ↑(↑Multiplicative.ofAdd
              (-↑(Associates.count (Associates.mk v.asIdeal)
                    (Associates.factors
                      (Associates.mk (Ideal.span {↑(SubmonoidClass.subtype R⁰) (IsLocalization.sec R⁰ ↑x).snd})))))))⁻¹
[PROOFSTEP]
rw [if_neg <| IsLocalization.sec_fst_ne_zero le_rfl x.ne_zero, if_neg ?_]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(valuationOfNeZeroToFun v x) =
    ↑(↑Multiplicative.ofAdd
          (-↑(Associates.count (Associates.mk v.asIdeal)
                (Associates.factors (Associates.mk (Ideal.span {(IsLocalization.sec R⁰ ↑x).fst})))))) *
      (↑(↑Multiplicative.ofAdd
            (-↑(Associates.count (Associates.mk v.asIdeal)
                  (Associates.factors
                    (Associates.mk (Ideal.span {↑(SubmonoidClass.subtype R⁰) (IsLocalization.sec R⁰ ↑x).snd})))))))⁻¹
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ¬↑(SubmonoidClass.subtype R⁰) (IsLocalization.sec R⁰ ↑x).snd = 0
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ¬↑(SubmonoidClass.subtype R⁰) (IsLocalization.sec R⁰ ↑x).snd = 0
[PROOFSTEP]
exact nonZeroDivisors.coe_ne_zero _
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ valuationOfNeZeroToFun v 1 = 1
[PROOFSTEP]
rw [← WithZero.coe_inj, valuationOfNeZeroToFun_eq]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ ↑(valuation v) ↑1 = ↑1
[PROOFSTEP]
exact map_one _
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x✝¹ x✝ : Kˣ
⊢ OneHom.toFun { toFun := valuationOfNeZeroToFun v, map_one' := (_ : valuationOfNeZeroToFun v 1 = 1) } (x✝¹ * x✝) =
    OneHom.toFun { toFun := valuationOfNeZeroToFun v, map_one' := (_ : valuationOfNeZeroToFun v 1 = 1) } x✝¹ *
      OneHom.toFun { toFun := valuationOfNeZeroToFun v, map_one' := (_ : valuationOfNeZeroToFun v 1 = 1) } x✝
[PROOFSTEP]
rw [← WithZero.coe_inj, WithZero.coe_mul]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x✝¹ x✝ : Kˣ
⊢ ↑(OneHom.toFun { toFun := valuationOfNeZeroToFun v, map_one' := (_ : valuationOfNeZeroToFun v 1 = 1) } (x✝¹ * x✝)) =
    ↑(OneHom.toFun { toFun := valuationOfNeZeroToFun v, map_one' := (_ : valuationOfNeZeroToFun v 1 = 1) } x✝¹) *
      ↑(OneHom.toFun { toFun := valuationOfNeZeroToFun v, map_one' := (_ : valuationOfNeZeroToFun v 1 = 1) } x✝)
[PROOFSTEP]
simp only [valuationOfNeZeroToFun_eq]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x✝¹ x✝ : Kˣ
⊢ ↑(valuation v) ↑(x✝¹ * x✝) = ↑(valuation v) ↑x✝¹ * ↑(valuation v) ↑x✝
[PROOFSTEP]
exact map_mul _ _ _
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Rˣ
⊢ ↑(valuationOfNeZero v) (↑(Units.map ↑(algebraMap R K)) x) = 1
[PROOFSTEP]
rw [← WithZero.coe_inj, valuationOfNeZero_eq, Units.coe_map, eq_iff_le_not_lt]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Rˣ
⊢ ↑(valuation v) (↑↑(algebraMap R K) ↑x) ≤ ↑1 ∧ ¬↑(valuation v) (↑↑(algebraMap R K) ↑x) < ↑1
[PROOFSTEP]
constructor
[GOAL]
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Rˣ
⊢ ↑(valuation v) (↑↑(algebraMap R K) ↑x) ≤ ↑1
[PROOFSTEP]
exact v.valuation_le_one x
[GOAL]
case right
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Rˣ
⊢ ¬↑(valuation v) (↑↑(algebraMap R K) ↑x) < ↑1
[PROOFSTEP]
cases' x with x _ hx _
[GOAL]
case right.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
hx : x * inv✝ = 1
inv_val✝ : inv✝ * x = 1
⊢ ¬↑(valuation v) (↑↑(algebraMap R K) ↑{ val := x, inv := inv✝, val_inv := hx, inv_val := inv_val✝ }) < ↑1
[PROOFSTEP]
change ¬v.valuation (algebraMap R K x) < 1
[GOAL]
case right.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
hx : x * inv✝ = 1
inv_val✝ : inv✝ * x = 1
⊢ ¬↑(valuation v) (↑(algebraMap R K) x) < 1
[PROOFSTEP]
apply_fun v.intValuation at hx
[GOAL]
case right.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : ↑(intValuation v) (x * inv✝) = ↑(intValuation v) 1
⊢ ¬↑(valuation v) (↑(algebraMap R K) x) < 1
[PROOFSTEP]
rw [map_one, map_mul] at hx
[GOAL]
case right.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : ↑(intValuation v) x * ↑(intValuation v) inv✝ = 1
⊢ ¬↑(valuation v) (↑(algebraMap R K) x) < 1
[PROOFSTEP]
rw [not_lt, ← hx, ← mul_one <| v.valuation _, valuation_of_algebraMap,
  mul_le_mul_left₀ <| left_ne_zero_of_mul_eq_one hx]
[GOAL]
case right.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x inv✝ : R
inv_val✝ : inv✝ * x = 1
hx : ↑(intValuation v) x * ↑(intValuation v) inv✝ = 1
⊢ ↑(intValuation v) inv✝ ≤ 1
[PROOFSTEP]
exact v.int_valuation_le_one _
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
n : ℕ
⊢ MonoidHom.range (powMonoidHom n) ≤
    Subgroup.comap (valuationOfNeZero v) (↑AddSubgroup.toSubgroup (AddSubgroup.zmultiples ↑n))
[PROOFSTEP]
rintro _ ⟨x, rfl⟩
[GOAL]
case intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
n : ℕ
x : Kˣ
⊢ ↑(powMonoidHom n) x ∈ Subgroup.comap (valuationOfNeZero v) (↑AddSubgroup.toSubgroup (AddSubgroup.zmultiples ↑n))
[PROOFSTEP]
exact ⟨v.valuationOfNeZero x, by simp only [powMonoidHom_apply, map_pow, Int.toAdd_pow]; rfl⟩
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
n : ℕ
x : Kˣ
⊢ (fun x => x • ↑n) (↑(valuationOfNeZero v) x) = ↑Multiplicative.toAdd (↑(valuationOfNeZero v) (↑(powMonoidHom n) x))
[PROOFSTEP]
simp only [powMonoidHom_apply, map_pow, Int.toAdd_pow]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
n : ℕ
x : Kˣ
⊢ ↑(valuationOfNeZero v) x • ↑n = ↑Multiplicative.toAdd (↑(valuationOfNeZero v) x) * ↑n
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
n : ℕ
x : Rˣ
⊢ ↑(valuationOfNeZeroMod v n) ↑(↑(Units.map ↑(algebraMap R K)) x) = 1
[PROOFSTEP]
rw [valuationOfNeZeroMod, MonoidHom.comp_apply, ← QuotientGroup.coe_mk',
  QuotientGroup.map_mk' (G := Kˣ) (N := MonoidHom.range (powMonoidHom n)), valuation_of_unit_eq, QuotientGroup.mk_one,
  map_one]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
a✝ b✝ : Kˣ ⧸ MonoidHom.range (powMonoidHom n)
hx : a✝ ∈ {x | ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) x = 1}
hy : b✝ ∈ {x | ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) x = 1}
v : HeightOneSpectrum R
hv : ¬v ∈ S
⊢ ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) (a✝ * b✝) = 1
[PROOFSTEP]
rw [map_mul, hx v hv, hy v hv, one_mul]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x✝¹ : HeightOneSpectrum R
x✝ : ¬x✝¹ ∈ S
⊢ ↑(HeightOneSpectrum.valuationOfNeZeroMod x✝¹ n) 1 = 1
[PROOFSTEP]
rw [map_one]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x✝ : Kˣ ⧸ MonoidHom.range (powMonoidHom n)
hx :
  x✝ ∈
    {
          toSubsemigroup :=
            {
              carrier :=
                {x | ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) x = 1},
              mul_mem' :=
                (_ :
                  ∀ {a b : Kˣ ⧸ MonoidHom.range (powMonoidHom n)},
                    a ∈
                        {x |
                          ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) x = 1} →
                      b ∈
                          {x |
                            ∀ (v : HeightOneSpectrum R), ¬v ∈ S → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) x = 1} →
                        ∀ (v : HeightOneSpectrum R),
                          ¬v ∈ S → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) (a * b) = 1) },
          one_mem' :=
            (_ :
              ∀ (x : HeightOneSpectrum R),
                ¬x ∈ S → ↑(HeightOneSpectrum.valuationOfNeZeroMod x n) 1 = 1) }.toSubsemigroup.carrier
v : HeightOneSpectrum R
hv : ¬v ∈ S
⊢ ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) x✝⁻¹ = 1
[PROOFSTEP]
rw [map_inv, hx v hv, inv_one]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x y : { x // x ∈ selmerGroup }
⊢ OneHom.toFun
      { toFun := fun x v => ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑x,
        map_one' := (_ : (fun x v => ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑x) 1 = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := fun x v => ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑x,
          map_one' := (_ : (fun x v => ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑x) 1 = 1) }
        x *
      OneHom.toFun
        { toFun := fun x v => ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑x,
          map_one' := (_ : (fun x v => ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑x) 1 = 1) }
        y
[PROOFSTEP]
simp only [Submonoid.coe_mul, Subgroup.coe_toSubmonoid, map_mul]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x y : { x // x ∈ selmerGroup }
⊢ (fun v => ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑x * ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑y) =
    (fun v => ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑x) * fun v =>
      ↑(HeightOneSpectrum.valuationOfNeZeroMod (↑v) n) ↑y
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
⊢ MonoidHom.ker valuation = Subgroup.subgroupOf selmerGroup selmerGroup
[PROOFSTEP]
ext ⟨_, hx⟩
[GOAL]
case h.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ MonoidHom.range (powMonoidHom n)
hx : val✝ ∈ selmerGroup
⊢ { val := val✝, property := hx } ∈ MonoidHom.ker valuation ↔
    { val := val✝, property := hx } ∈ Subgroup.subgroupOf selmerGroup selmerGroup
[PROOFSTEP]
constructor
[GOAL]
case h.mk.mp
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ MonoidHom.range (powMonoidHom n)
hx : val✝ ∈ selmerGroup
⊢ { val := val✝, property := hx } ∈ MonoidHom.ker valuation →
    { val := val✝, property := hx } ∈ Subgroup.subgroupOf selmerGroup selmerGroup
[PROOFSTEP]
intro hx' v _
[GOAL]
case h.mk.mp
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ MonoidHom.range (powMonoidHom n)
hx : val✝ ∈ selmerGroup
hx' : { val := val✝, property := hx } ∈ MonoidHom.ker valuation
v : HeightOneSpectrum R
x✝ : ¬v ∈ ∅
⊢ ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) (↑(Subgroup.subtype selmerGroup) { val := val✝, property := hx }) = 1
[PROOFSTEP]
by_cases hv : v ∈ S
[GOAL]
case pos
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ MonoidHom.range (powMonoidHom n)
hx : val✝ ∈ selmerGroup
hx' : { val := val✝, property := hx } ∈ MonoidHom.ker valuation
v : HeightOneSpectrum R
x✝ : ¬v ∈ ∅
hv : v ∈ S
⊢ ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) (↑(Subgroup.subtype selmerGroup) { val := val✝, property := hx }) = 1
[PROOFSTEP]
exact congr_fun hx' ⟨v, hv⟩
[GOAL]
case neg
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ MonoidHom.range (powMonoidHom n)
hx : val✝ ∈ selmerGroup
hx' : { val := val✝, property := hx } ∈ MonoidHom.ker valuation
v : HeightOneSpectrum R
x✝ : ¬v ∈ ∅
hv : ¬v ∈ S
⊢ ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) (↑(Subgroup.subtype selmerGroup) { val := val✝, property := hx }) = 1
[PROOFSTEP]
exact hx v hv
[GOAL]
case h.mk.mpr
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ MonoidHom.range (powMonoidHom n)
hx : val✝ ∈ selmerGroup
⊢ { val := val✝, property := hx } ∈ Subgroup.subgroupOf selmerGroup selmerGroup →
    { val := val✝, property := hx } ∈ MonoidHom.ker valuation
[PROOFSTEP]
exact fun hx' => funext fun v => hx' v <| Set.not_mem_empty v
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n✝ n : ℕ
⊢ (fun x =>
        { val := ↑(↑(Units.map ↑(algebraMap R K)) x),
          property :=
            (_ :
              ∀ (v : HeightOneSpectrum R),
                ¬v ∈ ∅ → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) ↑(↑(Units.map ↑(algebraMap R K)) x) = 1) })
      1 =
    1
[PROOFSTEP]
simp only [map_one, QuotientGroup.mk_one, Subgroup.mk_eq_one_iff]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n✝ n : ℕ
x✝¹ x✝ : Rˣ
⊢ OneHom.toFun
      {
        toFun := fun x =>
          { val := ↑(↑(Units.map ↑(algebraMap R K)) x),
            property :=
              (_ :
                ∀ (v : HeightOneSpectrum R),
                  ¬v ∈ ∅ → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) ↑(↑(Units.map ↑(algebraMap R K)) x) = 1) },
        map_one' :=
          (_ :
            { val := ↑(↑(Units.map ↑(algebraMap R K)) 1),
                property :=
                  (_ :
                    ∀ (v : HeightOneSpectrum R),
                      ¬v ∈ ∅ →
                        ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) ↑(↑(Units.map ↑(algebraMap R K)) 1) = 1) } =
              1) }
      (x✝¹ * x✝) =
    OneHom.toFun
        {
          toFun := fun x =>
            { val := ↑(↑(Units.map ↑(algebraMap R K)) x),
              property :=
                (_ :
                  ∀ (v : HeightOneSpectrum R),
                    ¬v ∈ ∅ → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) ↑(↑(Units.map ↑(algebraMap R K)) x) = 1) },
          map_one' :=
            (_ :
              { val := ↑(↑(Units.map ↑(algebraMap R K)) 1),
                  property :=
                    (_ :
                      ∀ (v : HeightOneSpectrum R),
                        ¬v ∈ ∅ →
                          ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) ↑(↑(Units.map ↑(algebraMap R K)) 1) = 1) } =
                1) }
        x✝¹ *
      OneHom.toFun
        {
          toFun := fun x =>
            { val := ↑(↑(Units.map ↑(algebraMap R K)) x),
              property :=
                (_ :
                  ∀ (v : HeightOneSpectrum R),
                    ¬v ∈ ∅ → ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) ↑(↑(Units.map ↑(algebraMap R K)) x) = 1) },
          map_one' :=
            (_ :
              { val := ↑(↑(Units.map ↑(algebraMap R K)) 1),
                  property :=
                    (_ :
                      ∀ (v : HeightOneSpectrum R),
                        ¬v ∈ ∅ →
                          ↑(HeightOneSpectrum.valuationOfNeZeroMod v n) ↑(↑(Units.map ↑(algebraMap R K)) 1) = 1) } =
                1) }
        x✝
[PROOFSTEP]
simp only [RingHom.toMonoidHom_eq_coe, map_mul, MonoidHom.mem_range, powMonoidHom_apply, QuotientGroup.mk_mul,
  Submonoid.mk_mul_mk]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
⊢ MonoidHom.ker fromUnit = MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
ext ⟨_, _, _, _⟩
[GOAL]
case h.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit ↔
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
constructor
[GOAL]
case h.mk.mp
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit →
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
intro hx
[GOAL]
case h.mk.mp
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
rcases(QuotientGroup.eq_one_iff _).mp (Subtype.mk.inj hx) with ⟨⟨v, i, vi, iv⟩, hx⟩
[GOAL]
case h.mk.mp.intro.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  ↑(powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
have hv : ↑(_ ^ n : Kˣ) = algebraMap R K _ := by exact congr_arg Units.val hx
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  ↑(powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
⊢ ↑(?m.1066492 ^ n) = ↑(algebraMap R K) ?m.1066434
[PROOFSTEP]
exact congr_arg Units.val hx
[GOAL]
case h.mk.mp.intro.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  ↑(powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑({ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n) =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
have hi : ↑(_ ^ n : Kˣ)⁻¹ = algebraMap R K _ := by exact congr_arg Units.inv hx
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  ↑(powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑({ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n) =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
⊢ ↑(?m.1219650 ^ n)⁻¹ = ↑(algebraMap R K) ?m.1219637
[PROOFSTEP]
exact congr_arg Units.inv hx
[GOAL]
case h.mk.mp.intro.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  ↑(powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑({ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n) =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑({ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n)⁻¹ =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
rw [Units.val_pow_eq_pow_val] at hv
[GOAL]
case h.mk.mp.intro.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  ↑(powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑({ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n)⁻¹ =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
rw [← inv_pow, Units.inv_mk, Units.val_pow_eq_pow_val] at hi
[GOAL]
case h.mk.mp.intro.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  ↑(powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := i, inv := v, val_inv := iv, inv_val := vi } ^ n =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
rcases IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow (R := R) (x := v) hn.out
    (hv.symm ▸ isIntegral_algebraMap) with
  ⟨v', rfl⟩
[GOAL]
case h.mk.mp.intro.mk.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
i : K
v' : R
vi : ↑(algebraMap R K) v' * i = 1
iv : i * ↑(algebraMap R K) v' = 1
hx :
  ↑(powMonoidHom n) { val := ↑(algebraMap R K) v', inv := i, val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := ↑(algebraMap R K) v', inv := i, val_inv := vi, inv_val := iv } ^ n =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := i, inv := ↑(algebraMap R K) v', val_inv := iv, inv_val := vi } ^ n =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
rcases IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow (R := R) (x := i) hn.out
    (hi.symm ▸ isIntegral_algebraMap) with
  ⟨i', rfl⟩
[GOAL]
case h.mk.mp.intro.mk.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v' i' : R
vi : ↑(algebraMap R K) v' * ↑(algebraMap R K) i' = 1
iv : ↑(algebraMap R K) i' * ↑(algebraMap R K) v' = 1
hx :
  ↑(powMonoidHom n) { val := ↑(algebraMap R K) v', inv := ↑(algebraMap R K) i', val_inv := vi, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := ↑(algebraMap R K) v', inv := ↑(algebraMap R K) i', val_inv := vi, inv_val := iv } ^ n =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := ↑(algebraMap R K) i', inv := ↑(algebraMap R K) v', val_inv := iv, inv_val := vi } ^ n =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
rw [← map_mul, map_eq_one_iff _ <| NoZeroSMulDivisors.algebraMap_injective R K] at vi
[GOAL]
case h.mk.mp.intro.mk.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v' i' : R
vi✝ : ↑(algebraMap R K) v' * ↑(algebraMap R K) i' = 1
vi : v' * i' = 1
iv : ↑(algebraMap R K) i' * ↑(algebraMap R K) v' = 1
hx :
  ↑(powMonoidHom n) { val := ↑(algebraMap R K) v', inv := ↑(algebraMap R K) i', val_inv := vi✝, inv_val := iv } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := ↑(algebraMap R K) v', inv := ↑(algebraMap R K) i', val_inv := vi✝, inv_val := iv } ^ n =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := ↑(algebraMap R K) i', inv := ↑(algebraMap R K) v', val_inv := iv, inv_val := vi✝ } ^ n =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
rw [← map_mul, map_eq_one_iff _ <| NoZeroSMulDivisors.algebraMap_injective R K] at iv
[GOAL]
case h.mk.mp.intro.mk.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v' i' : R
vi✝ : ↑(algebraMap R K) v' * ↑(algebraMap R K) i' = 1
vi : v' * i' = 1
iv✝ : ↑(algebraMap R K) i' * ↑(algebraMap R K) v' = 1
iv : i' * v' = 1
hx :
  ↑(powMonoidHom n) { val := ↑(algebraMap R K) v', inv := ↑(algebraMap R K) i', val_inv := vi✝, inv_val := iv✝ } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := ↑(algebraMap R K) v', inv := ↑(algebraMap R K) i', val_inv := vi✝, inv_val := iv✝ } ^ n =
    ↑(algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑{ val := ↑(algebraMap R K) i', inv := ↑(algebraMap R K) v', val_inv := iv✝, inv_val := vi✝ } ^ n =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
rw [Units.val_mk, ← map_pow] at hv
[GOAL]
case h.mk.mp.intro.mk.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v' i' : R
vi✝ : ↑(algebraMap R K) v' * ↑(algebraMap R K) i' = 1
vi : v' * i' = 1
iv✝ : ↑(algebraMap R K) i' * ↑(algebraMap R K) v' = 1
iv : i' * v' = 1
hx :
  ↑(powMonoidHom n) { val := ↑(algebraMap R K) v', inv := ↑(algebraMap R K) i', val_inv := vi✝, inv_val := iv✝ } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv : ↑(algebraMap R K) (v' ^ n) = ↑(algebraMap R K) val✝
hi :
  ↑{ val := ↑(algebraMap R K) i', inv := ↑(algebraMap R K) v', val_inv := iv✝, inv_val := vi✝ } ^ n =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n)
[PROOFSTEP]
exact
  ⟨⟨v', i', vi, iv⟩, by
    simpa only [Units.ext_iff, powMonoidHom_apply, Units.val_pow_eq_pow_val] using
      NoZeroSMulDivisors.algebraMap_injective R K hv⟩
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
v' i' : R
vi✝ : ↑(algebraMap R K) v' * ↑(algebraMap R K) i' = 1
vi : v' * i' = 1
iv✝ : ↑(algebraMap R K) i' * ↑(algebraMap R K) v' = 1
iv : i' * v' = 1
hx :
  ↑(powMonoidHom n) { val := ↑(algebraMap R K) v', inv := ↑(algebraMap R K) i', val_inv := vi✝, inv_val := iv✝ } =
    ↑(Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv : ↑(algebraMap R K) (v' ^ n) = ↑(algebraMap R K) val✝
hi :
  ↑{ val := ↑(algebraMap R K) i', inv := ↑(algebraMap R K) v', val_inv := iv✝, inv_val := vi✝ } ^ n =
    ↑(algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ ↑(powMonoidHom n) { val := v', inv := i', val_inv := vi, inv_val := iv } =
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
[PROOFSTEP]
simpa only [Units.ext_iff, powMonoidHom_apply, Units.val_pow_eq_pow_val] using
  NoZeroSMulDivisors.algebraMap_injective R K hv
[GOAL]
case h.mk.mpr
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.range (powMonoidHom n) →
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case h.mk.mpr.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
x : Rˣ
hx : ↑(powMonoidHom n) x = { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ MonoidHom.ker fromUnit
[PROOFSTEP]
rw [← hx]
[GOAL]
case h.mk.mpr.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
x : Rˣ
hx : ↑(powMonoidHom n) x = { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
⊢ ↑(powMonoidHom n) x ∈ MonoidHom.ker fromUnit
[PROOFSTEP]
exact
  Subtype.mk_eq_mk.mpr <|
    (QuotientGroup.eq_one_iff _).mpr
      ⟨Units.map (algebraMap R K) x, by simp only [powMonoidHom_apply, RingHom.toMonoidHom_eq_coe, map_pow]⟩
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
x : Rˣ
hx : ↑(powMonoidHom n) x = { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
⊢ ↑(powMonoidHom n) (↑(Units.map ↑(algebraMap R K)) x) = ↑(Units.map ↑(algebraMap R K)) (↑(powMonoidHom n) x)
[PROOFSTEP]
simp only [powMonoidHom_apply, RingHom.toMonoidHom_eq_coe, map_pow]
[GOAL]
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsDedekindDomain R
K : Type v
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
inst✝ : Fact (0 < n)
⊢ Function.Injective ↑fromUnitLift
[PROOFSTEP]
dsimp only [fromUnitLift, MonoidHom.coe_comp, MulEquiv.coe_toMonoidHom]
[GOAL]
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsDedekindDomain R
K : Type v
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
inst✝ : Fact (0 < n)
⊢ Function.Injective
    (↑(QuotientGroup.kerLift fromUnit) ∘
      ↑(MulEquiv.symm
          (QuotientGroup.quotientMulEquivOfEq (_ : MonoidHom.ker fromUnit = MonoidHom.range (powMonoidHom n)))))
[PROOFSTEP]
exact Function.Injective.comp (QuotientGroup.kerLift_injective _) (MulEquiv.injective _)