[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1
[PROOFSTEP]
by_cases hc : p = 2
[GOAL]
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : p = 2
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1
[PROOFSTEP]
subst hc
[GOAL]
case pos
inst✝ : Fact (Nat.Prime 2)
x : (ZMod 2)ˣ
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (2 / 2) = 1
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton, exists_const]
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1
[PROOFSTEP]
have h₀ := FiniteField.unit_isSquare_iff (by rwa [ringChar_zmod_n]) x
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
⊢ ringChar (ZMod p) ≠ 2
[PROOFSTEP]
rwa [ringChar_zmod_n]
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1
[PROOFSTEP]
have hs : (∃ y : (ZMod p)ˣ, y ^ 2 = x) ↔ IsSquare x :=
  by
  rw [isSquare_iff_exists_sq x]
  simp_rw [eq_comm]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
⊢ (∃ y, y ^ 2 = x) ↔ IsSquare x
[PROOFSTEP]
rw [isSquare_iff_exists_sq x]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
⊢ (∃ y, y ^ 2 = x) ↔ ∃ c, x = c ^ 2
[PROOFSTEP]
simp_rw [eq_comm]
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
hs : (∃ y, y ^ 2 = x) ↔ IsSquare x
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1
[PROOFSTEP]
rw [hs]
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
hs : (∃ y, y ^ 2 = x) ↔ IsSquare x
⊢ IsSquare x ↔ x ^ (p / 2) = 1
[PROOFSTEP]
rwa [card p] at h₀
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ IsSquare a ↔ a ^ (p / 2) = 1
[PROOFSTEP]
apply (iff_congr _ (by simp [Units.ext_iff])).mp (euler_criterion_units p (Units.mk0 a ha))
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ Units.mk0 a ha ^ (p / 2) = 1 ↔ a ^ (p / 2) = 1
[PROOFSTEP]
simp [Units.ext_iff]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ (∃ y, y ^ 2 = Units.mk0 a ha) ↔ IsSquare a
[PROOFSTEP]
simp only [Units.ext_iff, sq, Units.val_mk0, Units.val_mul]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ (∃ y, ↑y * ↑y = a) ↔ IsSquare a
[PROOFSTEP]
constructor
[GOAL]
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ (∃ y, ↑y * ↑y = a) → IsSquare a
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case mp.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
y : (ZMod p)ˣ
hy : ↑y * ↑y = a
⊢ IsSquare a
[PROOFSTEP]
exact ⟨y, hy.symm⟩
[GOAL]
case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ IsSquare a → ∃ y, ↑y * ↑y = a
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case mpr.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
⊢ ∃ y_1, ↑y_1 * ↑y_1 = y * y
[PROOFSTEP]
have hy : y ≠ 0 := by
  rintro rfl
  simp [zero_pow, mul_zero, ne_eq, not_true] at ha
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
⊢ y ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
ha : 0 * 0 ≠ 0
⊢ False
[PROOFSTEP]
simp [zero_pow, mul_zero, ne_eq, not_true] at ha
[GOAL]
case mpr.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ∃ y_1, ↑y_1 * ↑y_1 = y * y
[PROOFSTEP]
refine' ⟨Units.mk0 y hy, _⟩
[GOAL]
case mpr.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ↑(Units.mk0 y hy) * ↑(Units.mk0 y hy) = y * y
[PROOFSTEP]
simp
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1
[PROOFSTEP]
cases' Prime.eq_two_or_odd (@Fact.out p.Prime _) with hp2 hp_odd
[GOAL]
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp2 : p = 2
⊢ a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1
[PROOFSTEP]
subst p
[GOAL]
case inl
inst✝ : Fact (Nat.Prime 2)
a : ZMod 2
ha : a ≠ 0
⊢ a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1
[PROOFSTEP]
revert a ha
[GOAL]
case inl
inst✝ : Fact (Nat.Prime 2)
⊢ ∀ {a : ZMod 2}, a ≠ 0 → a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1
[PROOFSTEP]
intro a
[GOAL]
case inl
inst✝ : Fact (Nat.Prime 2)
a : ZMod 2
⊢ a ≠ 0 → a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1
[PROOFSTEP]
fin_cases a
[GOAL]
case inl.head
inst✝ : Fact (Nat.Prime 2)
⊢ { val := 0, isLt := (_ : 0 < 1 + 1) } ≠ 0 →
    { val := 0, isLt := (_ : 0 < 1 + 1) } ^ (2 / 2) = 1 ∨ { val := 0, isLt := (_ : 0 < 1 + 1) } ^ (2 / 2) = -1
case inl.tail.head
inst✝ : Fact (Nat.Prime 2)
⊢ { val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) } ≠ 0 →
    { val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) } ^ (2 / 2) = 1 ∨
      { val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) } ^ (2 / 2) = -1
[PROOFSTEP]
tauto
[GOAL]
case inl.tail.head
inst✝ : Fact (Nat.Prime 2)
⊢ { val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) } ≠ 0 →
    { val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) } ^ (2 / 2) = 1 ∨
      { val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) } ^ (2 / 2) = -1
[PROOFSTEP]
simp
[GOAL]
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp_odd : p % 2 = 1
⊢ a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1
[PROOFSTEP]
rw [← mul_self_eq_one_iff, ← pow_add, ← two_mul, two_mul_odd_div_two hp_odd]
[GOAL]
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp_odd : p % 2 = 1
⊢ a ^ (p - 1) = 1
[PROOFSTEP]
exact pow_card_sub_one_eq_one ha
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)
[PROOFSTEP]
cases' eq_or_ne (ringChar (ZMod p)) 2 with hc hc
[GOAL]
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)
[PROOFSTEP]
by_cases ha : (a : ZMod p) = 0
[GOAL]
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ↑a = 0
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)
[PROOFSTEP]
rw [legendreSym, ha, quadraticChar_zero, zero_pow (Nat.div_pos (@Fact.out p.Prime).two_le (succ_pos 1))]
[GOAL]
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ↑a = 0
⊢ ↑0 = 0
[PROOFSTEP]
norm_cast
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ¬↑a = 0
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)
[PROOFSTEP]
have := (ringChar_zmod_n p).symm.trans hc
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ¬↑a = 0
this : p = 2
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)
[PROOFSTEP]
subst p
[GOAL]
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
ha : ¬↑a = 0
⊢ ↑(legendreSym 2 a) = ↑a ^ (2 / 2)
[PROOFSTEP]
rw [legendreSym, quadraticChar_eq_one_of_char_two hc ha]
[GOAL]
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
ha : ¬↑a = 0
⊢ ↑1 = ↑a ^ (2 / 2)
[PROOFSTEP]
revert ha
[GOAL]
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬↑a = 0 → ↑1 = ↑a ^ (2 / 2)
[PROOFSTEP]
push_cast
[GOAL]
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬↑a = 0 → 1 = ↑a ^ (2 / 2)
[PROOFSTEP]
generalize (a : ZMod 2) = b
[GOAL]
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
b : ZMod 2
⊢ ¬b = 0 → 1 = b ^ (2 / 2)
[PROOFSTEP]
fin_cases b
[GOAL]
case neg.head
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬{ val := 0, isLt := (_ : 0 < 1 + 1) } = 0 → 1 = { val := 0, isLt := (_ : 0 < 1 + 1) } ^ (2 / 2)
[PROOFSTEP]
tauto
[GOAL]
case neg.tail.head
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬{ val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) } = 0 →
    1 = { val := 1, isLt := (_ : (fun a => a < 1 + 1) 1) } ^ (2 / 2)
[PROOFSTEP]
simp
[GOAL]
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)
[PROOFSTEP]
convert quadraticChar_eq_pow_of_char_ne_two' hc (a : ZMod p)
[GOAL]
case h.e'_3.h.e'_6.h.e'_5
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ p = Fintype.card (ZMod p)
[PROOFSTEP]
norm_cast
[GOAL]
case h.e'_3.h.e'_6.h.e'_5
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ p = Fintype.card (ZMod p)
[PROOFSTEP]
congr
[GOAL]
case h.e'_3.h.e'_6.h.e'_5
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ p = Fintype.card (ZMod p)
[PROOFSTEP]
exact (card p).symm
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ legendreSym p 0 = 0
[PROOFSTEP]
rw [legendreSym, Int.cast_zero, MulChar.map_zero]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ legendreSym p 1 = 1
[PROOFSTEP]
rw [legendreSym, Int.cast_one, MulChar.map_one]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a b : ℤ
⊢ legendreSym p (a * b) = legendreSym p a * legendreSym p b
[PROOFSTEP]
simp [legendreSym, Int.cast_mul, map_mul, quadraticCharFun_mul]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
⊢ legendreSym p (a ^ 2) = 1
[PROOFSTEP]
dsimp only [legendreSym]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
⊢ ↑(quadraticChar (ZMod p)) ↑(a ^ 2) = 1
[PROOFSTEP]
rw [Int.cast_pow]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
⊢ ↑(quadraticChar (ZMod p)) (↑a ^ 2) = 1
[PROOFSTEP]
exact quadraticChar_sq_one' ha
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
⊢ legendreSym p a = legendreSym p (a % ↑p)
[PROOFSTEP]
simp only [legendreSym, int_cast_mod]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha0 : ↑a ≠ 0
⊢ legendreSym p ↑a = 1 ↔ IsSquare ↑a
[PROOFSTEP]
rw [eq_one_iff]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha0 : ↑a ≠ 0
⊢ IsSquare ↑↑a ↔ IsSquare ↑a
case ha0 p : ℕ inst✝ : Fact (Nat.Prime p) a : ℕ ha0 : ↑a ≠ 0 ⊢ ↑↑a ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
case ha0
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha0 : ↑a ≠ 0
⊢ ↑↑a ≠ 0
[PROOFSTEP]
exact_mod_cast ha0
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
⊢ legendreSym p ↑a = -1 ↔ ¬IsSquare ↑a
[PROOFSTEP]
rw [eq_neg_one_iff]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
⊢ ¬IsSquare ↑↑a ↔ ¬IsSquare ↑a
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : x ^ 2 - ↑a * y ^ 2 = 0
⊢ legendreSym p a = 1
[PROOFSTEP]
apply_fun (· * y⁻¹ ^ 2) at hxy
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = 0 * y⁻¹ ^ 2
⊢ legendreSym p a = 1
[PROOFSTEP]
simp only [zero_mul] at hxy
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = 0
⊢ legendreSym p a = 1
[PROOFSTEP]
rw [(by ring : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = (x * y⁻¹) ^ 2 - a * (y * y⁻¹) ^ 2), mul_inv_cancel hy, one_pow, mul_one,
  sub_eq_zero, pow_two] at hxy
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = 0
⊢ (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = (x * y⁻¹) ^ 2 - ↑a * (y * y⁻¹) ^ 2
[PROOFSTEP]
ring
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : x * y⁻¹ * (x * y⁻¹) = ↑a
⊢ legendreSym p a = 1
[PROOFSTEP]
exact (eq_one_iff p ha).mpr ⟨x * y⁻¹, hxy.symm⟩
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hx : x ≠ 0
hxy : x ^ 2 - ↑a * y ^ 2 = 0
⊢ legendreSym p a = 1
[PROOFSTEP]
haveI hy : y ≠ 0 := by
  rintro rfl
  rw [zero_pow' 2 (by norm_num), mul_zero, sub_zero, pow_eq_zero_iff (by norm_num : 0 < 2)] at hxy
  exact hx hxy
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hx : x ≠ 0
hxy : x ^ 2 - ↑a * y ^ 2 = 0
⊢ y ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x : ZMod p
hx : x ≠ 0
hxy : x ^ 2 - ↑a * 0 ^ 2 = 0
⊢ False
[PROOFSTEP]
rw [zero_pow' 2 (by norm_num), mul_zero, sub_zero, pow_eq_zero_iff (by norm_num : 0 < 2)] at hxy
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x : ZMod p
hx : x ≠ 0
hxy : x ^ 2 - ↑a * 0 ^ 2 = 0
⊢ 2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x : ZMod p
hx : x ≠ 0
hxy : x ^ 2 = 0
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x : ZMod p
hx : x ≠ 0
hxy : x = 0
⊢ False
[PROOFSTEP]
exact hx hxy
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hx : x ≠ 0
hxy : x ^ 2 - ↑a * y ^ 2 = 0
hy : y ≠ 0
⊢ legendreSym p a = 1
[PROOFSTEP]
exact eq_one_of_sq_sub_mul_sq_eq_zero ha hy hxy
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
⊢ x = 0 ∧ y = 0
[PROOFSTEP]
have ha : (a : ZMod p) ≠ 0 := by
  intro hf
  rw [(eq_zero_iff p a).mpr hf] at h
  exact Int.zero_ne_neg_of_ne zero_ne_one h
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
⊢ ↑a ≠ 0
[PROOFSTEP]
intro hf
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
hf : ↑a = 0
⊢ False
[PROOFSTEP]
rw [(eq_zero_iff p a).mpr hf] at h
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : 0 = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
hf : ↑a = 0
⊢ False
[PROOFSTEP]
exact Int.zero_ne_neg_of_ne zero_ne_one h
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
⊢ x = 0 ∧ y = 0
[PROOFSTEP]
by_contra hf
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
hf : ¬(x = 0 ∧ y = 0)
⊢ False
[PROOFSTEP]
cases' imp_iff_or_not.mp (not_and'.mp hf) with hx hy
[GOAL]
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
hf : ¬(x = 0 ∧ y = 0)
hx : ¬x = 0
⊢ False
[PROOFSTEP]
rw [eq_one_of_sq_sub_mul_sq_eq_zero' ha hx hxy, eq_neg_self_iff] at h
[GOAL]
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : 1 = 0
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
hf : ¬(x = 0 ∧ y = 0)
hx : ¬x = 0
⊢ False
[PROOFSTEP]
exact one_ne_zero h
[GOAL]
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
hf : ¬(x = 0 ∧ y = 0)
hy : ¬y = 0
⊢ False
[PROOFSTEP]
rw [eq_one_of_sq_sub_mul_sq_eq_zero ha hy hxy, eq_neg_self_iff] at h
[GOAL]
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : 1 = 0
x y : ZMod p
hxy : x ^ 2 - ↑a * y ^ 2 = 0
ha : ↑a ≠ 0
hf : ¬(x = 0 ∧ y = 0)
hy : ¬y = 0
⊢ False
[PROOFSTEP]
exact one_ne_zero h
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : ↑p ∣ x ^ 2 - a * y ^ 2
⊢ ↑p ∣ x ∧ ↑p ∣ y
[PROOFSTEP]
simp_rw [← ZMod.int_cast_zmod_eq_zero_iff_dvd] at hxy ⊢
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : ↑(x ^ 2 - a * y ^ 2) = 0
⊢ ↑x = 0 ∧ ↑y = 0
[PROOFSTEP]
push_cast at hxy
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : ↑x ^ 2 - ↑a * ↑y ^ 2 = 0
⊢ ↑x = 0 ∧ ↑y = 0
[PROOFSTEP]
exact eq_zero_mod_of_eq_neg_one h hxy
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ legendreSym p (-1) = ↑χ₄ ↑p
[PROOFSTEP]
simp only [legendreSym, card p, quadraticChar_neg_one ((ringChar_zmod_n p).substr hp), Int.cast_neg, Int.cast_one]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsSquare (-1) ↔ p % 4 ≠ 3
[PROOFSTEP]
rw [FiniteField.isSquare_neg_one_iff, card p]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : x ^ 2 = -y ^ 2
⊢ (x / y) ^ 2 = -1
[PROOFSTEP]
apply_fun fun z => z / y ^ 2 at hxy
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : x ^ 2 / y ^ 2 = -y ^ 2 / y ^ 2
⊢ (x / y) ^ 2 = -1
[PROOFSTEP]
rwa [neg_div, ← div_pow, ← div_pow, div_self hy, one_pow] at hxy


[GOAL]
p : ℕ
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q = ↑p ^ (-padicValRat p q)
[PROOFSTEP]
simp [hq, padicNorm]
[GOAL]
p : ℕ
q : ℚ
hq : q = 0
⊢ 0 ≤ padicNorm p q
[PROOFSTEP]
simp [hq, padicNorm]
[GOAL]
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ padicNorm p q
[PROOFSTEP]
unfold padicNorm
[GOAL]
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ if q = 0 then 0 else ↑p ^ (-padicValRat p q)
[PROOFSTEP]
split_ifs
[GOAL]
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ ↑p ^ (-padicValRat p q)
[PROOFSTEP]
apply zpow_nonneg
[GOAL]
case ha
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ ↑p
[PROOFSTEP]
exact_mod_cast Nat.zero_le _
[GOAL]
p : ℕ
⊢ padicNorm p 0 = 0
[PROOFSTEP]
simp [padicNorm]
[GOAL]
p : ℕ
⊢ padicNorm p 1 = 1
[PROOFSTEP]
simp [padicNorm]
[GOAL]
p : ℕ
hp : 1 < p
⊢ padicNorm p ↑p = (↑p)⁻¹
[PROOFSTEP]
simp [padicNorm, (pos_of_gt hp).ne', padicValNat.self hp]
[GOAL]
p q : ℕ
p_prime : Fact (Nat.Prime p)
q_prime : Fact (Nat.Prime q)
neq : p ≠ q
⊢ padicNorm p ↑q = 1
[PROOFSTEP]
have p : padicValRat p q = 0 := by exact_mod_cast padicValNat_primes neq
[GOAL]
p q : ℕ
p_prime : Fact (Nat.Prime p)
q_prime : Fact (Nat.Prime q)
neq : p ≠ q
⊢ padicValRat p ↑q = 0
[PROOFSTEP]
exact_mod_cast padicValNat_primes neq
[GOAL]
p✝ q : ℕ
p_prime : Fact (Nat.Prime p✝)
q_prime : Fact (Nat.Prime q)
neq : p✝ ≠ q
p : padicValRat p✝ ↑q = 0
⊢ padicNorm p✝ ↑q = 1
[PROOFSTEP]
rw [padicNorm, p]
[GOAL]
p✝ q : ℕ
p_prime : Fact (Nat.Prime p✝)
q_prime : Fact (Nat.Prime q)
neq : p✝ ≠ q
p : padicValRat p✝ ↑q = 0
⊢ (if ↑q = 0 then 0 else ↑p✝ ^ (-0)) = 1
[PROOFSTEP]
simp [q_prime.1.ne_zero]
[GOAL]
p : ℕ
hp : 1 < p
⊢ padicNorm p ↑p < 1
[PROOFSTEP]
rw [padicNorm_p hp, inv_lt_one_iff]
[GOAL]
p : ℕ
hp : 1 < p
⊢ ↑p ≤ 0 ∨ 1 < ↑p
[PROOFSTEP]
exact_mod_cast Or.inr hp
[GOAL]
p : ℕ
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q = ↑p ^ (-padicValRat p q)
[PROOFSTEP]
simp [padicNorm, hq]
[GOAL]
p : ℕ
q : ℚ
hq : q = 0
⊢ padicNorm p (-q) = padicNorm p q
[PROOFSTEP]
simp [hq]
[GOAL]
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ padicNorm p (-q) = padicNorm p q
[PROOFSTEP]
simp [padicNorm, hq]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q ≠ 0
[PROOFSTEP]
rw [padicNorm.eq_zpow_of_nonzero hq]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑p ^ (-padicValRat p q) ≠ 0
[PROOFSTEP]
apply zpow_ne_zero_of_ne_zero
[GOAL]
case ha
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast ne_of_gt hp.1.pos
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : padicNorm p q = 0
⊢ q = 0
[PROOFSTEP]
apply by_contradiction
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : padicNorm p q = 0
⊢ ¬q = 0 → False
[PROOFSTEP]
intro hq
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : padicNorm p q = 0
hq : ¬q = 0
⊢ False
[PROOFSTEP]
unfold padicNorm at h
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : (if q = 0 then 0 else ↑p ^ (-padicValRat p q)) = 0
hq : ¬q = 0
⊢ False
[PROOFSTEP]
rw [if_neg hq] at h
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : ↑p ^ (-padicValRat p q) = 0
hq : ¬q = 0
⊢ False
[PROOFSTEP]
apply absurd h
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : ↑p ^ (-padicValRat p q) = 0
hq : ¬q = 0
⊢ ¬↑p ^ (-padicValRat p q) = 0
[PROOFSTEP]
apply zpow_ne_zero_of_ne_zero
[GOAL]
case a.ha
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : ↑p ^ (-padicValRat p q) = 0
hq : ¬q = 0
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast hp.1.ne_zero
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q = 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r
[PROOFSTEP]
simp [hq]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : r = 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r
[PROOFSTEP]
simp [hr]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : ¬r = 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r
[PROOFSTEP]
have : (p : ℚ) ≠ 0 := by simp [hp.1.ne_zero]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : ¬r = 0
⊢ ↑p ≠ 0
[PROOFSTEP]
simp [hp.1.ne_zero]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : ¬r = 0
this : ↑p ≠ 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r
[PROOFSTEP]
simp [padicNorm, *, padicValRat.mul, zpow_add₀ this, mul_comm]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hr : r = 0
⊢ padicNorm p (q / r) = padicNorm p q / padicNorm p r
[PROOFSTEP]
simp [hr]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hr : ¬r = 0
⊢ padicNorm p (q / r) * padicNorm p r = padicNorm p q
[PROOFSTEP]
rw [← padicNorm.mul, div_mul_cancel _ hr]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z = 0
⊢ padicNorm p ↑z ≤ 1
[PROOFSTEP]
simp [hz, zero_le_one]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : ¬z = 0
⊢ padicNorm p ↑z ≤ 1
[PROOFSTEP]
unfold padicNorm
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : ¬z = 0
⊢ (if ↑z = 0 then 0 else ↑p ^ (-padicValRat p ↑z)) ≤ 1
[PROOFSTEP]
rw [if_neg _]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : ¬z = 0
⊢ ↑p ^ (-padicValRat p ↑z) ≤ 1
[PROOFSTEP]
refine' zpow_le_one_of_nonpos _ _
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : ¬z = 0
⊢ 1 ≤ ↑p
[PROOFSTEP]
exact_mod_cast le_of_lt hp.1.one_lt
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : ¬z = 0
⊢ -padicValRat p ↑z ≤ 0
[PROOFSTEP]
rw [padicValRat.of_int, neg_nonpos]
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : ¬z = 0
⊢ 0 ≤ ↑(padicValInt p z)
[PROOFSTEP]
norm_cast
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : ¬z = 0
⊢ 0 ≤ padicValInt p z
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : ¬z = 0
⊢ ¬↑z = 0
[PROOFSTEP]
exact_mod_cast hz
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : q = 0
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
simp [hq, max_eq_right hnrp, le_max_right]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : r = 0
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
simp [hr, max_eq_left hnqp, le_max_left]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : q + r = 0
⊢ padicNorm p (q + r) ≤ padicNorm p q
[PROOFSTEP]
simpa [hqr] using hnqp
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
unfold padicNorm
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ (if q + r = 0 then 0 else ↑p ^ (-padicValRat p (q + r))) ≤
    max (if q = 0 then 0 else ↑p ^ (-padicValRat p q)) (if r = 0 then 0 else ↑p ^ (-padicValRat p r))
[PROOFSTEP]
split_ifs
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ ↑p ^ (-padicValRat p (q + r)) ≤ max (↑p ^ (-padicValRat p q)) (↑p ^ (-padicValRat p r))
[PROOFSTEP]
apply le_max_iff.2
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ ↑p ^ (-padicValRat p (q + r)) ≤ ↑p ^ (-padicValRat p q) ∨ ↑p ^ (-padicValRat p (q + r)) ≤ ↑p ^ (-padicValRat p r)
[PROOFSTEP]
left
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ ↑p ^ (-padicValRat p (q + r)) ≤ ↑p ^ (-padicValRat p q)
[PROOFSTEP]
apply zpow_le_of_le
[GOAL]
case h.ha
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ 1 ≤ ↑p
[PROOFSTEP]
exact_mod_cast le_of_lt hp.1.one_lt
[GOAL]
case h.h
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ -padicValRat p (q + r) ≤ -padicValRat p q
[PROOFSTEP]
apply neg_le_neg
[GOAL]
case h.h.a
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
[PROOFSTEP]
have : padicValRat p q = min (padicValRat p q) (padicValRat p r) := (min_eq_left h).symm
[GOAL]
case h.h.a
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
this : padicValRat p q = min (padicValRat p q) (padicValRat p r)
⊢ padicValRat p q ≤ padicValRat p (q + r)
[PROOFSTEP]
rw [this]
[GOAL]
case h.h.a
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
this : padicValRat p q = min (padicValRat p q) (padicValRat p r)
⊢ min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
[PROOFSTEP]
exact min_le_padicValRat_add hqr
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
wlog hle : padicValRat p q ≤ padicValRat p r generalizing q r
[GOAL]
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
rw [add_comm, max_comm]
[GOAL]
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (r + q) ≤ max (padicNorm p r) (padicNorm p q)
[PROOFSTEP]
exact this (le_of_not_le hle)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hle : padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
exact nonarchimedean_aux hle
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q - r) ≤ max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
rw [sub_eq_add_neg, ← padicNorm.neg r]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q + -r) ≤ max (padicNorm p q) (padicNorm p (-r))
[PROOFSTEP]
exact padicNorm.nonarchimedean
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
⊢ padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
wlog hlt : padicNorm p r < padicNorm p q
[GOAL]
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
this :
  ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ},
    padicNorm p q ≠ padicNorm p r →
      padicNorm p r < padicNorm p q → padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
hlt : ¬padicNorm p r < padicNorm p q
⊢ padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
rw [add_comm, max_comm]
[GOAL]
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
this :
  ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ},
    padicNorm p q ≠ padicNorm p r →
      padicNorm p r < padicNorm p q → padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
hlt : ¬padicNorm p r < padicNorm p q
⊢ padicNorm p (r + q) = max (padicNorm p r) (padicNorm p q)
[PROOFSTEP]
exact this hne.symm (hne.lt_or_lt.resolve_right hlt)
[GOAL]
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
⊢ padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
have : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r) :=
  calc
    padicNorm p q = padicNorm p (q + r + (-r)) := by ring_nf
    _ ≤ max (padicNorm p (q + r)) (padicNorm p (-r)) := padicNorm.nonarchimedean
    _ = max (padicNorm p (q + r)) (padicNorm p r) := by simp
[GOAL]
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
⊢ padicNorm p q = padicNorm p (q + r + -r)
[PROOFSTEP]
ring_nf
[GOAL]
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
⊢ max (padicNorm p (q + r)) (padicNorm p (-r)) = max (padicNorm p (q + r)) (padicNorm p r)
[PROOFSTEP]
simp
[GOAL]
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
⊢ padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
have hnge : padicNorm p r ≤ padicNorm p (q + r) :=
  by
  apply le_of_not_gt
  intro hgt
  rw [max_eq_right_of_lt hgt] at this
  exact not_lt_of_ge this hlt
[GOAL]
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
⊢ padicNorm p r ≤ padicNorm p (q + r)
[PROOFSTEP]
apply le_of_not_gt
[GOAL]
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
⊢ ¬padicNorm p r > padicNorm p (q + r)
[PROOFSTEP]
intro hgt
[GOAL]
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
hgt : padicNorm p r > padicNorm p (q + r)
⊢ False
[PROOFSTEP]
rw [max_eq_right_of_lt hgt] at this
[GOAL]
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ padicNorm p r
hgt : padicNorm p r > padicNorm p (q + r)
⊢ False
[PROOFSTEP]
exact not_lt_of_ge this hlt
[GOAL]
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
hnge : padicNorm p r ≤ padicNorm p (q + r)
⊢ padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
have : padicNorm p q ≤ padicNorm p (q + r) := by rwa [max_eq_left hnge] at this
[GOAL]
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
hnge : padicNorm p r ≤ padicNorm p (q + r)
⊢ padicNorm p q ≤ padicNorm p (q + r)
[PROOFSTEP]
rwa [max_eq_left hnge] at this
[GOAL]
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this✝ : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
hnge : padicNorm p r ≤ padicNorm p (q + r)
this : padicNorm p q ≤ padicNorm p (q + r)
⊢ padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
apply _root_.le_antisymm
[GOAL]
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this✝ : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
hnge : padicNorm p r ≤ padicNorm p (q + r)
this : padicNorm p q ≤ padicNorm p (q + r)
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
[PROOFSTEP]
apply padicNorm.nonarchimedean
[GOAL]
case a
p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
this✝ : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r)
hnge : padicNorm p r ≤ padicNorm p (q + r)
this : padicNorm p q ≤ padicNorm p (q + r)
⊢ max (padicNorm p q) (padicNorm p r) ≤ padicNorm p (q + r)
[PROOFSTEP]
rwa [max_eq_left_of_lt hlt]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x✝ : ℚ
hx : x✝ = 0
⊢ padicNorm p x✝ = 0
[PROOFSTEP]
simp [hx]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
⊢ ↑(p ^ n) ∣ z ↔ padicNorm p ↑z ≤ ↑p ^ (-↑n)
[PROOFSTEP]
unfold padicNorm
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
⊢ ↑(p ^ n) ∣ z ↔ (if ↑z = 0 then 0 else ↑p ^ (-padicValRat p ↑z)) ≤ ↑p ^ (-↑n)
[PROOFSTEP]
split_ifs with hz
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ 0 ≤ ↑p ^ (-↑n)
[PROOFSTEP]
norm_cast at hz
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : z = 0
⊢ ↑(p ^ n) ∣ z ↔ 0 ≤ ↑p ^ (-↑n)
[PROOFSTEP]
simp [hz]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑p ^ (-padicValRat p ↑z) ≤ ↑p ^ (-↑n)
[PROOFSTEP]
rw [zpow_le_iff_le, neg_le_neg_iff, padicValRat.of_int, padicValInt.of_ne_one_ne_zero hp.1.ne_one _]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑n ≤ ↑(Part.get (multiplicity (↑p) z) (_ : multiplicity.Finite (↑p) z))
[PROOFSTEP]
norm_cast
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ n ≤ Part.get (multiplicity (↑p) z) (_ : multiplicity.Finite (↑p) z)
[PROOFSTEP]
rw [← PartENat.coe_le_coe, PartENat.natCast_get, ← multiplicity.pow_dvd_iff_le_multiplicity, Nat.cast_pow]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ z ≠ 0
p : ℕ hp : Fact (Nat.Prime p) n : ℕ z : ℤ hz : ¬↑z = 0 ⊢ z ≠ 0
[PROOFSTEP]
exact_mod_cast hz
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ 1 < ↑p
[PROOFSTEP]
exact_mod_cast hp.1.one_lt
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m = 1 ↔ ¬↑p ∣ m
[PROOFSTEP]
nth_rw 2 [← pow_one p]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m = 1 ↔ ¬↑(p ^ 1) ∣ m
[PROOFSTEP]
simp only [dvd_iff_norm_le, Int.cast_ofNat, Nat.cast_one, zpow_neg, zpow_one, not_le]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m = 1 ↔ (↑p)⁻¹ < padicNorm p ↑m
[PROOFSTEP]
constructor
[GOAL]
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m = 1 → (↑p)⁻¹ < padicNorm p ↑m
[PROOFSTEP]
intro h
[GOAL]
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ (↑p)⁻¹ < padicNorm p ↑m
[PROOFSTEP]
rw [h, inv_lt_one_iff_of_pos]
[GOAL]
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 1 < ↑p
[PROOFSTEP]
norm_cast
[GOAL]
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 0 < ↑p
[PROOFSTEP]
norm_cast
[GOAL]
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 1 < p
[PROOFSTEP]
exact Nat.Prime.one_lt Fact.out
[GOAL]
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 0 < p
[PROOFSTEP]
exact Nat.Prime.pos Fact.out
[GOAL]
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ (↑p)⁻¹ < padicNorm p ↑m → padicNorm p ↑m = 1
[PROOFSTEP]
simp only [padicNorm]
[GOAL]
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ ((↑p)⁻¹ < if ↑m = 0 then 0 else ↑p ^ (-padicValRat p ↑m)) → (if ↑m = 0 then 0 else ↑p ^ (-padicValRat p ↑m)) = 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ↑m = 0
⊢ (↑p)⁻¹ < 0 → 0 = 1
[PROOFSTEP]
rw [inv_lt_zero, ← Nat.cast_zero, Nat.cast_lt]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ↑m = 0
⊢ p < 0 → ↑0 = 1
[PROOFSTEP]
intro h
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ↑m = 0
h : p < 0
⊢ ↑0 = 1
[PROOFSTEP]
exact (Nat.not_lt_zero p h).elim
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
⊢ (↑p)⁻¹ < ↑p ^ (-padicValRat p ↑m) → ↑p ^ (-padicValRat p ↑m) = 1
[PROOFSTEP]
have : 1 < (p : ℚ) := by norm_cast; exact Nat.Prime.one_lt (Fact.out : Nat.Prime p)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
⊢ 1 < ↑p
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
⊢ 1 < p
[PROOFSTEP]
exact Nat.Prime.one_lt (Fact.out : Nat.Prime p)
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this : 1 < ↑p
⊢ (↑p)⁻¹ < ↑p ^ (-padicValRat p ↑m) → ↑p ^ (-padicValRat p ↑m) = 1
[PROOFSTEP]
rw [← zpow_neg_one, zpow_lt_iff_lt this]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this : 1 < ↑p
⊢ -1 < -padicValRat p ↑m → ↑p ^ (-padicValRat p ↑m) = 1
[PROOFSTEP]
have : 0 ≤ padicValRat p m
[GOAL]
case this
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this : 1 < ↑p
⊢ 0 ≤ padicValRat p ↑m
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
⊢ -1 < -padicValRat p ↑m → ↑p ^ (-padicValRat p ↑m) = 1
[PROOFSTEP]
simp only [of_int, Nat.cast_nonneg]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
⊢ -1 < -padicValRat p ↑m → ↑p ^ (-padicValRat p ↑m) = 1
[PROOFSTEP]
intro h
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ ↑p ^ (-padicValRat p ↑m) = 1
[PROOFSTEP]
rw [← zpow_zero (p : ℚ), zpow_inj]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ -padicValRat p ↑m = 0
[PROOFSTEP]
linarith
[GOAL]
case neg.h₀
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ 0 < ↑p
[PROOFSTEP]
linarith
[GOAL]
case neg.h₁
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
this✝ : 1 < ↑p
this : 0 ≤ padicValRat p ↑m
h : -1 < -padicValRat p ↑m
⊢ ↑p ≠ 1
[PROOFSTEP]
linarith
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m < 1 ↔ ↑p ∣ m
[PROOFSTEP]
rw [← not_iff_not, ← int_eq_one_iff, eq_iff_le_not_lt]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ ¬padicNorm p ↑m < 1 ↔ padicNorm p ↑m ≤ 1 ∧ ¬padicNorm p ↑m < 1
[PROOFSTEP]
simp only [padicNorm.of_int, true_and_iff]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p ↑m = 1 ↔ ¬p ∣ m
[PROOFSTEP]
rw [← Int.coe_nat_dvd, ← int_eq_one_iff, Int.cast_ofNat]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p ↑m < 1 ↔ p ∣ m
[PROOFSTEP]
rw [← Int.coe_nat_dvd, ← int_lt_one_iff, Int.cast_ofNat]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ Finset.Nonempty s → (∀ (i : α), i ∈ s → padicNorm p (F i) < t) → padicNorm p (∑ i in s, F i) < t
[PROOFSTEP]
classical
refine' s.induction_on (by rintro ⟨-, ⟨⟩⟩) _
rintro a S haS IH - ht
by_cases hs : S.Nonempty
· rw [Finset.sum_insert haS]
  exact
    lt_of_le_of_lt padicNorm.nonarchimedean
      (max_lt (ht a (Finset.mem_insert_self a S)) (IH hs fun b hb ↦ ht b (Finset.mem_insert_of_mem hb)))
· simp_all
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ Finset.Nonempty s → (∀ (i : α), i ∈ s → padicNorm p (F i) < t) → padicNorm p (∑ i in s, F i) < t
[PROOFSTEP]
refine' s.induction_on (by rintro ⟨-, ⟨⟩⟩) _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ Finset.Nonempty ∅ → (∀ (i : α), i ∈ ∅ → padicNorm p (F i) < t) → padicNorm p (∑ i in ∅, F i) < t
[PROOFSTEP]
rintro ⟨-, ⟨⟩⟩
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (Finset.Nonempty s → (∀ (i : α), i ∈ s → padicNorm p (F i) < t) → padicNorm p (∑ i in s, F i) < t) →
        Finset.Nonempty (insert a s) →
          (∀ (i : α), i ∈ insert a s → padicNorm p (F i) < t) → padicNorm p (∑ i in insert a s, F i) < t
[PROOFSTEP]
rintro a S haS IH - ht
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : ¬a ∈ S
IH : Finset.Nonempty S → (∀ (i : α), i ∈ S → padicNorm p (F i) < t) → padicNorm p (∑ i in S, F i) < t
ht : ∀ (i : α), i ∈ insert a S → padicNorm p (F i) < t
⊢ padicNorm p (∑ i in insert a S, F i) < t
[PROOFSTEP]
by_cases hs : S.Nonempty
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : ¬a ∈ S
IH : Finset.Nonempty S → (∀ (i : α), i ∈ S → padicNorm p (F i) < t) → padicNorm p (∑ i in S, F i) < t
ht : ∀ (i : α), i ∈ insert a S → padicNorm p (F i) < t
hs : Finset.Nonempty S
⊢ padicNorm p (∑ i in insert a S, F i) < t
[PROOFSTEP]
rw [Finset.sum_insert haS]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : ¬a ∈ S
IH : Finset.Nonempty S → (∀ (i : α), i ∈ S → padicNorm p (F i) < t) → padicNorm p (∑ i in S, F i) < t
ht : ∀ (i : α), i ∈ insert a S → padicNorm p (F i) < t
hs : Finset.Nonempty S
⊢ padicNorm p (F a + ∑ x in S, F x) < t
[PROOFSTEP]
exact
  lt_of_le_of_lt padicNorm.nonarchimedean
    (max_lt (ht a (Finset.mem_insert_self a S)) (IH hs fun b hb ↦ ht b (Finset.mem_insert_of_mem hb)))
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : ¬a ∈ S
IH : Finset.Nonempty S → (∀ (i : α), i ∈ S → padicNorm p (F i) < t) → padicNorm p (∑ i in S, F i) < t
ht : ∀ (i : α), i ∈ insert a S → padicNorm p (F i) < t
hs : ¬Finset.Nonempty S
⊢ padicNorm p (∑ i in insert a S, F i) < t
[PROOFSTEP]
simp_all
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ Finset.Nonempty s → (∀ (i : α), i ∈ s → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in s, F i) ≤ t
[PROOFSTEP]
classical
refine' s.induction_on (by rintro ⟨-, ⟨⟩⟩) _
rintro a S haS IH - ht
by_cases hs : S.Nonempty
· rw [Finset.sum_insert haS]
  exact
    padicNorm.nonarchimedean.trans
      (max_le (ht a (Finset.mem_insert_self a S)) (IH hs fun b hb ↦ ht b (Finset.mem_insert_of_mem hb)))
· simp_all
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ Finset.Nonempty s → (∀ (i : α), i ∈ s → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in s, F i) ≤ t
[PROOFSTEP]
refine' s.induction_on (by rintro ⟨-, ⟨⟩⟩) _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ Finset.Nonempty ∅ → (∀ (i : α), i ∈ ∅ → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in ∅, F i) ≤ t
[PROOFSTEP]
rintro ⟨-, ⟨⟩⟩
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (Finset.Nonempty s → (∀ (i : α), i ∈ s → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in s, F i) ≤ t) →
        Finset.Nonempty (insert a s) →
          (∀ (i : α), i ∈ insert a s → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in insert a s, F i) ≤ t
[PROOFSTEP]
rintro a S haS IH - ht
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : ¬a ∈ S
IH : Finset.Nonempty S → (∀ (i : α), i ∈ S → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in S, F i) ≤ t
ht : ∀ (i : α), i ∈ insert a S → padicNorm p (F i) ≤ t
⊢ padicNorm p (∑ i in insert a S, F i) ≤ t
[PROOFSTEP]
by_cases hs : S.Nonempty
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : ¬a ∈ S
IH : Finset.Nonempty S → (∀ (i : α), i ∈ S → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in S, F i) ≤ t
ht : ∀ (i : α), i ∈ insert a S → padicNorm p (F i) ≤ t
hs : Finset.Nonempty S
⊢ padicNorm p (∑ i in insert a S, F i) ≤ t
[PROOFSTEP]
rw [Finset.sum_insert haS]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : ¬a ∈ S
IH : Finset.Nonempty S → (∀ (i : α), i ∈ S → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in S, F i) ≤ t
ht : ∀ (i : α), i ∈ insert a S → padicNorm p (F i) ≤ t
hs : Finset.Nonempty S
⊢ padicNorm p (F a + ∑ x in S, F x) ≤ t
[PROOFSTEP]
exact
  padicNorm.nonarchimedean.trans
    (max_le (ht a (Finset.mem_insert_self a S)) (IH hs fun b hb ↦ ht b (Finset.mem_insert_of_mem hb)))
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
a : α
S : Finset α
haS : ¬a ∈ S
IH : Finset.Nonempty S → (∀ (i : α), i ∈ S → padicNorm p (F i) ≤ t) → padicNorm p (∑ i in S, F i) ≤ t
ht : ∀ (i : α), i ∈ insert a S → padicNorm p (F i) ≤ t
hs : ¬Finset.Nonempty S
⊢ padicNorm p (∑ i in insert a S, F i) ≤ t
[PROOFSTEP]
simp_all
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ (i : α), i ∈ s → padicNorm p (F i) < t
ht : 0 < t
⊢ padicNorm p (∑ i in s, F i) < t
[PROOFSTEP]
obtain rfl | hs := Finset.eq_empty_or_nonempty s
[GOAL]
case inl
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
ht : 0 < t
hF : ∀ (i : α), i ∈ ∅ → padicNorm p (F i) < t
⊢ padicNorm p (∑ i in ∅, F i) < t
[PROOFSTEP]
simp [ht]
[GOAL]
case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ (i : α), i ∈ s → padicNorm p (F i) < t
ht : 0 < t
hs : Finset.Nonempty s
⊢ padicNorm p (∑ i in s, F i) < t
[PROOFSTEP]
exact sum_lt hs hF
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ (i : α), i ∈ s → padicNorm p (F i) ≤ t
ht : 0 ≤ t
⊢ padicNorm p (∑ i in s, F i) ≤ t
[PROOFSTEP]
obtain rfl | hs := Finset.eq_empty_or_nonempty s
[GOAL]
case inl
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
ht : 0 ≤ t
hF : ∀ (i : α), i ∈ ∅ → padicNorm p (F i) ≤ t
⊢ padicNorm p (∑ i in ∅, F i) ≤ t
[PROOFSTEP]
simp [ht]
[GOAL]
case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ (i : α), i ∈ s → padicNorm p (F i) ≤ t
ht : 0 ≤ t
hs : Finset.Nonempty s
⊢ padicNorm p (∑ i in s, F i) ≤ t
[PROOFSTEP]
exact sum_le hs hF