[GOAL]
R : Type u₁
inst✝¹ : CommRing R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
n : ℕ
⊢ (-1) (n + 1) ^ p = (-1) n
[PROOFSTEP]
simp_rw [← frobenius_def, Pi.neg_apply, Pi.one_apply, RingHom.map_neg, RingHom.map_one]
[GOAL]
R : Type u₁
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
f : Ring.Perfection R p
n : ℕ
⊢ ↑(coeff R p (n + 1)) (f ^ p) = ↑(coeff R p n) f
[PROOFSTEP]
rw [RingHom.map_pow]
[GOAL]
R : Type u₁
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
f : Ring.Perfection R p
n : ℕ
⊢ ↑(coeff R p (n + 1)) f ^ p = ↑(coeff R p n) f
[PROOFSTEP]
exact f.2 n
[GOAL]
R : Type u₁
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
f : Ring.Perfection R p
n : ℕ
⊢ ↑(coeff R p (n + 1)) (↑(frobenius (Ring.Perfection R p) p) f) = ↑(coeff R p n) f
[PROOFSTEP]
apply coeff_pow_p f n
[GOAL]
R : Type u₁
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
f : Ring.Perfection R p
n m✝ m : ℕ
ih : ↑(coeff R p (n + m)) ((↑(frobenius (Ring.Perfection R p) p))^[m] f) = ↑(coeff R p n) f
⊢ ↑(coeff R p (n + Nat.succ m)) ((↑(frobenius (Ring.Perfection R p) p))^[Nat.succ m] f) = ↑(coeff R p n) f
[PROOFSTEP]
erw [Function.iterate_succ_apply', coeff_frobenius, ih]
[GOAL]
R : Type u₁
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x : Ring.Perfection R p
n : ℕ
⊢ ↑(coeff R p n) (↑(RingHom.comp (pthRoot R p) (frobenius (Ring.Perfection R p) p)) x) =
    ↑(coeff R p n) (↑(RingHom.id (Ring.Perfection R p)) x)
[PROOFSTEP]
rw [RingHom.comp_apply, RingHom.id_apply, coeff_pthRoot, coeff_frobenius]
[GOAL]
R : Type u₁
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x : Ring.Perfection R p
n : ℕ
⊢ ↑(coeff R p n) (↑(RingHom.comp (frobenius (Ring.Perfection R p) p) (pthRoot R p)) x) =
    ↑(coeff R p n) (↑(RingHom.id (Ring.Perfection R p)) x)
[PROOFSTEP]
rw [RingHom.comp_apply, RingHom.id_apply, RingHom.map_frobenius, coeff_pthRoot, ←
  @RingHom.map_frobenius (Ring.Perfection R p) _ R, coeff_frobenius]
[GOAL]
R : Type u₁
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
f : Ring.Perfection R p
n : ℕ
hfn : ↑(coeff R p n) f ≠ 0
k✝ k : ℕ
ih : ↑(coeff R p (n + k)) f ≠ 0
h : ↑(coeff R p (n + Nat.succ k)) f = 0
⊢ ↑(coeff R p (n + k)) f = 0
[PROOFSTEP]
erw [← coeff_pow_p, RingHom.map_pow, h, zero_pow hp.1.pos]
[GOAL]
R✝ : Type u₁
inst✝⁶ : CommSemiring R✝
p : ℕ
hp : Fact (Nat.Prime p)
inst✝⁵ : CharP R✝ p
R : Type u₁
inst✝⁴ : CommSemiring R
inst✝³ : CharP R p
inst✝² : PerfectRing R p
S : Type u₂
inst✝¹ : CommSemiring S
inst✝ : CharP S p
f : R →+* S
r : R
n : ℕ
⊢ (fun n => ↑f ((↑↑(RingEquiv.symm (frobeniusEquiv R p)))^[n] r)) (n + 1) ^ p =
    (fun n => ↑f ((↑↑(RingEquiv.symm (frobeniusEquiv R p)))^[n] r)) n
[PROOFSTEP]
erw [← f.map_pow, Function.iterate_succ_apply', frobeniusEquiv_symm_pow_p]
[GOAL]
R✝ : Type u₁
inst✝⁶ : CommSemiring R✝
p : ℕ
hp : Fact (Nat.Prime p)
inst✝⁵ : CharP R✝ p
R : Type u₁
inst✝⁴ : CommSemiring R
inst✝³ : CharP R p
inst✝² : PerfectRing R p
S : Type u₂
inst✝¹ : CommSemiring S
inst✝ : CharP S p
f : R →+* Ring.Perfection S p
r : R
n : ℕ
⊢ ↑(coeff S p 0) (↑f ((↑(RingEquiv.symm (frobeniusEquiv R p)))^[n] r)) = ↑(coeff S p n) (↑f r)
[PROOFSTEP]
rw [← coeff_iterate_frobenius _ 0 n, zero_add, ← RingHom.map_iterate_frobenius,
  Function.RightInverse.iterate (frobenius_apply_frobeniusEquiv_symm R p) n]
[GOAL]
R : Type u₁
inst✝³ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝² : CharP R p
S : Type u₂
inst✝¹ : CommSemiring S
inst✝ : CharP S p
φ : R →+* S
f : Ring.Perfection R p
n : ℕ
⊢ (fun n => ↑φ (↑(coeff R p n) f)) (n + 1) ^ p = (fun n => ↑φ (↑(coeff R p n) f)) n
[PROOFSTEP]
rw [← φ.map_pow, coeff_pow_p']
[GOAL]
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
R : Type u₁
inst✝⁴ : CommSemiring R
inst✝³ : CharP R p
P : Type u₃
inst✝² : CommSemiring P
inst✝¹ : CharP P p
inst✝ : PerfectRing P p
f : P →+* R
g : P ≃+* Ring.Perfection R p
hfg : ↑(Perfection.lift p P R) f = ↑g
y : ℕ → R
hy : ∀ (n : ℕ), y (n + 1) ^ p = y n
x : P
hx : ↑g x = { val := y, property := hy }
n : ℕ
⊢ ↑(Perfection.coeff R p n) (↑(↑(Perfection.lift p P R) f) x) = ↑(Perfection.coeff R p n) { val := y, property := hy }
[PROOFSTEP]
simp [hfg, hx]
[GOAL]
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
R : Type u₁
inst✝⁵ : CommSemiring R
inst✝⁴ : CharP R p
P : Type u₃
inst✝³ : CommSemiring P
inst✝² : CharP P p
inst✝¹ : PerfectRing P p
inst✝ : PerfectRing R p
f : ℕ → R
hf : ∀ (n : ℕ), f (n + 1) ^ p = f n
n✝ n : ℕ
ih : (↑(RingEquiv.symm (frobeniusEquiv R p)))^[n] (f 0) = f n
⊢ (↑(RingEquiv.symm (frobeniusEquiv R p)))^[Nat.succ n] (f 0) ^ p = f (Nat.succ n) ^ p
[PROOFSTEP]
rw [Function.iterate_succ_apply', frobeniusEquiv_symm_pow_p, ih, hf]
[GOAL]
p : ℕ
inst✝¹¹ : Fact (Nat.Prime p)
R : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CharP R p
P✝ : Type u₃
inst✝⁸ : CommSemiring P✝
inst✝⁷ : CharP P✝ p
inst✝⁶ : PerfectRing P✝ p
inst✝⁵ : PerfectRing R p
S : Type u₂
inst✝⁴ : CommSemiring S
inst✝³ : CharP S p
P : Type u₃
inst✝² : CommSemiring P
inst✝¹ : CharP P p
inst✝ : PerfectRing P p
π : P →+* S
m : PerfectionMap p π
f : R →+* S
⊢ (fun f => RingHom.comp π f) ((fun f => RingHom.comp (↑(RingEquiv.symm (equiv m))) (↑(Perfection.lift p R S) f)) f) = f
[PROOFSTEP]
simp_rw [← RingHom.comp_assoc, comp_symm_equiv']
[GOAL]
p : ℕ
inst✝¹¹ : Fact (Nat.Prime p)
R : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CharP R p
P✝ : Type u₃
inst✝⁸ : CommSemiring P✝
inst✝⁷ : CharP P✝ p
inst✝⁶ : PerfectRing P✝ p
inst✝⁵ : PerfectRing R p
S : Type u₂
inst✝⁴ : CommSemiring S
inst✝³ : CharP S p
P : Type u₃
inst✝² : CommSemiring P
inst✝¹ : CharP P p
inst✝ : PerfectRing P p
π : P →+* S
m : PerfectionMap p π
f : R →+* S
⊢ RingHom.comp (Perfection.coeff S p 0) (↑(Perfection.lift p R S) f) = f
[PROOFSTEP]
exact (Perfection.lift p R S).symm_apply_apply f
[GOAL]
p : ℕ
inst✝¹¹ : Fact (Nat.Prime p)
R : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CharP R p
P✝ : Type u₃
inst✝⁸ : CommSemiring P✝
inst✝⁷ : CharP P✝ p
inst✝⁶ : PerfectRing P✝ p
inst✝⁵ : PerfectRing R p
S : Type u₂
inst✝⁴ : CommSemiring S
inst✝³ : CharP S p
P : Type u₃
inst✝² : CommSemiring P
inst✝¹ : CharP P p
inst✝ : PerfectRing P p
π : P →+* S
m : PerfectionMap p π
f : R →+* P
⊢ (fun f => RingHom.comp (↑(RingEquiv.symm (equiv m))) (↑(Perfection.lift p R S) f)) ((fun f => RingHom.comp π f) f) = f
[PROOFSTEP]
exact
  RingHom.ext fun x =>
    m.equiv.injective <|
      (m.equiv.apply_symm_apply _).trans <|
        show Perfection.lift p R S (π.comp f) x = RingHom.comp (↑m.equiv) f x from
          RingHom.ext_iff.1 (by rw [Equiv.apply_eq_iff_eq_symm_apply]; rfl) _
[GOAL]
p : ℕ
inst✝¹¹ : Fact (Nat.Prime p)
R : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CharP R p
P✝ : Type u₃
inst✝⁸ : CommSemiring P✝
inst✝⁷ : CharP P✝ p
inst✝⁶ : PerfectRing P✝ p
inst✝⁵ : PerfectRing R p
S : Type u₂
inst✝⁴ : CommSemiring S
inst✝³ : CharP S p
P : Type u₃
inst✝² : CommSemiring P
inst✝¹ : CharP P p
inst✝ : PerfectRing P p
π : P →+* S
m : PerfectionMap p π
f : R →+* P
x : R
⊢ ↑(Perfection.lift p R S) (RingHom.comp π f) = RingHom.comp (↑(equiv m)) f
[PROOFSTEP]
rw [Equiv.apply_eq_iff_eq_symm_apply]
[GOAL]
p : ℕ
inst✝¹¹ : Fact (Nat.Prime p)
R : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CharP R p
P✝ : Type u₃
inst✝⁸ : CommSemiring P✝
inst✝⁷ : CharP P✝ p
inst✝⁶ : PerfectRing P✝ p
inst✝⁵ : PerfectRing R p
S : Type u₂
inst✝⁴ : CommSemiring S
inst✝³ : CharP S p
P : Type u₃
inst✝² : CommSemiring P
inst✝¹ : CharP P p
inst✝ : PerfectRing P p
π : P →+* S
m : PerfectionMap p π
f : R →+* P
x : R
⊢ RingHom.comp π f = ↑(Perfection.lift p R S).symm (RingHom.comp (↑(equiv m)) f)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
inst✝¹⁰ : Fact (Nat.Prime p)
R : Type u₁
inst✝⁹ : CommSemiring R
inst✝⁸ : CharP R p
P : Type u₃
inst✝⁷ : CommSemiring P
inst✝⁶ : CharP P p
inst✝⁵ : PerfectRing P p
S : Type u₂
inst✝⁴ : CommSemiring S
inst✝³ : CharP S p
Q : Type u₄
inst✝² : CommSemiring Q
inst✝¹ : CharP Q p
inst✝ : PerfectRing Q p
φ : R →+* S
f : Ring.Perfection R p
⊢ ↑(Perfection.coeff S p 0)
      (↑(map p (_ : PerfectionMap p (Perfection.coeff R p 0)) (_ : PerfectionMap p (Perfection.coeff S p 0)) φ) f) =
    ↑(Perfection.coeff S p 0) (↑(Perfection.map p φ) f)
[PROOFSTEP]
rw [map_map, Perfection.coeff_map]
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x : O
hx : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
⊢ preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) x) = ↑v (↑(algebraMap O K) x)
[PROOFSTEP]
obtain ⟨r, hr⟩ : ∃ (a : O), a * (p : O) = (Quotient.mk'' x).out' - x :=
  Ideal.mem_span_singleton'.1 <| Ideal.Quotient.eq.1 <| Quotient.sound' <| Quotient.mk_out' _
[GOAL]
case intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x : O
hx : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
r : O
hr : r * ↑p = Quotient.out' (Quotient.mk'' x) - x
⊢ preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) x) = ↑v (↑(algebraMap O K) x)
[PROOFSTEP]
refine' (if_neg hx).trans (v.map_eq_of_sub_lt <| lt_of_not_le _)
[GOAL]
case intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x : O
hx : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
r : O
hr : r * ↑p = Quotient.out' (Quotient.mk'' x) - x
⊢ ¬↑v (↑(algebraMap O K) x) ≤
      ↑v (↑(algebraMap O K) (Quotient.out' (↑(Ideal.Quotient.mk (Ideal.span {↑p})) x)) - ↑(algebraMap O K) x)
[PROOFSTEP]
erw [← RingHom.map_sub, ← hr, hv.le_iff_dvd]
[GOAL]
case intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x : O
hx : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
r : O
hr : r * ↑p = Quotient.out' (Quotient.mk'' x) - x
⊢ ¬r * ↑p ∣ x
[PROOFSTEP]
exact fun hprx => hx (Ideal.Quotient.eq_zero_iff_mem.2 <| Ideal.mem_span_singleton.2 <| dvd_of_mul_left_dvd hprx)
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x y : ModP K v O hv p
hxy0 : x * y ≠ 0
⊢ preVal K v O hv p (x * y) = preVal K v O hv p x * preVal K v O hv p y
[PROOFSTEP]
have hx0 : x ≠ 0 := mt (by rintro rfl; rw [zero_mul]) hxy0
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x y : ModP K v O hv p
hxy0 : x * y ≠ 0
⊢ x = 0 → x * y = 0
[PROOFSTEP]
rintro rfl
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
y : ModP K v O hv p
hxy0 : 0 * y ≠ 0
⊢ 0 * y = 0
[PROOFSTEP]
rw [zero_mul]
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x y : ModP K v O hv p
hxy0 : x * y ≠ 0
hx0 : x ≠ 0
⊢ preVal K v O hv p (x * y) = preVal K v O hv p x * preVal K v O hv p y
[PROOFSTEP]
have hy0 : y ≠ 0 := mt (by rintro rfl; rw [mul_zero]) hxy0
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x y : ModP K v O hv p
hxy0 : x * y ≠ 0
hx0 : x ≠ 0
⊢ y = 0 → x * y = 0
[PROOFSTEP]
rintro rfl
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x : ModP K v O hv p
hx0 : x ≠ 0
hxy0 : x * 0 ≠ 0
⊢ x * 0 = 0
[PROOFSTEP]
rw [mul_zero]
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x y : ModP K v O hv p
hxy0 : x * y ≠ 0
hx0 : x ≠ 0
hy0 : y ≠ 0
⊢ preVal K v O hv p (x * y) = preVal K v O hv p x * preVal K v O hv p y
[PROOFSTEP]
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
[GOAL]
case intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
y : ModP K v O hv p
hy0 : y ≠ 0
r : O
hxy0 : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) r * y ≠ 0
hx0 : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
⊢ preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) r * y) =
    preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) r) * preVal K v O hv p y
[PROOFSTEP]
obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y
[GOAL]
case intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
r : O
hx0 : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
s : O
hy0 : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
hxy0 : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) r * ↑(Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
⊢ preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) r * ↑(Ideal.Quotient.mk (Ideal.span {↑p})) s) =
    preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) r) *
      preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) s)
[PROOFSTEP]
rw [← RingHom.map_mul] at hxy0 ⊢
[GOAL]
case intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
r : O
hx0 : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
s : O
hy0 : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
hxy0 : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) (r * s) ≠ 0
⊢ preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) (r * s)) =
    preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) r) *
      preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) s)
[PROOFSTEP]
rw [preVal_mk hx0, preVal_mk hy0, preVal_mk hxy0, RingHom.map_mul, v.map_mul]
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x y : ModP K v O hv p
⊢ preVal K v O hv p (x + y) ≤ max (preVal K v O hv p x) (preVal K v O hv p y)
[PROOFSTEP]
by_cases hx0 : x = 0
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x y : ModP K v O hv p
hx0 : x = 0
⊢ preVal K v O hv p (x + y) ≤ max (preVal K v O hv p x) (preVal K v O hv p y)
[PROOFSTEP]
rw [hx0, zero_add]
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x y : ModP K v O hv p
hx0 : x = 0
⊢ preVal K v O hv p y ≤ max (preVal K v O hv p 0) (preVal K v O hv p y)
[PROOFSTEP]
exact le_max_right _ _
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x y : ModP K v O hv p
hx0 : ¬x = 0
⊢ preVal K v O hv p (x + y) ≤ max (preVal K v O hv p x) (preVal K v O hv p y)
[PROOFSTEP]
by_cases hy0 : y = 0
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x y : ModP K v O hv p
hx0 : ¬x = 0
hy0 : y = 0
⊢ preVal K v O hv p (x + y) ≤ max (preVal K v O hv p x) (preVal K v O hv p y)
[PROOFSTEP]
rw [hy0, add_zero]
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x y : ModP K v O hv p
hx0 : ¬x = 0
hy0 : y = 0
⊢ preVal K v O hv p x ≤ max (preVal K v O hv p x) (preVal K v O hv p 0)
[PROOFSTEP]
exact le_max_left _ _
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x y : ModP K v O hv p
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ preVal K v O hv p (x + y) ≤ max (preVal K v O hv p x) (preVal K v O hv p y)
[PROOFSTEP]
by_cases hxy0 : x + y = 0
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x y : ModP K v O hv p
hx0 : ¬x = 0
hy0 : ¬y = 0
hxy0 : x + y = 0
⊢ preVal K v O hv p (x + y) ≤ max (preVal K v O hv p x) (preVal K v O hv p y)
[PROOFSTEP]
rw [hxy0, preVal_zero]
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x y : ModP K v O hv p
hx0 : ¬x = 0
hy0 : ¬y = 0
hxy0 : x + y = 0
⊢ 0 ≤ max (preVal K v O hv p x) (preVal K v O hv p y)
[PROOFSTEP]
exact zero_le _
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x y : ModP K v O hv p
hx0 : ¬x = 0
hy0 : ¬y = 0
hxy0 : ¬x + y = 0
⊢ preVal K v O hv p (x + y) ≤ max (preVal K v O hv p x) (preVal K v O hv p y)
[PROOFSTEP]
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
[GOAL]
case neg.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
y : ModP K v O hv p
hy0 : ¬y = 0
r : O
hx0 : ¬↑(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0
hxy0 : ¬↑(Ideal.Quotient.mk (Ideal.span {↑p})) r + y = 0
⊢ preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) r + y) ≤
    max (preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) r)) (preVal K v O hv p y)
[PROOFSTEP]
obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y
[GOAL]
case neg.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
r : O
hx0 : ¬↑(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0
s : O
hy0 : ¬↑(Ideal.Quotient.mk (Ideal.span {↑p})) s = 0
hxy0 : ¬↑(Ideal.Quotient.mk (Ideal.span {↑p})) r + ↑(Ideal.Quotient.mk (Ideal.span {↑p})) s = 0
⊢ preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) r + ↑(Ideal.Quotient.mk (Ideal.span {↑p})) s) ≤
    max (preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) r))
      (preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) s))
[PROOFSTEP]
rw [← RingHom.map_add] at hxy0 ⊢
[GOAL]
case neg.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
r : O
hx0 : ¬↑(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0
s : O
hy0 : ¬↑(Ideal.Quotient.mk (Ideal.span {↑p})) s = 0
hxy0 : ¬↑(Ideal.Quotient.mk (Ideal.span {↑p})) (r + s) = 0
⊢ preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) (r + s)) ≤
    max (preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) r))
      (preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) s))
[PROOFSTEP]
rw [preVal_mk hx0, preVal_mk hy0, preVal_mk hxy0, RingHom.map_add]
[GOAL]
case neg.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
r : O
hx0 : ¬↑(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0
s : O
hy0 : ¬↑(Ideal.Quotient.mk (Ideal.span {↑p})) s = 0
hxy0 : ¬↑(Ideal.Quotient.mk (Ideal.span {↑p})) (r + s) = 0
⊢ ↑v (↑(algebraMap O K) r + ↑(algebraMap O K) s) ≤ max (↑v (↑(algebraMap O K) r)) (↑v (↑(algebraMap O K) s))
[PROOFSTEP]
exact v.map_add _ _
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x : ModP K v O hv p
⊢ ↑v ↑p < preVal K v O hv p x ↔ x ≠ 0
[PROOFSTEP]
refine' ⟨fun h hx => by rw [hx, preVal_zero] at h ; exact not_lt_zero' h, fun h => lt_of_not_le fun hp => h _⟩
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x : ModP K v O hv p
h : ↑v ↑p < preVal K v O hv p x
hx : x = 0
⊢ False
[PROOFSTEP]
rw [hx, preVal_zero] at h 
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x : ModP K v O hv p
h : ↑v ↑p < 0
hx : x = 0
⊢ False
[PROOFSTEP]
exact not_lt_zero' h
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp✝ : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x : ModP K v O hv p
h : x ≠ 0
hp : preVal K v O hv p x ≤ ↑v ↑p
⊢ x = 0
[PROOFSTEP]
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
[GOAL]
case intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp✝ : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
r : O
h : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
hp : preVal K v O hv p (↑(Ideal.Quotient.mk (Ideal.span {↑p})) r) ≤ ↑v ↑p
⊢ ↑(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0
[PROOFSTEP]
rw [preVal_mk h, ← map_natCast (algebraMap O K) p, hv.le_iff_dvd] at hp 
[GOAL]
case intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp✝ : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
r : O
h : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
hp : ↑p ∣ r
⊢ ↑(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0
[PROOFSTEP]
rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]
[GOAL]
case intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp✝ : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
r : O
h : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
hp : ↑p ∣ r
⊢ ↑p ∣ r
[PROOFSTEP]
exact hp
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x : ModP K v O hv p
hvx : preVal K v O hv p x = 0
hx0 : x ≠ 0
⊢ False
[PROOFSTEP]
rw [← v_p_lt_preVal, hvx] at hx0 
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x : ModP K v O hv p
hvx : preVal K v O hv p x = 0
hx0 : ↑v ↑p < 0
⊢ False
[PROOFSTEP]
exact not_lt_zero' hx0
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x : O
⊢ ↑v ↑p < ↑v (↑(algebraMap O K) x) ↔ ↑(Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
[PROOFSTEP]
rw [lt_iff_not_le, not_iff_not, ← map_natCast (algebraMap O K) p, hv.le_iff_dvd, Ideal.Quotient.eq_zero_iff_mem,
  Ideal.mem_span_singleton]
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
x y : ModP K v O hv p
hx : x ^ p ≠ 0
hy : y ^ p ≠ 0
⊢ x * y ≠ 0
[PROOFSTEP]
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
[GOAL]
case intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
y : ModP K v O hv p
hy : y ^ p ≠ 0
r : O
hx : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) r ^ p ≠ 0
⊢ ↑(Ideal.Quotient.mk (Ideal.span {↑p})) r * y ≠ 0
[PROOFSTEP]
obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y
[GOAL]
case intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) r ^ p ≠ 0
s : O
hy : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) s ^ p ≠ 0
⊢ ↑(Ideal.Quotient.mk (Ideal.span {↑p})) r * ↑(Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
[PROOFSTEP]
have h1p : (0 : ℝ) < 1 / p := one_div_pos.2 (Nat.cast_pos.2 hp.1.pos)
[GOAL]
case intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) r ^ p ≠ 0
s : O
hy : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) s ^ p ≠ 0
h1p : 0 < 1 / ↑p
⊢ ↑(Ideal.Quotient.mk (Ideal.span {↑p})) r * ↑(Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
[PROOFSTEP]
rw [← RingHom.map_mul]
[GOAL]
case intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) r ^ p ≠ 0
s : O
hy : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) s ^ p ≠ 0
h1p : 0 < 1 / ↑p
⊢ ↑(Ideal.Quotient.mk (Ideal.span {↑p})) (r * s) ≠ 0
[PROOFSTEP]
rw [← RingHom.map_pow] at hx hy 
[GOAL]
case intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) (r ^ p) ≠ 0
s : O
hy : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) (s ^ p) ≠ 0
h1p : 0 < 1 / ↑p
⊢ ↑(Ideal.Quotient.mk (Ideal.span {↑p})) (r * s) ≠ 0
[PROOFSTEP]
rw [← v_p_lt_val hv] at hx hy ⊢
[GOAL]
case intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑v ↑p < ↑v (↑(algebraMap O K) (r ^ p))
s : O
hy : ↑v ↑p < ↑v (↑(algebraMap O K) (s ^ p))
h1p : 0 < 1 / ↑p
⊢ ↑v ↑p < ↑v (↑(algebraMap O K) (r * s))
[PROOFSTEP]
rw [RingHom.map_pow, v.map_pow, ← rpow_lt_rpow_iff h1p, ← rpow_nat_cast, ← rpow_mul,
  mul_one_div_cancel (Nat.cast_ne_zero.2 hp.1.ne_zero : (p : ℝ) ≠ 0), rpow_one] at hx hy 
[GOAL]
case intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) r)
s : O
hy : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) s)
h1p : 0 < 1 / ↑p
⊢ ↑v ↑p < ↑v (↑(algebraMap O K) (r * s))
[PROOFSTEP]
rw [RingHom.map_mul, v.map_mul]
[GOAL]
case intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) r)
s : O
hy : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) s)
h1p : 0 < 1 / ↑p
⊢ ↑v ↑p < ↑v (↑(algebraMap O K) r) * ↑v (↑(algebraMap O K) s)
[PROOFSTEP]
refine' lt_of_le_of_lt _ (mul_lt_mul₀ hx hy)
[GOAL]
case intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) r)
s : O
hy : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) s)
h1p : 0 < 1 / ↑p
⊢ ↑v ↑p ≤ ↑v ↑p ^ (1 / ↑p) * ↑v ↑p ^ (1 / ↑p)
[PROOFSTEP]
by_cases hvp : v p = 0
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp✝ : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) r)
s : O
hy : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : ↑v ↑p = 0
⊢ ↑v ↑p ≤ ↑v ↑p ^ (1 / ↑p) * ↑v ↑p ^ (1 / ↑p)
[PROOFSTEP]
rw [hvp]
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp✝ : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) r)
s : O
hy : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : ↑v ↑p = 0
⊢ 0 ≤ 0 ^ (1 / ↑p) * 0 ^ (1 / ↑p)
[PROOFSTEP]
exact zero_le _
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp✝ : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) r)
s : O
hy : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : ¬↑v ↑p = 0
⊢ ↑v ↑p ≤ ↑v ↑p ^ (1 / ↑p) * ↑v ↑p ^ (1 / ↑p)
[PROOFSTEP]
replace hvp := zero_lt_iff.2 hvp
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp✝ : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) r)
s : O
hy : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < ↑v ↑p
⊢ ↑v ↑p ≤ ↑v ↑p ^ (1 / ↑p) * ↑v ↑p ^ (1 / ↑p)
[PROOFSTEP]
conv_lhs => rw [← rpow_one (v p)]
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp✝ : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) r)
s : O
hy : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < ↑v ↑p
| ↑v ↑p
[PROOFSTEP]
rw [← rpow_one (v p)]
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp✝ : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) r)
s : O
hy : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < ↑v ↑p
| ↑v ↑p
[PROOFSTEP]
rw [← rpow_one (v p)]
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp✝ : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) r)
s : O
hy : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < ↑v ↑p
| ↑v ↑p
[PROOFSTEP]
rw [← rpow_one (v p)]
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp✝ : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) r)
s : O
hy : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < ↑v ↑p
⊢ ↑v ↑p ^ 1 ≤ ↑v ↑p ^ (1 / ↑p) * ↑v ↑p ^ (1 / ↑p)
[PROOFSTEP]
rw [← rpow_add (ne_of_gt hvp)]
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp✝ : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) r)
s : O
hy : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < ↑v ↑p
⊢ ↑v ↑p ^ 1 ≤ ↑v ↑p ^ (1 / ↑p + 1 / ↑p)
[PROOFSTEP]
refine' rpow_le_rpow_of_exponent_ge hvp (map_natCast (algebraMap O K) p ▸ hv.2 _) _
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp✝ : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) r)
s : O
hy : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < ↑v ↑p
⊢ 1 / ↑p + 1 / ↑p ≤ 1
[PROOFSTEP]
rw [← add_div, div_le_one (Nat.cast_pos.2 hp.1.pos : 0 < (p : ℝ))]
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp✝ : Fact (↑v ↑p ≠ 1)
r : O
hx : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) r)
s : O
hy : ↑v ↑p ^ (1 / ↑p) < ↑v (↑(algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : 0 < ↑v ↑p
⊢ 1 + 1 ≤ ↑p
[PROOFSTEP]
exact_mod_cast hp.1.two_le
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
n : ℕ
hfn : ↑(coeff (ModP K v O hv p) p n) f ≠ 0
⊢ valAux K v O hv p f = ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p n) f) ^ p ^ n
[PROOFSTEP]
have h : ∃ n, coeff _ _ n f ≠ 0 := ⟨n, hfn⟩
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
n : ℕ
hfn : ↑(coeff (ModP K v O hv p) p n) f ≠ 0
h : ∃ n, ↑(coeff (ModP K v O hv p) p n) f ≠ 0
⊢ valAux K v O hv p f = ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p n) f) ^ p ^ n
[PROOFSTEP]
rw [valAux, dif_pos h]
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
n : ℕ
hfn : ↑(coeff (ModP K v O hv p) p n) f ≠ 0
h : ∃ n, ↑(coeff (ModP K v O hv p) p n) f ≠ 0
⊢ ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p n) f) ^ p ^ n
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le (Nat.find_min' h hfn)
[GOAL]
case intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
h : ∃ n, ↑(coeff (ModP K v O hv p) p n) f ≠ 0
k : ℕ
hfn : ↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f ≠ 0
⊢ ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case intro.zero
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
h : ∃ n, ↑(coeff (ModP K v O hv p) p n) f ≠ 0
k : ℕ
hfn✝ : ↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f ≠ 0
hfn : ↑(coeff (ModP K v O hv p) p (Nat.find h + Nat.zero)) f ≠ 0
⊢ ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h + Nat.zero)) f) ^ p ^ (Nat.find h + Nat.zero)
[PROOFSTEP]
rfl
[GOAL]
case intro.succ
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
h : ∃ n, ↑(coeff (ModP K v O hv p) p n) f ≠ 0
k✝ : ℕ
hfn✝ : ↑(coeff (ModP K v O hv p) p (Nat.find h + k✝)) f ≠ 0
k : ℕ
ih :
  ↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : ↑(coeff (ModP K v O hv p) p (Nat.find h + Nat.succ k)) f ≠ 0
⊢ ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h + Nat.succ k)) f) ^ p ^ (Nat.find h + Nat.succ k)
[PROOFSTEP]
obtain ⟨x, hx⟩ := Ideal.Quotient.mk_surjective (coeff _ _ (Nat.find h + k + 1) f)
[GOAL]
case intro.succ.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
h : ∃ n, ↑(coeff (ModP K v O hv p) p n) f ≠ 0
k✝ : ℕ
hfn✝ : ↑(coeff (ModP K v O hv p) p (Nat.find h + k✝)) f ≠ 0
k : ℕ
ih :
  ↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : ↑(coeff (ModP K v O hv p) p (Nat.find h + Nat.succ k)) f ≠ 0
x : O
hx : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) x = ↑(coeff (ModP K v O hv p) p (Nat.find h + k + 1)) f
⊢ ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h + Nat.succ k)) f) ^ p ^ (Nat.find h + Nat.succ k)
[PROOFSTEP]
have h1 : (Ideal.Quotient.mk _ x : ModP K v O hv p) ≠ 0 := hx.symm ▸ hfn
[GOAL]
case intro.succ.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
h : ∃ n, ↑(coeff (ModP K v O hv p) p n) f ≠ 0
k✝ : ℕ
hfn✝ : ↑(coeff (ModP K v O hv p) p (Nat.find h + k✝)) f ≠ 0
k : ℕ
ih :
  ↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : ↑(coeff (ModP K v O hv p) p (Nat.find h + Nat.succ k)) f ≠ 0
x : O
hx : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) x = ↑(coeff (ModP K v O hv p) p (Nat.find h + k + 1)) f
h1 : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
⊢ ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h + Nat.succ k)) f) ^ p ^ (Nat.find h + Nat.succ k)
[PROOFSTEP]
have h2 : (Ideal.Quotient.mk _ (x ^ p) : ModP K v O hv p) ≠ 0 :=
  by
  erw [RingHom.map_pow, hx, ← RingHom.map_pow, coeff_pow_p]
  exact coeff_nat_find_add_ne_zero k
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
h : ∃ n, ↑(coeff (ModP K v O hv p) p n) f ≠ 0
k✝ : ℕ
hfn✝ : ↑(coeff (ModP K v O hv p) p (Nat.find h + k✝)) f ≠ 0
k : ℕ
ih :
  ↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : ↑(coeff (ModP K v O hv p) p (Nat.find h + Nat.succ k)) f ≠ 0
x : O
hx : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) x = ↑(coeff (ModP K v O hv p) p (Nat.find h + k + 1)) f
h1 : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
⊢ ↑(Ideal.Quotient.mk (Ideal.span {↑p})) (x ^ p) ≠ 0
[PROOFSTEP]
erw [RingHom.map_pow, hx, ← RingHom.map_pow, coeff_pow_p]
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
h : ∃ n, ↑(coeff (ModP K v O hv p) p n) f ≠ 0
k✝ : ℕ
hfn✝ : ↑(coeff (ModP K v O hv p) p (Nat.find h + k✝)) f ≠ 0
k : ℕ
ih :
  ↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : ↑(coeff (ModP K v O hv p) p (Nat.find h + Nat.succ k)) f ≠ 0
x : O
hx : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) x = ↑(coeff (ModP K v O hv p) p (Nat.find h + k + 1)) f
h1 : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
⊢ ↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f ≠ 0
[PROOFSTEP]
exact coeff_nat_find_add_ne_zero k
[GOAL]
case intro.succ.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
h : ∃ n, ↑(coeff (ModP K v O hv p) p n) f ≠ 0
k✝ : ℕ
hfn✝ : ↑(coeff (ModP K v O hv p) p (Nat.find h + k✝)) f ≠ 0
k : ℕ
ih :
  ↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : ↑(coeff (ModP K v O hv p) p (Nat.find h + Nat.succ k)) f ≠ 0
x : O
hx : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) x = ↑(coeff (ModP K v O hv p) p (Nat.find h + k + 1)) f
h1 : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
h2 : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) (x ^ p) ≠ 0
⊢ ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h + Nat.succ k)) f) ^ p ^ (Nat.find h + Nat.succ k)
[PROOFSTEP]
erw [ih (coeff_nat_find_add_ne_zero k), ← hx, ← coeff_pow_p, RingHom.map_pow, ← hx, ← RingHom.map_pow,
  ModP.preVal_mk h1, ModP.preVal_mk h2, RingHom.map_pow, v.map_pow, ← pow_mul, pow_succ]
[GOAL]
case intro.succ.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
h : ∃ n, ↑(coeff (ModP K v O hv p) p n) f ≠ 0
k✝ : ℕ
hfn✝ : ↑(coeff (ModP K v O hv p) p (Nat.find h + k✝)) f ≠ 0
k : ℕ
ih :
  ↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : ↑(coeff (ModP K v O hv p) p (Nat.find h + Nat.succ k)) f ≠ 0
x : O
hx : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) x = ↑(coeff (ModP K v O hv p) p (Nat.find h + k + 1)) f
h1 : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
h2 : ↑(Ideal.Quotient.mk (Ideal.span {↑p})) (x ^ p) ≠ 0
⊢ ↑v (↑(algebraMap O K) x) ^ (p * p ^ (Nat.find h + k)) = ↑v (↑(algebraMap O K) x) ^ (p * p ^ Nat.add (Nat.find h) k)
[PROOFSTEP]
rfl
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
⊢ ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p 0) 1) ^ p ^ 0 = 1
[PROOFSTEP]
rw [pow_zero, pow_one, RingHom.map_one, ← (Ideal.Quotient.mk _).map_one, ModP.preVal_mk, RingHom.map_one, v.map_one]
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
⊢ ↑(Ideal.Quotient.mk (Ideal.span {↑p})) 1 ≠ 0
[PROOFSTEP]
change (1 : ModP K v O hv p) ≠ 0
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
⊢ valAux K v O hv p (f * g) = valAux K v O hv p f * valAux K v O hv p g
[PROOFSTEP]
by_cases hf : f = 0
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : f = 0
⊢ valAux K v O hv p (f * g) = valAux K v O hv p f * valAux K v O hv p g
[PROOFSTEP]
rw [hf, zero_mul, valAux_zero, zero_mul]
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
⊢ valAux K v O hv p (f * g) = valAux K v O hv p f * valAux K v O hv p g
[PROOFSTEP]
by_cases hg : g = 0
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : g = 0
⊢ valAux K v O hv p (f * g) = valAux K v O hv p f * valAux K v O hv p g
[PROOFSTEP]
rw [hg, mul_zero, valAux_zero, mul_zero]
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
⊢ valAux K v O hv p (f * g) = valAux K v O hv p f * valAux K v O hv p g
[PROOFSTEP]
obtain ⟨m, hm⟩ : ∃ n, coeff _ _ n f ≠ 0 := not_forall.1 fun h => hf <| Perfection.ext h
[GOAL]
case neg.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
m : ℕ
hm : ↑(coeff (ModP K v O hv p) p m) f ≠ 0
⊢ valAux K v O hv p (f * g) = valAux K v O hv p f * valAux K v O hv p g
[PROOFSTEP]
obtain ⟨n, hn⟩ : ∃ n, coeff _ _ n g ≠ 0 := not_forall.1 fun h => hg <| Perfection.ext h
[GOAL]
case neg.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
m : ℕ
hm : ↑(coeff (ModP K v O hv p) p m) f ≠ 0
n : ℕ
hn : ↑(coeff (ModP K v O hv p) p n) g ≠ 0
⊢ valAux K v O hv p (f * g) = valAux K v O hv p f * valAux K v O hv p g
[PROOFSTEP]
replace hm := coeff_ne_zero_of_le hm (le_max_left m n)
[GOAL]
case neg.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hn : ↑(coeff (ModP K v O hv p) p n) g ≠ 0
hm : ↑(coeff (ModP K v O hv p) p (max m n)) f ≠ 0
⊢ valAux K v O hv p (f * g) = valAux K v O hv p f * valAux K v O hv p g
[PROOFSTEP]
replace hn := coeff_ne_zero_of_le hn (le_max_right m n)
[GOAL]
case neg.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hm : ↑(coeff (ModP K v O hv p) p (max m n)) f ≠ 0
hn : ↑(coeff (ModP K v O hv p) p (max m n)) g ≠ 0
⊢ valAux K v O hv p (f * g) = valAux K v O hv p f * valAux K v O hv p g
[PROOFSTEP]
have hfg : coeff _ _ (max m n + 1) (f * g) ≠ 0 :=
  by
  rw [RingHom.map_mul]
  refine' ModP.mul_ne_zero_of_pow_p_ne_zero _ _
  · rw [← RingHom.map_pow, coeff_pow_p f]; assumption
  · rw [← RingHom.map_pow, coeff_pow_p g]; assumption
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hm : ↑(coeff (ModP K v O hv p) p (max m n)) f ≠ 0
hn : ↑(coeff (ModP K v O hv p) p (max m n)) g ≠ 0
⊢ ↑(coeff (ModP K v O hv p) p (max m n + 1)) (f * g) ≠ 0
[PROOFSTEP]
rw [RingHom.map_mul]
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hm : ↑(coeff (ModP K v O hv p) p (max m n)) f ≠ 0
hn : ↑(coeff (ModP K v O hv p) p (max m n)) g ≠ 0
⊢ ↑(coeff (ModP K v O hv p) p (max m n + 1)) f * ↑(coeff (ModP K v O hv p) p (max m n + 1)) g ≠ 0
[PROOFSTEP]
refine' ModP.mul_ne_zero_of_pow_p_ne_zero _ _
[GOAL]
case refine'_1
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hm : ↑(coeff (ModP K v O hv p) p (max m n)) f ≠ 0
hn : ↑(coeff (ModP K v O hv p) p (max m n)) g ≠ 0
⊢ ↑(coeff (ModP K v O hv p) p (max m n + 1)) f ^ p ≠ 0
[PROOFSTEP]
rw [← RingHom.map_pow, coeff_pow_p f]
[GOAL]
case refine'_1
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hm : ↑(coeff (ModP K v O hv p) p (max m n)) f ≠ 0
hn : ↑(coeff (ModP K v O hv p) p (max m n)) g ≠ 0
⊢ ↑(coeff (ModP K v O hv p) p (max m n)) f ≠ 0
[PROOFSTEP]
assumption
[GOAL]
case refine'_2
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hm : ↑(coeff (ModP K v O hv p) p (max m n)) f ≠ 0
hn : ↑(coeff (ModP K v O hv p) p (max m n)) g ≠ 0
⊢ ↑(coeff (ModP K v O hv p) p (max m n + 1)) g ^ p ≠ 0
[PROOFSTEP]
rw [← RingHom.map_pow, coeff_pow_p g]
[GOAL]
case refine'_2
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hm : ↑(coeff (ModP K v O hv p) p (max m n)) f ≠ 0
hn : ↑(coeff (ModP K v O hv p) p (max m n)) g ≠ 0
⊢ ↑(coeff (ModP K v O hv p) p (max m n)) g ≠ 0
[PROOFSTEP]
assumption
[GOAL]
case neg.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hm : ↑(coeff (ModP K v O hv p) p (max m n)) f ≠ 0
hn : ↑(coeff (ModP K v O hv p) p (max m n)) g ≠ 0
hfg : ↑(coeff (ModP K v O hv p) p (max m n + 1)) (f * g) ≠ 0
⊢ valAux K v O hv p (f * g) = valAux K v O hv p f * valAux K v O hv p g
[PROOFSTEP]
rw [valAux_eq (coeff_add_ne_zero hm 1), valAux_eq (coeff_add_ne_zero hn 1), valAux_eq hfg]
[GOAL]
case neg.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hm : ↑(coeff (ModP K v O hv p) p (max m n)) f ≠ 0
hn : ↑(coeff (ModP K v O hv p) p (max m n)) g ≠ 0
hfg : ↑(coeff (ModP K v O hv p) p (max m n + 1)) (f * g) ≠ 0
⊢ ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (max m n + 1)) (f * g)) ^ p ^ (max m n + 1) =
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (max m n + 1)) f) ^ p ^ (max m n + 1) *
      ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (max m n + 1)) g) ^ p ^ (max m n + 1)
[PROOFSTEP]
rw [RingHom.map_mul] at hfg ⊢
[GOAL]
case neg.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
m n : ℕ
hm : ↑(coeff (ModP K v O hv p) p (max m n)) f ≠ 0
hn : ↑(coeff (ModP K v O hv p) p (max m n)) g ≠ 0
hfg : ↑(coeff (ModP K v O hv p) p (max m n + 1)) f * ↑(coeff (ModP K v O hv p) p (max m n + 1)) g ≠ 0
⊢ ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (max m n + 1)) f * ↑(coeff (ModP K v O hv p) p (max m n + 1)) g) ^
      p ^ (max m n + 1) =
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (max m n + 1)) f) ^ p ^ (max m n + 1) *
      ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (max m n + 1)) g) ^ p ^ (max m n + 1)
[PROOFSTEP]
rw [ModP.preVal_mul hfg, mul_pow]
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
⊢ valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
[PROOFSTEP]
by_cases hf : f = 0
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : f = 0
⊢ valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
[PROOFSTEP]
rw [hf, zero_add, valAux_zero, max_eq_right]
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : f = 0
⊢ 0 ≤ valAux K v O hv p g
[PROOFSTEP]
exact zero_le _
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
⊢ valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
[PROOFSTEP]
by_cases hg : g = 0
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : g = 0
⊢ valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
[PROOFSTEP]
rw [hg, add_zero, valAux_zero, max_eq_left]
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : g = 0
⊢ 0 ≤ valAux K v O hv p f
[PROOFSTEP]
exact zero_le _
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
⊢ valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
[PROOFSTEP]
by_cases hfg : f + g = 0
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
hfg : f + g = 0
⊢ valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
[PROOFSTEP]
rw [hfg, valAux_zero]
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
hfg : f + g = 0
⊢ 0 ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
[PROOFSTEP]
exact zero_le _
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ¬f = 0
hg : ¬g = 0
hfg : ¬f + g = 0
⊢ valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
[PROOFSTEP]
replace hf : ∃ n, coeff _ _ n f ≠ 0 := not_forall.1 fun h => hf <| Perfection.ext h
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hg : ¬g = 0
hfg : ¬f + g = 0
hf : ∃ n, ↑(coeff (ModP K v O hv p) p n) f ≠ 0
⊢ valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
[PROOFSTEP]
replace hg : ∃ n, coeff _ _ n g ≠ 0 := not_forall.1 fun h => hg <| Perfection.ext h
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hfg : ¬f + g = 0
hf : ∃ n, ↑(coeff (ModP K v O hv p) p n) f ≠ 0
hg : ∃ n, ↑(coeff (ModP K v O hv p) p n) g ≠ 0
⊢ valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
[PROOFSTEP]
replace hfg : ∃ n, coeff _ _ n (f + g) ≠ 0 := not_forall.1 fun h => hfg <| Perfection.ext h
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hf : ∃ n, ↑(coeff (ModP K v O hv p) p n) f ≠ 0
hg : ∃ n, ↑(coeff (ModP K v O hv p) p n) g ≠ 0
hfg : ∃ n, ↑(coeff (ModP K v O hv p) p n) (f + g) ≠ 0
⊢ valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
[PROOFSTEP]
obtain ⟨m, hm⟩ := hf
[GOAL]
case neg.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hg : ∃ n, ↑(coeff (ModP K v O hv p) p n) g ≠ 0
hfg : ∃ n, ↑(coeff (ModP K v O hv p) p n) (f + g) ≠ 0
m : ℕ
hm : ↑(coeff (ModP K v O hv p) p m) f ≠ 0
⊢ valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
[PROOFSTEP]
obtain ⟨n, hn⟩ := hg
[GOAL]
case neg.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
hfg : ∃ n, ↑(coeff (ModP K v O hv p) p n) (f + g) ≠ 0
m : ℕ
hm : ↑(coeff (ModP K v O hv p) p m) f ≠ 0
n : ℕ
hn : ↑(coeff (ModP K v O hv p) p n) g ≠ 0
⊢ valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
[PROOFSTEP]
obtain ⟨k, hk⟩ := hfg
[GOAL]
case neg.intro.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
m : ℕ
hm : ↑(coeff (ModP K v O hv p) p m) f ≠ 0
n : ℕ
hn : ↑(coeff (ModP K v O hv p) p n) g ≠ 0
k : ℕ
hk : ↑(coeff (ModP K v O hv p) p k) (f + g) ≠ 0
⊢ valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
[PROOFSTEP]
replace hm := coeff_ne_zero_of_le hm (le_trans (le_max_left m n) (le_max_left _ k))
[GOAL]
case neg.intro.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
m n : ℕ
hn : ↑(coeff (ModP K v O hv p) p n) g ≠ 0
k : ℕ
hk : ↑(coeff (ModP K v O hv p) p k) (f + g) ≠ 0
hm : ↑(coeff (ModP K v O hv p) p (max (max m n) k)) f ≠ 0
⊢ valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
[PROOFSTEP]
replace hn := coeff_ne_zero_of_le hn (le_trans (le_max_right m n) (le_max_left _ k))
[GOAL]
case neg.intro.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
m n k : ℕ
hk : ↑(coeff (ModP K v O hv p) p k) (f + g) ≠ 0
hm : ↑(coeff (ModP K v O hv p) p (max (max m n) k)) f ≠ 0
hn : ↑(coeff (ModP K v O hv p) p (max (max m n) k)) g ≠ 0
⊢ valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
[PROOFSTEP]
replace hk := coeff_ne_zero_of_le hk (le_max_right (max m n) k)
[GOAL]
case neg.intro.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
m n k : ℕ
hm : ↑(coeff (ModP K v O hv p) p (max (max m n) k)) f ≠ 0
hn : ↑(coeff (ModP K v O hv p) p (max (max m n) k)) g ≠ 0
hk : ↑(coeff (ModP K v O hv p) p (max (max m n) k)) (f + g) ≠ 0
⊢ valAux K v O hv p (f + g) ≤ max (valAux K v O hv p f) (valAux K v O hv p g)
[PROOFSTEP]
rw [valAux_eq hm, valAux_eq hn, valAux_eq hk, RingHom.map_add]
[GOAL]
case neg.intro.intro.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
m n k : ℕ
hm : ↑(coeff (ModP K v O hv p) p (max (max m n) k)) f ≠ 0
hn : ↑(coeff (ModP K v O hv p) p (max (max m n) k)) g ≠ 0
hk : ↑(coeff (ModP K v O hv p) p (max (max m n) k)) (f + g) ≠ 0
⊢ ModP.preVal K v O hv p
        (↑(coeff (ModP K v O hv p) p (max (max m n) k)) f + ↑(coeff (ModP K v O hv p) p (max (max m n) k)) g) ^
      p ^ max (max m n) k ≤
    max (ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (max (max m n) k)) f) ^ p ^ max (max m n) k)
      (ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (max (max m n) k)) g) ^ p ^ max (max m n) k)
[PROOFSTEP]
cases' le_max_iff.1 (ModP.preVal_add (coeff _ _ (max (max m n) k) f) (coeff _ _ (max (max m n) k) g)) with h h
[GOAL]
case neg.intro.intro.intro.inl
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
m n k : ℕ
hm : ↑(coeff (ModP K v O hv p) p (max (max m n) k)) f ≠ 0
hn : ↑(coeff (ModP K v O hv p) p (max (max m n) k)) g ≠ 0
hk : ↑(coeff (ModP K v O hv p) p (max (max m n) k)) (f + g) ≠ 0
h :
  ModP.preVal K v O hv p
      (↑(coeff (ModP K v O hv p) p (max (max m n) k)) f + ↑(coeff (ModP K v O hv p) p (max (max m n) k)) g) ≤
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (max (max m n) k)) f)
⊢ ModP.preVal K v O hv p
        (↑(coeff (ModP K v O hv p) p (max (max m n) k)) f + ↑(coeff (ModP K v O hv p) p (max (max m n) k)) g) ^
      p ^ max (max m n) k ≤
    max (ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (max (max m n) k)) f) ^ p ^ max (max m n) k)
      (ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (max (max m n) k)) g) ^ p ^ max (max m n) k)
[PROOFSTEP]
exact le_max_of_le_left (pow_le_pow_of_le_left' h _)
[GOAL]
case neg.intro.intro.intro.inr
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f g : PreTilt K v O hv p
m n k : ℕ
hm : ↑(coeff (ModP K v O hv p) p (max (max m n) k)) f ≠ 0
hn : ↑(coeff (ModP K v O hv p) p (max (max m n) k)) g ≠ 0
hk : ↑(coeff (ModP K v O hv p) p (max (max m n) k)) (f + g) ≠ 0
h :
  ModP.preVal K v O hv p
      (↑(coeff (ModP K v O hv p) p (max (max m n) k)) f + ↑(coeff (ModP K v O hv p) p (max (max m n) k)) g) ≤
    ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (max (max m n) k)) g)
⊢ ModP.preVal K v O hv p
        (↑(coeff (ModP K v O hv p) p (max (max m n) k)) f + ↑(coeff (ModP K v O hv p) p (max (max m n) k)) g) ^
      p ^ max (max m n) k ≤
    max (ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (max (max m n) k)) f) ^ p ^ max (max m n) k)
      (ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p (max (max m n) k)) g) ^ p ^ max (max m n) k)
[PROOFSTEP]
exact le_max_of_le_right (pow_le_pow_of_le_left' h _)
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
⊢ ↑(val K v O hv p) f = 0 ↔ f = 0
[PROOFSTEP]
by_cases hf0 : f = 0
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
hf0 : f = 0
⊢ ↑(val K v O hv p) f = 0 ↔ f = 0
[PROOFSTEP]
rw [hf0]
[GOAL]
case pos
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
hf0 : f = 0
⊢ ↑(val K v O hv p) 0 = 0 ↔ 0 = 0
[PROOFSTEP]
exact iff_of_true (Valuation.map_zero _) rfl
[GOAL]
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
hf0 : ¬f = 0
⊢ ↑(val K v O hv p) f = 0 ↔ f = 0
[PROOFSTEP]
obtain ⟨n, hn⟩ : ∃ n, coeff _ _ n f ≠ 0 := not_forall.1 fun h => hf0 <| Perfection.ext h
[GOAL]
case neg.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
hf0 : ¬f = 0
n : ℕ
hn : ↑(coeff (ModP K v O hv p) p n) f ≠ 0
⊢ ↑(val K v O hv p) f = 0 ↔ f = 0
[PROOFSTEP]
show valAux K v O hv p f = 0 ↔ f = 0
[GOAL]
case neg.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
hf0 : ¬f = 0
n : ℕ
hn : ↑(coeff (ModP K v O hv p) p n) f ≠ 0
⊢ valAux K v O hv p f = 0 ↔ f = 0
[PROOFSTEP]
refine' iff_of_false (fun hvf => hn _) hf0
[GOAL]
case neg.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
hf0 : ¬f = 0
n : ℕ
hn : ↑(coeff (ModP K v O hv p) p n) f ≠ 0
hvf : valAux K v O hv p f = 0
⊢ ↑(coeff (ModP K v O hv p) p n) f = 0
[PROOFSTEP]
rw [valAux_eq hn] at hvf 
[GOAL]
case neg.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
hf0 : ¬f = 0
n : ℕ
hn : ↑(coeff (ModP K v O hv p) p n) f ≠ 0
hvf : ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p n) f) ^ p ^ n = 0
⊢ ↑(coeff (ModP K v O hv p) p n) f = 0
[PROOFSTEP]
replace hvf := pow_eq_zero hvf
[GOAL]
case neg.intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
f : PreTilt K v O hv p
hf0 : ¬f = 0
n : ℕ
hn : ↑(coeff (ModP K v O hv p) p n) f ≠ 0
hvf : ModP.preVal K v O hv p (↑(coeff (ModP K v O hv p) p n) f) = 0
⊢ ↑(coeff (ModP K v O hv p) p n) f = 0
[PROOFSTEP]
rwa [ModP.preVal_eq_zero] at hvf 
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
⊢ IsDomain (PreTilt K v O hv p)
[PROOFSTEP]
haveI : Nontrivial (PreTilt K v O hv p) := ⟨(CharP.nontrivial_of_char_ne_one hp.1.ne_one).1⟩
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
this : Nontrivial (PreTilt K v O hv p)
⊢ IsDomain (PreTilt K v O hv p)
[PROOFSTEP]
haveI : NoZeroDivisors (PreTilt K v O hv p) :=
  ⟨fun hfg => by
    simp_rw [← map_eq_zero] at hfg ⊢; contrapose! hfg; rw [Valuation.map_mul]
    exact mul_ne_zero hfg.1 hfg.2⟩
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
this : Nontrivial (PreTilt K v O hv p)
a✝ b✝ : PreTilt K v O hv p
hfg : a✝ * b✝ = 0
⊢ a✝ = 0 ∨ b✝ = 0
[PROOFSTEP]
simp_rw [← map_eq_zero] at hfg ⊢
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
this : Nontrivial (PreTilt K v O hv p)
a✝ b✝ : PreTilt K v O hv p
hfg : ↑(val K v O hv p) (a✝ * b✝) = 0
⊢ ↑(val K v O hv p) a✝ = 0 ∨ ↑(val K v O hv p) b✝ = 0
[PROOFSTEP]
contrapose! hfg
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
this : Nontrivial (PreTilt K v O hv p)
a✝ b✝ : PreTilt K v O hv p
hfg : ↑(val K v O hv p) a✝ ≠ 0 ∧ ↑(val K v O hv p) b✝ ≠ 0
⊢ ↑(val K v O hv p) (a✝ * b✝) ≠ 0
[PROOFSTEP]
rw [Valuation.map_mul]
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
this : Nontrivial (PreTilt K v O hv p)
a✝ b✝ : PreTilt K v O hv p
hfg : ↑(val K v O hv p) a✝ ≠ 0 ∧ ↑(val K v O hv p) b✝ ≠ 0
⊢ ↑(val K v O hv p) a✝ * ↑(val K v O hv p) b✝ ≠ 0
[PROOFSTEP]
exact mul_ne_zero hfg.1 hfg.2
[GOAL]
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : Valuation.Integers v O
p : ℕ
hp : Fact (Nat.Prime p)
hvp : Fact (↑v ↑p ≠ 1)
this✝ : Nontrivial (PreTilt K v O hv p)
this : NoZeroDivisors (PreTilt K v O hv p)
⊢ IsDomain (PreTilt K v O hv p)
[PROOFSTEP]
exact NoZeroDivisors.to_isDomain _
