[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 _


[GOAL]
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
⊢ Subalgebra.restrictScalars C (adjoin D S) =
    Subalgebra.restrictScalars C (adjoin { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } S)
[PROOFSTEP]
suffices Set.range (algebraMap D E) = Set.range (algebraMap ((⊤ : Subalgebra C D).map (IsScalarTower.toAlgHom C D E)) E)
  by
  ext x
  change x ∈ Subsemiring.closure (_ ∪ S) ↔ x ∈ Subsemiring.closure (_ ∪ S)
  rw [this]
[GOAL]
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
this :
  Set.range ↑(algebraMap D E) = Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E)
⊢ Subalgebra.restrictScalars C (adjoin D S) =
    Subalgebra.restrictScalars C (adjoin { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } S)
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
this :
  Set.range ↑(algebraMap D E) = Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E)
x : E
⊢ x ∈ Subalgebra.restrictScalars C (adjoin D S) ↔
    x ∈ Subalgebra.restrictScalars C (adjoin { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } S)
[PROOFSTEP]
change x ∈ Subsemiring.closure (_ ∪ S) ↔ x ∈ Subsemiring.closure (_ ∪ S)
[GOAL]
case h
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
this :
  Set.range ↑(algebraMap D E) = Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E)
x : E
⊢ x ∈ Subsemiring.closure (Set.range ↑(algebraMap D E) ∪ S) ↔
    x ∈ Subsemiring.closure (Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E) ∪ S)
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
⊢ Set.range ↑(algebraMap D E) = Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E)
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
x : E
⊢ x ∈ Set.range ↑(algebraMap D E) ↔
    x ∈ Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
x : E
⊢ x ∈ Set.range ↑(algebraMap D E) →
    x ∈ Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E)
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case h.mp.intro
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
x : E
y : D
hy : ↑(algebraMap D E) y = x
⊢ x ∈ Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E)
[PROOFSTEP]
exact ⟨⟨algebraMap D E y, ⟨y, ⟨Algebra.mem_top, rfl⟩⟩⟩, hy⟩
[GOAL]
case h.mpr
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
x : E
⊢ x ∈ Set.range ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E) →
    x ∈ Set.range ↑(algebraMap D E)
[PROOFSTEP]
rintro ⟨⟨y, ⟨z, ⟨h0, h1⟩⟩⟩, h2⟩
[GOAL]
case h.mpr.intro.mk.intro.intro
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
x y : E
z : D
h0 : z ∈ ↑⊤.toSubsemiring
h1 : ↑↑(IsScalarTower.toAlgHom C D E) z = y
h2 :
  ↑(algebraMap { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤ } E)
      { val := y, property := (_ : ∃ a, a ∈ ↑⊤.toSubsemiring ∧ ↑↑(IsScalarTower.toAlgHom C D E) a = y) } =
    x
⊢ x ∈ Set.range ↑(algebraMap D E)
[PROOFSTEP]
exact ⟨z, Eq.trans h1 h2⟩
[GOAL]
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : CommSemiring C
inst✝⁹ : CommSemiring D
inst✝⁸ : CommSemiring E
inst✝⁷ : CommSemiring F
inst✝⁶ : Algebra C D
inst✝⁵ : Algebra C E
inst✝⁴ : Algebra C F
inst✝³ : Algebra D F
inst✝² : Algebra E F
inst✝¹ : IsScalarTower C D F
inst✝ : IsScalarTower C E F
S : Set D
T : Set E
hS : adjoin C S = ⊤
hT : adjoin C T = ⊤
⊢ Subalgebra.restrictScalars C (adjoin E (↑(algebraMap D F) '' S)) =
    Subalgebra.restrictScalars C (adjoin D (↑(algebraMap E F) '' T))
[PROOFSTEP]
rw [adjoin_restrictScalars C E, adjoin_restrictScalars C D, ← hS, ← hT, ← Algebra.adjoin_image, ← Algebra.adjoin_image,
  ← AlgHom.coe_toRingHom, ← AlgHom.coe_toRingHom, IsScalarTower.coe_toAlgHom, IsScalarTower.coe_toAlgHom, ←
  adjoin_union_eq_adjoin_adjoin, ← adjoin_union_eq_adjoin_adjoin, Set.union_comm]
[GOAL]
R✝ : Type u
S✝ : Type v
A✝ : Type w
B : Type u₁
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hRS : Subalgebra.FG ⊤
hSA : Subalgebra.FG ⊤
s : Finset S
hs : adjoin R ↑s = ⊤
t : Finset A
ht : adjoin S ↑t = ⊤
⊢ adjoin R ↑(Finset.image (↑(algebraMap S A)) s ∪ t) = ⊤
[PROOFSTEP]
rw [Finset.coe_union, Finset.coe_image, Algebra.adjoin_union_eq_adjoin_adjoin, Algebra.adjoin_algebraMap, hs,
  Algebra.map_top, IsScalarTower.adjoin_range_toAlgHom, ht, Subalgebra.restrictScalars_top]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
hAC : Subalgebra.FG ⊤
hBC : FG ⊤
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
cases' hAC with x hx
[GOAL]
case intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
hBC : FG ⊤
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
cases' hBC with y hy
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
have := hy
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy this : span B ↑y = ⊤
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
simp_rw [eq_top_iff', mem_span_finset] at this
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
this : ∀ (x : C), ∃ f, (Finset.sum y fun i => f i • i) = x
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
choose f hf using this
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
let s : Finset B := Finset.image₂ f (x ∪ y * y) y
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
have hxy : ∀ xi ∈ x, xi ∈ span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) := fun xi hxi =>
  hf xi ▸
    sum_mem fun yj hyj =>
      smul_mem (span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C))
        ⟨f xi yj, Algebra.subset_adjoin <| mem_image₂_of_mem (mem_union_left _ hxi) hyj⟩
        (subset_span <| mem_insert_of_mem hyj)
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
have hyy :
  span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) *
      span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) ≤
    span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) :=
  by
  rw [span_mul_span, span_le, coe_insert]
  rintro _ ⟨yi, yj, rfl | hyi, rfl | hyj, rfl⟩ <;> dsimp
  · rw [mul_one]
    exact subset_span (Set.mem_insert _ _)
  · rw [one_mul]
    exact subset_span (Set.mem_insert_of_mem _ hyj)
  · rw [mul_one]
    exact subset_span (Set.mem_insert_of_mem _ hyi)
  · rw [← hf (yi * yj)]
    exact
      SetLike.mem_coe.2
        (sum_mem fun yk hyk =>
          smul_mem (span (Algebra.adjoin A (↑s : Set B)) (insert 1 ↑y : Set C))
            ⟨f (yi * yj) yk, Algebra.subset_adjoin <| mem_image₂_of_mem (mem_union_right _ <| mul_mem_mul hyi hyj) hyk⟩
            (subset_span <| Set.mem_insert_of_mem _ hyk : yk ∈ _))
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) * span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) ≤
    span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
[PROOFSTEP]
rw [span_mul_span, span_le, coe_insert]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ insert 1 ↑y * insert 1 ↑y ⊆ ↑(span { x // x ∈ Algebra.adjoin A ↑s } (insert 1 ↑y))
[PROOFSTEP]
rintro _ ⟨yi, yj, rfl | hyi, rfl | hyj, rfl⟩
[GOAL]
case intro.intro.intro.inl.intro.inl
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ (fun x x_1 => x * x_1) 1 1 ∈ ↑(span { x // x ∈ Algebra.adjoin A ↑s } (insert 1 ↑y))
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro.intro.inl.intro.inr
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yj : C
hyj : yj ∈ ↑y
⊢ (fun x x_1 => x * x_1) 1 yj ∈ ↑(span { x // x ∈ Algebra.adjoin A ↑s } (insert 1 ↑y))
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro.intro.inr.intro.inl
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yi : C
hyi : yi ∈ ↑y
⊢ (fun x x_1 => x * x_1) yi 1 ∈ ↑(span { x // x ∈ Algebra.adjoin A ↑s } (insert 1 ↑y))
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro.intro.inr.intro.inr
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yi yj : C
hyi : yi ∈ ↑y
hyj : yj ∈ ↑y
⊢ (fun x x_1 => x * x_1) yi yj ∈ ↑(span { x // x ∈ Algebra.adjoin A ↑s } (insert 1 ↑y))
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro.intro.inl.intro.inl
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ 1 * 1 ∈ ↑(span { x_1 // x_1 ∈ Algebra.adjoin A ↑(image₂ f (x ∪ y * y) y) } (insert 1 ↑y))
[PROOFSTEP]
rw [mul_one]
[GOAL]
case intro.intro.intro.inl.intro.inl
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ 1 ∈ ↑(span { x_1 // x_1 ∈ Algebra.adjoin A ↑(image₂ f (x ∪ y * y) y) } (insert 1 ↑y))
[PROOFSTEP]
exact subset_span (Set.mem_insert _ _)
[GOAL]
case intro.intro.intro.inl.intro.inr
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yj : C
hyj : yj ∈ ↑y
⊢ 1 * yj ∈ ↑(span { x_1 // x_1 ∈ Algebra.adjoin A ↑(image₂ f (x ∪ y * y) y) } (insert 1 ↑y))
[PROOFSTEP]
rw [one_mul]
[GOAL]
case intro.intro.intro.inl.intro.inr
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yj : C
hyj : yj ∈ ↑y
⊢ yj ∈ ↑(span { x_1 // x_1 ∈ Algebra.adjoin A ↑(image₂ f (x ∪ y * y) y) } (insert 1 ↑y))
[PROOFSTEP]
exact subset_span (Set.mem_insert_of_mem _ hyj)
[GOAL]
case intro.intro.intro.inr.intro.inl
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yi : C
hyi : yi ∈ ↑y
⊢ yi * 1 ∈ ↑(span { x_1 // x_1 ∈ Algebra.adjoin A ↑(image₂ f (x ∪ y * y) y) } (insert 1 ↑y))
[PROOFSTEP]
rw [mul_one]
[GOAL]
case intro.intro.intro.inr.intro.inl
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yi : C
hyi : yi ∈ ↑y
⊢ yi ∈ ↑(span { x_1 // x_1 ∈ Algebra.adjoin A ↑(image₂ f (x ∪ y * y) y) } (insert 1 ↑y))
[PROOFSTEP]
exact subset_span (Set.mem_insert_of_mem _ hyi)
[GOAL]
case intro.intro.intro.inr.intro.inr
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yi yj : C
hyi : yi ∈ ↑y
hyj : yj ∈ ↑y
⊢ yi * yj ∈ ↑(span { x_1 // x_1 ∈ Algebra.adjoin A ↑(image₂ f (x ∪ y * y) y) } (insert 1 ↑y))
[PROOFSTEP]
rw [← hf (yi * yj)]
[GOAL]
case intro.intro.intro.inr.intro.inr
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
yi yj : C
hyi : yi ∈ ↑y
hyj : yj ∈ ↑y
⊢ (Finset.sum y fun i => f (yi * yj) i • i) ∈
    ↑(span { x_1 // x_1 ∈ Algebra.adjoin A ↑(image₂ f (x ∪ y * y) y) } (insert 1 ↑y))
[PROOFSTEP]
exact
  SetLike.mem_coe.2
    (sum_mem fun yk hyk =>
      smul_mem (span (Algebra.adjoin A (↑s : Set B)) (insert 1 ↑y : Set C))
        ⟨f (yi * yj) yk, Algebra.subset_adjoin <| mem_image₂_of_mem (mem_union_right _ <| mul_mem_mul hyi hyj) hyk⟩
        (subset_span <| Set.mem_insert_of_mem _ hyk : yk ∈ _))
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
hyy :
  span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) * span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) ≤
    span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ ∃ B₀, Subalgebra.FG B₀ ∧ FG ⊤
[PROOFSTEP]
refine' ⟨Algebra.adjoin A (↑s : Set B), Subalgebra.fg_adjoin_finset _, insert 1 y, _⟩
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
hyy :
  span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) * span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) ≤
    span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) = ⊤
[PROOFSTEP]
refine' restrictScalars_injective A (Algebra.adjoin A s) C _
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
hyy :
  span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) * span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) ≤
    span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ restrictScalars A (span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)) = restrictScalars A ⊤
[PROOFSTEP]
rw [restrictScalars_top, eq_top_iff, ← Algebra.top_toSubmodule, ← hx, Algebra.adjoin_eq_span, span_le]
[GOAL]
case intro.intro
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
hf : ∀ (x : C), (Finset.sum y fun i => f x i • i) = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ (xi : C), xi ∈ x → xi ∈ span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
hyy :
  span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) * span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y) ≤
    span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)
⊢ ↑(Submonoid.closure ↑x) ⊆ ↑(restrictScalars A (span { x // x ∈ Algebra.adjoin A ↑s } ↑(insert 1 y)))
[PROOFSTEP]
refine' fun r hr =>
  Submonoid.closure_induction hr (fun c hc => hxy c hc) (subset_span <| mem_insert_self _ _) fun p q hp hq =>
    hyy <| Submodule.mul_mem_mul hp hq


[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
⊢ IsIdempotentElem I ↔ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
⊢ IsIdempotentElem I → ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
[PROOFSTEP]
intro e
[GOAL]
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
⊢ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
[PROOFSTEP]
obtain ⟨r, hr, hr'⟩ :=
  Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul I I h
    (by
      rw [smul_eq_mul]
      exact e.ge)
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
⊢ I ≤ I • I
[PROOFSTEP]
rw [smul_eq_mul]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
⊢ I ≤ I * I
[PROOFSTEP]
exact e.ge
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r • n = n
⊢ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
[PROOFSTEP]
simp_rw [smul_eq_mul] at hr'
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r * n = n
⊢ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
[PROOFSTEP]
refine' ⟨r, hr' r hr, antisymm _ ((Submodule.span_singleton_le_iff_mem _ _).mpr hr)⟩
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r * n = n
⊢ I ≤ Submodule.span R {r}
[PROOFSTEP]
intro x hx
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r * n = n
x : R
hx : x ∈ I
⊢ x ∈ Submodule.span R {r}
[PROOFSTEP]
rw [← hr' x hx]
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r * n = n
x : R
hx : x ∈ I
⊢ r * x ∈ Submodule.span R {r}
[PROOFSTEP]
exact Ideal.mem_span_singleton'.mpr ⟨_, mul_comm _ _⟩
[GOAL]
case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
⊢ (∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}) → IsIdempotentElem I
[PROOFSTEP]
rintro ⟨e, he, rfl⟩
[GOAL]
case mpr.intro.intro
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
⊢ IsIdempotentElem (Submodule.span R {e})
[PROOFSTEP]
simp [IsIdempotentElem, Ideal.span_singleton_mul_span_singleton, he.eq]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : FG I
⊢ IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : FG I
⊢ IsIdempotentElem I → I = ⊥ ∨ I = ⊤
[PROOFSTEP]
intro H
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : FG I
H : IsIdempotentElem I
⊢ I = ⊥ ∨ I = ⊤
[PROOFSTEP]
obtain ⟨e, he, rfl⟩ := (I.isIdempotentElem_iff_of_fg h).mp H
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ Submodule.span R {e} = ⊥ ∨ Submodule.span R {e} = ⊤
[PROOFSTEP]
simp only [Ideal.submodule_span_eq, Ideal.span_singleton_eq_bot]
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ e = 0 ∨ span {e} = ⊤
[PROOFSTEP]
apply Or.imp id _ (IsIdempotentElem.iff_eq_zero_or_one.mp he)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ e = 1 → span {e} = ⊤
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
he : IsIdempotentElem 1
h : FG (Submodule.span R {1})
H : IsIdempotentElem (Submodule.span R {1})
⊢ span {1} = ⊤
[PROOFSTEP]
simp
[GOAL]
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : FG I
⊢ I = ⊥ ∨ I = ⊤ → IsIdempotentElem I
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case mpr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : FG ⊥
⊢ IsIdempotentElem ⊥
[PROOFSTEP]
simp [IsIdempotentElem]
[GOAL]
case mpr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : FG ⊤
⊢ IsIdempotentElem ⊤
[PROOFSTEP]
simp [IsIdempotentElem]