[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ (wittStructureRat p Φ)) (W_ ℚ n) =
    ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (↑(bind₁ (xInTermsOfW p ℚ)) (W_ ℚ n))
[PROOFSTEP]
rw [bind₁_bind₁]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ (wittStructureRat p Φ)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ i)) (W_ ℚ n)
[PROOFSTEP]
exact eval₂Hom_congr (RingHom.ext_rat _ _) rfl rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (↑(bind₁ (xInTermsOfW p ℚ)) (W_ ℚ n)) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
[PROOFSTEP]
rw [bind₁_xInTermsOfW_wittPolynomial p _ n, bind₁_X_right]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ ∃! φ, ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
[PROOFSTEP]
refine' ⟨wittStructureRat p Φ, _, _⟩
[GOAL]
case refine'_1
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ (fun φ => ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ) (wittStructureRat p Φ)
[PROOFSTEP]
intro n
[GOAL]
case refine'_1
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ (wittStructureRat p Φ)) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
[PROOFSTEP]
apply wittStructureRat_prop
[GOAL]
case refine'_2
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ ∀ (y : ℕ → MvPolynomial (idx × ℕ) ℚ),
    (fun φ => ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ) y →
      y = wittStructureRat p Φ
[PROOFSTEP]
intro φ H
[GOAL]
case refine'_2
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
⊢ φ = wittStructureRat p Φ
[PROOFSTEP]
funext n
[GOAL]
case refine'_2.h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
n : ℕ
⊢ φ n = wittStructureRat p Φ n
[PROOFSTEP]
rw [show φ n = bind₁ φ (bind₁ (W_ ℚ) (xInTermsOfW p ℚ n)) by rw [bind₁_wittPolynomial_xInTermsOfW p, bind₁_X_right]]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
n : ℕ
⊢ φ n = ↑(bind₁ φ) (↑(bind₁ (W_ ℚ)) (xInTermsOfW p ℚ n))
[PROOFSTEP]
rw [bind₁_wittPolynomial_xInTermsOfW p, bind₁_X_right]
[GOAL]
case refine'_2.h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
n : ℕ
⊢ ↑(bind₁ φ) (↑(bind₁ (W_ ℚ)) (xInTermsOfW p ℚ n)) = wittStructureRat p Φ n
[PROOFSTEP]
rw [bind₁_bind₁]
[GOAL]
case refine'_2.h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
φ : ℕ → MvPolynomial (idx × ℕ) ℚ
H : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
n : ℕ
⊢ ↑(bind₁ fun i => ↑(bind₁ φ) (W_ ℚ i)) (xInTermsOfW p ℚ n) = wittStructureRat p Φ n
[PROOFSTEP]
exact eval₂Hom_congr (RingHom.ext_rat _ _) (funext H) rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n * ↑C (↑p ^ n) =
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
[PROOFSTEP]
have := xInTermsOfW_aux p ℚ n
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this : xInTermsOfW p ℚ n * ↑C (↑p ^ n) = X n - ∑ i in Finset.range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)
⊢ wittStructureRat p Φ n * ↑C (↑p ^ n) =
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
[PROOFSTEP]
replace := congr_arg (bind₁ fun k : ℕ => bind₁ (fun i => rename (Prod.mk i) (W_ ℚ k)) Φ) this
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this :
  ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n * ↑C (↑p ^ n)) =
    ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i in Finset.range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ wittStructureRat p Φ n * ↑C (↑p ^ n) =
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
[PROOFSTEP]
rw [AlgHom.map_mul, bind₁_C_right] at this
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this :
  ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n) * ↑C (↑p ^ n) =
    ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i in Finset.range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ wittStructureRat p Φ n * ↑C (↑p ^ n) =
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
[PROOFSTEP]
rw [wittStructureRat, this]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this :
  ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n) * ↑C (↑p ^ n) =
    ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i in Finset.range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i in Finset.range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) =
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
[PROOFSTEP]
clear this
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i in Finset.range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) =
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
[PROOFSTEP]
conv_lhs => simp only [AlgHom.map_sub, bind₁_X_right]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
| ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
    (X n - ∑ i in Finset.range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
[PROOFSTEP]
simp only [AlgHom.map_sub, bind₁_X_right]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
| ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
    (X n - ∑ i in Finset.range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
[PROOFSTEP]
simp only [AlgHom.map_sub, bind₁_X_right]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
| ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
    (X n - ∑ i in Finset.range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
[PROOFSTEP]
simp only [AlgHom.map_sub, bind₁_X_right]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ -
      ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
        (∑ x in Finset.range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) =
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) Φ -
      ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
[PROOFSTEP]
rw [sub_right_inj]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (∑ x in Finset.range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
[PROOFSTEP]
simp only [AlgHom.map_sum, AlgHom.map_mul, bind₁_C_right, AlgHom.map_pow]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ∑ x in Finset.range n,
      ↑C (↑p ^ x) *
        ↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ x) ^ p ^ (n - x) =
    ∑ x in Finset.range n, ↑C (↑p ^ x) * wittStructureRat p Φ x ^ p ^ (n - x)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n =
    ↑C (1 / ↑p ^ n) *
      (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) Φ -
        ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))
[PROOFSTEP]
calc
  wittStructureRat p Φ n = C (1 / (p : ℚ) ^ n) * (wittStructureRat p Φ n * C ((p : ℚ) ^ n)) := ?_
  _ = _ := by rw [wittStructureRat_rec_aux]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑C (1 / ↑p ^ n) * (wittStructureRat p Φ n * ↑C (↑p ^ n)) =
    ↑C (1 / ↑p ^ n) *
      (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) Φ -
        ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))
[PROOFSTEP]
rw [wittStructureRat_rec_aux]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ wittStructureRat p Φ n = ↑C (1 / ↑p ^ n) * (wittStructureRat p Φ n * ↑C (↑p ^ n))
[PROOFSTEP]
rw [mul_left_comm, ← C_mul, div_mul_cancel, C_1, mul_one]
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑p ^ n ≠ 0
[PROOFSTEP]
exact pow_ne_zero _ (Nat.cast_ne_zero.2 hp.1.ne_zero)
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ =
    ↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n)
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑(map (Int.castRingHom ℚ)) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ) =
    ↑(map (Int.castRingHom ℚ)) (↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
[PROOFSTEP]
simp only [map_bind₁, map_rename, map_expand, rename_expand, map_wittPolynomial]
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑(bind₁ fun i => ↑(expand p) (↑(rename fun i_1 => (i, i_1)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
[PROOFSTEP]
have key := (wittStructureRat_prop p (map (Int.castRingHom ℚ) Φ) n).symm
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n)
⊢ ↑(bind₁ fun i => ↑(expand p) (↑(rename fun i_1 => (i, i_1)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
[PROOFSTEP]
apply_fun expand p at key
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(expand p) (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)) =
    ↑(expand p) (↑(bind₁ (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n))
⊢ ↑(bind₁ fun i => ↑(expand p) (↑(rename fun i_1 => (i, i_1)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
[PROOFSTEP]
simp only [expand_bind₁] at key
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(bind₁ fun i => ↑(expand p) (↑(rename (Prod.mk i)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n)
⊢ ↑(bind₁ fun i => ↑(expand p) (↑(rename fun i_1 => (i, i_1)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
[PROOFSTEP]
rw [key]
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(bind₁ fun i => ↑(expand p) (↑(rename (Prod.mk i)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n)
⊢ ↑(bind₁ fun i => ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
[PROOFSTEP]
clear key
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑(bind₁ fun i => ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
[PROOFSTEP]
apply eval₂Hom_congr' rfl _ rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ∀ (i : ℕ),
    i ∈ vars (W_ ℚ n) →
      i ∈ vars (W_ ℚ n) →
        ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i) =
          ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
[PROOFSTEP]
rintro i hi -
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
i : ℕ
hi : i ∈ vars (W_ ℚ n)
⊢ ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i) =
    ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
[PROOFSTEP]
rw [wittPolynomial_vars, Finset.mem_range] at hi
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
i : ℕ
hi : i < n + 1
⊢ ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i) =
    ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
[PROOFSTEP]
simp only [IH i hi]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑C ↑(p ^ n) ∣
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℤ n)) Φ -
      ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
IH :
  ∀ (m : ℕ),
    m < Nat.zero →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑C ↑(p ^ Nat.zero) ∣
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℤ Nat.zero)) Φ -
      ∑ i in Finset.range Nat.zero, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (Nat.zero - i)
[PROOFSTEP]
simp only [isUnit_one, Int.ofNat_zero, Int.ofNat_succ, zero_add, pow_zero, C_1, IsUnit.dvd, Nat.cast_one, Nat.zero_eq]
  -- prepare a useful equation for rewriting
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑C ↑(p ^ Nat.succ n) ∣
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℤ (Nat.succ n))) Φ -
      ∑ i in Finset.range (Nat.succ n), ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (Nat.succ n - i)
[PROOFSTEP]
have key := bind₁_rename_expand_wittPolynomial Φ n IH
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ =
    ↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n)
⊢ ↑C ↑(p ^ Nat.succ n) ∣
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℤ (Nat.succ n))) Φ -
      ∑ i in Finset.range (Nat.succ n), ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (Nat.succ n - i)
[PROOFSTEP]
apply_fun map (Int.castRingHom (ZMod (p ^ (n + 1)))) at key
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ) =
    ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
⊢ ↑C ↑(p ^ Nat.succ n) ∣
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℤ (Nat.succ n))) Φ -
      ∑ i in Finset.range (Nat.succ n), ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (Nat.succ n - i)
[PROOFSTEP]
conv_lhs at key =>
  simp only [map_bind₁, map_rename, map_expand, map_wittPolynomial]
    -- clean up and massage
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ) =
    ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
| ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ)
[PROOFSTEP]
simp only [map_bind₁, map_rename, map_expand, map_wittPolynomial]
    -- clean up and massage
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ) =
    ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
| ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ)
[PROOFSTEP]
simp only [map_bind₁, map_rename, map_expand, map_wittPolynomial]
    -- clean up and massage
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ) =
    ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
| ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ)
[PROOFSTEP]
simp only [map_bind₁, map_rename, map_expand, map_wittPolynomial]
  -- clean up and massage
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (↑(expand p) (W_ (ZMod (p ^ (n + 1))) n)))
      (↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
⊢ ↑C ↑(p ^ Nat.succ n) ∣
    ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℤ (Nat.succ n))) Φ -
      ∑ i in Finset.range (Nat.succ n), ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (Nat.succ n - i)
[PROOFSTEP]
rw [Nat.succ_eq_add_one, C_dvd_iff_zmod, RingHom.map_sub, sub_eq_zero, map_bind₁]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (↑(expand p) (W_ (ZMod (p ^ (n + 1))) n)))
      (↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
⊢ ↑(bind₁ fun i => ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(rename fun i_1 => (i, i_1)) (W_ ℤ (n + 1))))
      (↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    ↑(map (Int.castRingHom (ZMod (p ^ (n + 1)))))
      (∑ i in Finset.range (n + 1), ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i))
[PROOFSTEP]
simp only [map_rename, map_wittPolynomial, wittPolynomial_zmod_self]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (↑(expand p) (W_ (ZMod (p ^ (n + 1))) n)))
      (↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
⊢ ↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (↑(expand p) (W_ (ZMod (p ^ (n + 1))) n)))
      (↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    ↑(map (Int.castRingHom (ZMod (p ^ (n + 1)))))
      (∑ x in Finset.range (n + 1), ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n + 1 - x))
[PROOFSTEP]
rw [key]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (↑(expand p) (W_ (ZMod (p ^ (n + 1))) n)))
      (↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) =
    ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
⊢ ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n)) =
    ↑(map (Int.castRingHom (ZMod (p ^ (n + 1)))))
      (∑ x in Finset.range (n + 1), ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n + 1 - x))
[PROOFSTEP]
clear key IH
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n)) =
    ↑(map (Int.castRingHom (ZMod (p ^ (n + 1)))))
      (∑ x in Finset.range (n + 1), ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n + 1 - x))
[PROOFSTEP]
rw [bind₁, aeval_wittPolynomial, map_sum, map_sum, Finset.sum_congr rfl]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ∀ (x : ℕ),
    x ∈ Finset.range (n + 1) →
      ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ x * ↑(expand p) (wittStructureInt p Φ x) ^ p ^ (n - x)) =
        ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n + 1 - x))
[PROOFSTEP]
intro k hk
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ∈ Finset.range (n + 1)
⊢ ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ k * ↑(expand p) (wittStructureInt p Φ k) ^ p ^ (n - k)) =
    ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑C (↑p ^ k) * wittStructureInt p Φ k ^ p ^ (n + 1 - k))
[PROOFSTEP]
rw [Finset.mem_range, Nat.lt_succ_iff] at hk
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ k * ↑(expand p) (wittStructureInt p Φ k) ^ p ^ (n - k)) =
    ↑(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑C (↑p ^ k) * wittStructureInt p Φ k ^ p ^ (n + 1 - k))
[PROOFSTEP]
rw [← sub_eq_zero, ← RingHom.map_sub, ← C_dvd_iff_zmod, C_eq_coe_nat, ← Nat.cast_pow, ← Nat.cast_pow, C_eq_coe_nat, ←
  mul_sub]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ ↑(p ^ (n + 1)) ∣
    ↑(p ^ k) * (↑(expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))
[PROOFSTEP]
have : p ^ (n + 1) = p ^ k * p ^ (n - k + 1) := by rw [← pow_add, ← add_assoc]; congr 2;
  rw [add_comm, ← tsub_eq_iff_eq_add_of_le hk]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
[PROOFSTEP]
rw [← pow_add, ← add_assoc]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ p ^ (n + 1) = p ^ (k + (n - k) + 1)
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
⊢ n = k + (n - k)
[PROOFSTEP]
rw [add_comm, ← tsub_eq_iff_eq_add_of_le hk]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑(p ^ (n + 1)) ∣
    ↑(p ^ k) * (↑(expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))
[PROOFSTEP]
rw [this]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑(p ^ k * p ^ (n - k + 1)) ∣
    ↑(p ^ k) * (↑(expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))
[PROOFSTEP]
simp only
  -- Porting note: without this, the next `rw` doesn't do anything
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑(p ^ k * p ^ (n - k + 1)) ∣
    ↑(p ^ k) * (↑(expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))
[PROOFSTEP]
rw [Nat.cast_mul, Nat.cast_pow, Nat.cast_pow]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑p ^ k * ↑p ^ (n - k + 1) ∣
    ↑p ^ k * (↑(expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))
[PROOFSTEP]
apply mul_dvd_mul_left ((p : MvPolynomial (idx × ℕ) ℤ) ^ k)
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑p ^ (n - k + 1) ∣ ↑(expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k)
[PROOFSTEP]
rw [show p ^ (n + 1 - k) = p * p ^ (n - k) by rw [← pow_succ, ← tsub_add_eq_add_tsub hk]]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ p ^ (n + 1 - k) = p * p ^ (n - k)
[PROOFSTEP]
rw [← pow_succ, ← tsub_add_eq_add_tsub hk]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑p ^ (n - k + 1) ∣ ↑(expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ (p * p ^ (n - k))
[PROOFSTEP]
rw [pow_mul]
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑p ^ (n - k + 1) ∣ ↑(expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - (wittStructureInt p Φ k ^ p) ^ p ^ (n - k)
[PROOFSTEP]
rw [← Nat.cast_pow]
  -- Porting note: added
    -- the machine!
[GOAL]
case succ
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑(p ^ (n - k + 1)) ∣ ↑(expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - (wittStructureInt p Φ k ^ p) ^ p ^ (n - k)
[PROOFSTEP]
apply dvd_sub_pow_of_dvd_sub
[GOAL]
case succ.h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n k : ℕ
hk : k ≤ n
this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)
⊢ ↑p ∣ ↑(expand p) (wittStructureInt p Φ k) - wittStructureInt p Φ k ^ p
[PROOFSTEP]
rw [← C_eq_coe_nat, C_dvd_iff_zmod, RingHom.map_sub, sub_eq_zero, map_expand, RingHom.map_pow, MvPolynomial.expand_zmod]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) n
[PROOFSTEP]
induction n using Nat.strong_induction_on with
| h n IH => ?_
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) n
[PROOFSTEP]
induction n using Nat.strong_induction_on with
| h n IH => ?_
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) n
[PROOFSTEP]
rw [wittStructureInt, map_mapRange_eq_iff, Int.coe_castRingHom]
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ∀ (d : idx × ℕ →₀ ℕ),
    (fun x => ↑x) (coeff d (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) n)).num =
      coeff d (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) n)
[PROOFSTEP]
intro c
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
⊢ (fun x => ↑x) (coeff c (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) n)).num =
    coeff c (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) n)
[PROOFSTEP]
rw [wittStructureRat_rec, coeff_C_mul, mul_comm, mul_div_assoc', mul_one]
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
⊢ (fun x => ↑x)
      (coeff c
            (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ) -
              ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
          ↑p ^ n).num =
    coeff c
        (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ) -
          ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
      ↑p ^ n
[PROOFSTEP]
have sum_induction_steps :
  map (Int.castRingHom ℚ) (∑ i in range n, C ((p : ℤ) ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in range n, C ((p : ℚ) ^ i) * wittStructureRat p (map (Int.castRingHom ℚ) Φ) i ^ p ^ (n - i) :=
  by
  rw [map_sum]
  apply Finset.sum_congr rfl
  intro i hi
  rw [Finset.mem_range] at hi
  simp only [IH i hi, RingHom.map_mul, RingHom.map_pow, map_C]
  rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
[PROOFSTEP]
rw [map_sum]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
⊢ ∑ x in Finset.range n, ↑(map (Int.castRingHom ℚ)) (↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
⊢ ∀ (x : ℕ),
    x ∈ Finset.range n →
      ↑(map (Int.castRingHom ℚ)) (↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x)) =
        ↑C (↑p ^ x) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) x ^ p ^ (n - x)
[PROOFSTEP]
intro i hi
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
i : ℕ
hi : i ∈ Finset.range n
⊢ ↑(map (Int.castRingHom ℚ)) (↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
[PROOFSTEP]
rw [Finset.mem_range] at hi
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
i : ℕ
hi : i < n
⊢ ↑(map (Int.castRingHom ℚ)) (↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
[PROOFSTEP]
simp only [IH i hi, RingHom.map_mul, RingHom.map_pow, map_C]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
i : ℕ
hi : i < n
⊢ ↑C (↑(Int.castRingHom ℚ) ↑p) ^ i * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i) =
    ↑C ↑p ^ i * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
[PROOFSTEP]
rfl
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ (fun x => ↑x)
      (coeff c
            (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ) -
              ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
          ↑p ^ n).num =
    coeff c
        (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ) -
          ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) /
      ↑p ^ n
[PROOFSTEP]
simp only [← sum_induction_steps, ← map_wittPolynomial p (Int.castRingHom ℚ), ← map_rename, ← map_bind₁, ←
  RingHom.map_sub, coeff_map]
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑(↑(Int.castRingHom ℚ)
            (coeff c
              (↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
                ∑ x in Finset.range n, ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x))) /
          ↑p ^ n).num =
    ↑(Int.castRingHom ℚ)
        (coeff c
          (↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
            ∑ x in Finset.range n, ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x))) /
      ↑p ^ n
[PROOFSTEP]
rw [show (p : ℚ) ^ n = ((↑(p ^ n) : ℤ) : ℚ) by norm_cast]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑p ^ n = ↑↑(p ^ n)
[PROOFSTEP]
norm_cast
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑(↑(Int.castRingHom ℚ)
            (coeff c
              (↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
                ∑ x in Finset.range n, ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x))) /
          ↑↑(p ^ n)).num =
    ↑(Int.castRingHom ℚ)
        (coeff c
          (↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
            ∑ x in Finset.range n, ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x))) /
      ↑↑(p ^ n)
[PROOFSTEP]
rw [← Rat.den_eq_one_iff, eq_intCast, Rat.den_div_cast_eq_one_iff]
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑(p ^ n) ∣
    coeff c
      (↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
        ∑ x in Finset.range n, ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x))
case h.hn
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑(p ^ n) ≠ 0
[PROOFSTEP]
swap
[GOAL]
case h.hn
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑(p ^ n) ≠ 0
[PROOFSTEP]
exact_mod_cast pow_ne_zero n hp.1.ne_zero
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
c : idx × ℕ →₀ ℕ
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑(p ^ n) ∣
    coeff c
      (↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
        ∑ x in Finset.range n, ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x))
[PROOFSTEP]
revert c
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ∀ (c : idx × ℕ →₀ ℕ),
    ↑(p ^ n) ∣
      coeff c
        (↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
          ∑ x in Finset.range n, ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x))
[PROOFSTEP]
rw [← C_dvd_iff_dvd_coeff]
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n → ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
sum_induction_steps :
  ↑(map (Int.castRingHom ℚ)) (∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
    ∑ i in Finset.range n, ↑C (↑p ^ i) * wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)
⊢ ↑C ↑(p ^ n) ∣
    ↑(bind₁ fun i => ↑(rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ -
      ∑ x in Finset.range n, ↑C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n - x)
[PROOFSTEP]
exact C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum Φ n IH
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(bind₁ (wittStructureInt p Φ)) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (↑(bind₁ (wittStructureInt p Φ)) (W_ ℤ n)) =
    ↑(map (Int.castRingHom ℚ)) (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ)
[PROOFSTEP]
have := wittStructureRat_prop p (map (Int.castRingHom ℚ) Φ) n
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
this :
  ↑(bind₁ (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
⊢ ↑(map (Int.castRingHom ℚ)) (↑(bind₁ (wittStructureInt p Φ)) (W_ ℤ n)) =
    ↑(map (Int.castRingHom ℚ)) (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ)
[PROOFSTEP]
simpa only [map_bind₁, ← eval₂Hom_map_hom, eval₂Hom_C_left, map_rename, map_wittPolynomial, AlgHom.coe_toRingHom,
  map_wittStructureInt]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ φ = wittStructureInt p Φ
[PROOFSTEP]
funext k
[GOAL]
case h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ φ k = wittStructureInt p Φ k
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case h.a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (φ k) = ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ k)
[PROOFSTEP]
rw [map_wittStructureInt]
  -- Porting note: was `refine' congr_fun _ k`
[GOAL]
case h.a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k
[PROOFSTEP]
revert k
[GOAL]
case h.a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ∀ (k : ℕ), ↑(map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k
[PROOFSTEP]
refine' congr_fun _
[GOAL]
case h.a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ (fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) = fun k => wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k
[PROOFSTEP]
apply ExistsUnique.unique (wittStructureRat_existsUnique p (map (Int.castRingHom ℚ) Φ))
[GOAL]
case h.a.py₁
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ∀ (n : ℕ),
    ↑(bind₁ fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
      ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
[PROOFSTEP]
intro n
[GOAL]
case h.a.py₁
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
n : ℕ
⊢ ↑(bind₁ fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
[PROOFSTEP]
specialize h n
[GOAL]
case h.a.py₁
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
n : ℕ
h : ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ↑(bind₁ fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
[PROOFSTEP]
apply_fun map (Int.castRingHom ℚ) at h
[GOAL]
case h.a.py₁
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
n : ℕ
h :
  ↑(map (Int.castRingHom ℚ)) (↑(bind₁ φ) (W_ ℤ n)) =
    ↑(map (Int.castRingHom ℚ)) (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ)
⊢ ↑(bind₁ fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
[PROOFSTEP]
simpa only [map_bind₁, ← eval₂Hom_map_hom, eval₂Hom_C_left, map_rename, map_wittPolynomial, AlgHom.coe_toRingHom] using
  h
[GOAL]
case h.a.py₂
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ∀ (n : ℕ),
    ↑(bind₁ fun k => wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k) (W_ ℚ n) =
      ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
[PROOFSTEP]
intro n
[GOAL]
case h.a.py₂
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
n : ℕ
⊢ ↑(bind₁ fun k => wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
[PROOFSTEP]
apply wittStructureRat_prop
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(aeval fun i => ↑(map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) =
    ↑(aeval fun i => ↑(rename (Prod.mk i)) (W_ R n)) Φ
[PROOFSTEP]
convert congr_arg (map (Int.castRingHom R)) (wittStructureInt_prop p Φ n) using 1
[GOAL]
case h.e'_2
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(aeval fun i => ↑(map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) =
    ↑(map (Int.castRingHom R)) (↑(bind₁ (wittStructureInt p Φ)) (W_ ℤ n))
[PROOFSTEP]
rw [hom_bind₁]
[GOAL]
case h.e'_3
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(aeval fun i => ↑(rename (Prod.mk i)) (W_ R n)) Φ =
    ↑(map (Int.castRingHom R)) (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ)
[PROOFSTEP]
rw [hom_bind₁]
[GOAL]
case h.e'_2
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(aeval fun i => ↑(map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) =
    ↑(eval₂Hom (RingHom.comp (map (Int.castRingHom R)) C) fun i => ↑(map (Int.castRingHom R)) (wittStructureInt p Φ i))
      (W_ ℤ n)
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
case h.e'_3
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ ↑(aeval fun i => ↑(rename (Prod.mk i)) (W_ R n)) Φ =
    ↑(eval₂Hom (RingHom.comp (map (Int.castRingHom R)) C) fun i =>
          ↑(map (Int.castRingHom R)) (↑(rename (Prod.mk i)) (W_ ℤ n)))
      Φ
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (fun i => ↑(map (Int.castRingHom R)) (wittStructureInt p Φ i)) = fun i =>
    ↑(map (Int.castRingHom R)) (wittStructureInt p Φ i)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (fun i => ↑(rename (Prod.mk i)) (W_ R n)) = fun i => ↑(map (Int.castRingHom R)) (↑(rename (Prod.mk i)) (W_ ℤ n))
[PROOFSTEP]
simp only [map_rename, map_wittPolynomial]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ wittStructureInt p (↑(rename f) Φ) n = ↑(rename (Prod.map f id)) (wittStructureInt p Φ n)
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (wittStructureInt p (↑(rename f) Φ) n) =
    ↑(map (Int.castRingHom ℚ)) (↑(rename (Prod.map f id)) (wittStructureInt p Φ n))
[PROOFSTEP]
simp only [map_rename, map_wittStructureInt, wittStructureRat, rename_bind₁, rename_rename, bind₁_rename]
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ ↑(bind₁ fun k => ↑(bind₁ ((fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) ∘ f)) (↑(map (Int.castRingHom ℚ)) Φ))
      (xInTermsOfW p ℚ n) =
    ↑(bind₁ fun i =>
          ↑(bind₁ fun i_1 => ↑(rename (Prod.map f id ∘ Prod.mk i_1)) (W_ ℚ i)) (↑(map (Int.castRingHom ℚ)) Φ))
      (xInTermsOfW p ℚ n)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ ↑constantCoeff (wittStructureRat p Φ 0) = ↑constantCoeff Φ
[PROOFSTEP]
simp only [wittStructureRat, bind₁, map_aeval, xInTermsOfW_zero, constantCoeff_rename, constantCoeff_wittPolynomial,
  aeval_X, constantCoeff_comp_algebraMap, eval₂Hom_zero'_apply, RingHom.id_apply]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
h : ↑constantCoeff Φ = 0
n : ℕ
⊢ ↑constantCoeff (wittStructureRat p Φ n) = 0
[PROOFSTEP]
simp only [wittStructureRat, eval₂Hom_zero'_apply, h, bind₁, map_aeval, constantCoeff_rename,
  constantCoeff_wittPolynomial, constantCoeff_comp_algebraMap, RingHom.id_apply, constantCoeff_xInTermsOfW]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
⊢ ↑constantCoeff (wittStructureInt p Φ 0) = ↑constantCoeff Φ
[PROOFSTEP]
have inj : Function.Injective (Int.castRingHom ℚ) := by intro m n; exact Int.cast_inj.mp
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
⊢ Function.Injective ↑(Int.castRingHom ℚ)
[PROOFSTEP]
intro m n
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
m n : ℤ
⊢ ↑(Int.castRingHom ℚ) m = ↑(Int.castRingHom ℚ) n → m = n
[PROOFSTEP]
exact Int.cast_inj.mp
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ↑(Int.castRingHom ℚ)
⊢ ↑constantCoeff (wittStructureInt p Φ 0) = ↑constantCoeff Φ
[PROOFSTEP]
apply inj
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective ↑(Int.castRingHom ℚ)
⊢ ↑(Int.castRingHom ℚ) (↑constantCoeff (wittStructureInt p Φ 0)) = ↑(Int.castRingHom ℚ) (↑constantCoeff Φ)
[PROOFSTEP]
rw [← constantCoeff_map, map_wittStructureInt, constantCoeff_wittStructureRat_zero, constantCoeff_map]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : ↑constantCoeff Φ = 0
n : ℕ
⊢ ↑constantCoeff (wittStructureInt p Φ n) = 0
[PROOFSTEP]
have inj : Function.Injective (Int.castRingHom ℚ) := by intro m n; exact Int.cast_inj.mp
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : ↑constantCoeff Φ = 0
n : ℕ
⊢ Function.Injective ↑(Int.castRingHom ℚ)
[PROOFSTEP]
intro m n
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : ↑constantCoeff Φ = 0
n✝ : ℕ
m n : ℤ
⊢ ↑(Int.castRingHom ℚ) m = ↑(Int.castRingHom ℚ) n → m = n
[PROOFSTEP]
exact Int.cast_inj.mp
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : ↑constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ↑(Int.castRingHom ℚ)
⊢ ↑constantCoeff (wittStructureInt p Φ n) = 0
[PROOFSTEP]
apply inj
[GOAL]
case a
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : ↑constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ↑(Int.castRingHom ℚ)
⊢ ↑(Int.castRingHom ℚ) (↑constantCoeff (wittStructureInt p Φ n)) = ↑(Int.castRingHom ℚ) 0
[PROOFSTEP]
rw [← constantCoeff_map, map_wittStructureInt, constantCoeff_wittStructureRat, RingHom.map_zero]
[GOAL]
case a.h
p : ℕ
R : Type u_1
idx : Type u_2
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : ↑constantCoeff Φ = 0
n : ℕ
inj : Function.Injective ↑(Int.castRingHom ℚ)
⊢ ↑constantCoeff (↑(map (Int.castRingHom ℚ)) Φ) = 0
[PROOFSTEP]
rw [constantCoeff_map, h, RingHom.map_zero]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ vars (wittStructureRat p Φ n) ⊆ Finset.univ ×ˢ Finset.range (n + 1)
[PROOFSTEP]
rw [wittStructureRat]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)) ⊆
    Finset.univ ×ˢ Finset.range (n + 1)
[PROOFSTEP]
intro x hx
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
⊢ x ∈ Finset.univ ×ˢ Finset.range (n + 1)
[PROOFSTEP]
simp only [Finset.mem_product, true_and_iff, Finset.mem_univ, Finset.mem_range]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
⊢ x.snd < n + 1
[PROOFSTEP]
obtain ⟨k, hk, hx'⟩ := mem_vars_bind₁ _ _ hx
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
hx' : x ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
⊢ x.snd < n + 1
[PROOFSTEP]
obtain ⟨i, -, hx''⟩ := mem_vars_bind₁ _ _ hx'
[GOAL]
case intro.intro.intro.intro
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
hx' : x ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
i : idx
hx'' : x ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
⊢ x.snd < n + 1
[PROOFSTEP]
obtain ⟨j, hj, rfl⟩ := mem_vars_rename _ _ hx''
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
i : idx
j : ℕ
hj : j ∈ vars (W_ ℚ k)
hx : (i, j) ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
hx' : (i, j) ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
hx'' : (i, j) ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
⊢ (i, j).snd < n + 1
[PROOFSTEP]
rw [wittPolynomial_vars, Finset.mem_range] at hj
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
hx' : (i, j) ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
hx'' : (i, j) ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
⊢ (i, j).snd < n + 1
[PROOFSTEP]
replace hk := xInTermsOfW_vars_subset p _ hk
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
hx' : (i, j) ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
hx'' : (i, j) ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
hk : k ∈ Finset.range (n + 1)
⊢ (i, j).snd < n + 1
[PROOFSTEP]
rw [Finset.mem_range] at hk
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
hx' : (i, j) ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
hx'' : (i, j) ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
hk : k < n + 1
⊢ (i, j).snd < n + 1
[PROOFSTEP]
exact lt_of_lt_of_le hj hk
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ vars (wittStructureInt p Φ n) ⊆ Finset.univ ×ˢ Finset.range (n + 1)
[PROOFSTEP]
have : Function.Injective (Int.castRingHom ℚ) := Int.cast_injective
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
this : Function.Injective ↑(Int.castRingHom ℚ)
⊢ vars (wittStructureInt p Φ n) ⊆ Finset.univ ×ˢ Finset.range (n + 1)
[PROOFSTEP]
rw [← vars_map_of_injective _ this, map_wittStructureInt]
[GOAL]
p : ℕ
R : Type u_1
idx : Type u_2
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℤ
n : ℕ
this : Function.Injective ↑(Int.castRingHom ℚ)
⊢ vars (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) n) ⊆ Finset.univ ×ˢ Finset.range (n + 1)
[PROOFSTEP]
apply wittStructureRat_vars


[GOAL]
σ : Type u
R : Type v
inst✝¹ : CommRing R
p m : ℕ
inst✝ : CharP R p
n : ℕ
⊢ ↑n = 0 ↔ p ∣ n
[PROOFSTEP]
rw [← C_eq_coe_nat, ← C_0, C_inj, CharP.cast_eq_zero_iff R p]
[GOAL]
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
⊢ Finsupp.mapRange ↑f (_ : ↑f 0 = 0) p = ↑(map f) p
[PROOFSTEP]
change Finsupp.mapRange (f : R →+ S) (f : R →+ S).map_zero p = map f p
[GOAL]
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
⊢ Finsupp.mapRange ↑↑f (_ : ↑↑f 0 = 0) p = ↑(map f) p
[PROOFSTEP]
rw [p.as_sum, Finsupp.mapRange_finset_sum, (map f).map_sum]
[GOAL]
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
⊢ ∑ x in support p, Finsupp.mapRange ↑↑f (_ : ↑↑f 0 = 0) (↑(monomial x) (coeff x p)) =
    ∑ x in support p, ↑(map f) (↑(monomial x) (coeff x p))
[PROOFSTEP]
refine' Finset.sum_congr rfl fun n _ => _
[GOAL]
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
n : σ →₀ ℕ
x✝ : n ∈ support p
⊢ Finsupp.mapRange ↑↑f (_ : ↑↑f 0 = 0) (↑(monomial n) (coeff n p)) = ↑(map f) (↑(monomial n) (coeff n p))
[PROOFSTEP]
rw [map_monomial, ← single_eq_monomial, Finsupp.mapRange_single, single_eq_monomial]
[GOAL]
σ : Type u
R✝ : Type v
inst✝² : CommRing R✝
p✝ m : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
p : MvPolynomial σ R
f : R →+* S
n : σ →₀ ℕ
x✝ : n ∈ support p
⊢ ↑(monomial n) (↑↑f (coeff n p)) = ↑(monomial n) (↑f (coeff n p))
[PROOFSTEP]
simp_all only [AddMonoidHom.coe_coe]
[GOAL]
σ : Type u
R : Type v
inst✝ : CommRing R
p✝ m : ℕ
p : MvPolynomial σ R
⊢ p ∈ restrictTotalDegree σ R m ↔ totalDegree p ≤ m
[PROOFSTEP]
rw [totalDegree, Finset.sup_le_iff]
[GOAL]
σ : Type u
R : Type v
inst✝ : CommRing R
p✝ m : ℕ
p : MvPolynomial σ R
⊢ p ∈ restrictTotalDegree σ R m ↔ ∀ (b : σ →₀ ℕ), b ∈ support p → (Finsupp.sum b fun x e => e) ≤ m
[PROOFSTEP]
rfl
[GOAL]
σ : Type u
R : Type v
inst✝ : CommRing R
p✝ m : ℕ
p : MvPolynomial σ R
n : ℕ
⊢ p ∈ restrictDegree σ R n ↔ ∀ (s : σ →₀ ℕ), s ∈ support p → ∀ (i : σ), ↑s i ≤ n
[PROOFSTEP]
rw [restrictDegree, Finsupp.mem_supported]
[GOAL]
σ : Type u
R : Type v
inst✝ : CommRing R
p✝ m : ℕ
p : MvPolynomial σ R
n : ℕ
⊢ ↑p.support ⊆ {n_1 | ∀ (i : σ), ↑n_1 i ≤ n} ↔ ∀ (s : σ →₀ ℕ), s ∈ support p → ∀ (i : σ), ↑s i ≤ n
[PROOFSTEP]
rfl
[GOAL]
σ : Type u
R : Type v
inst✝¹ : CommRing R
p✝ m : ℕ
inst✝ : DecidableEq σ
p : MvPolynomial σ R
n : ℕ
⊢ p ∈ restrictDegree σ R n ↔ ∀ (i : σ), Multiset.count i (degrees p) ≤ n
[PROOFSTEP]
simp only [mem_restrictDegree, degrees_def, Multiset.count_finset_sup, Finsupp.count_toMultiset, Finset.sup_le_iff]
[GOAL]
σ : Type u
R : Type v
inst✝¹ : CommRing R
p✝ m : ℕ
inst✝ : DecidableEq σ
p : MvPolynomial σ R
n : ℕ
⊢ (∀ (s : σ →₀ ℕ), s ∈ support p → ∀ (i : σ), ↑s i ≤ n) ↔ ∀ (i : σ) (b : σ →₀ ℕ), b ∈ support p → ↑b i ≤ n
[PROOFSTEP]
exact ⟨fun h n s hs => h s hs n, fun h s hs n => h n s hs⟩


[GOAL]
⊢ StableUnderComposition fun {R S} [CommRing R] [CommRing S] f => IsIntegral f
[PROOFSTEP]
introv R hf hg
[GOAL]
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : IsIntegral f
hg : IsIntegral g
⊢ IsIntegral (comp g f)
[PROOFSTEP]
exact RingHom.isIntegral_trans _ _ hf hg
[GOAL]
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] f => IsIntegral f
[PROOFSTEP]
apply isIntegral_stableUnderComposition.respectsIso
[GOAL]
⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), IsIntegral (RingEquiv.toRingHom e)
[PROOFSTEP]
introv x
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
x : S
⊢ IsIntegralElem (RingEquiv.toRingHom e) x
[PROOFSTEP]
rw [← e.apply_symm_apply x]
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
x : S
⊢ IsIntegralElem (RingEquiv.toRingHom e) (↑e (↑(RingEquiv.symm e) x))
[PROOFSTEP]
apply RingHom.is_integral_map
[GOAL]
⊢ StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] f => IsIntegral f
[PROOFSTEP]
refine' StableUnderBaseChange.mk _ isIntegral_respectsIso _
[GOAL]
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], IsIntegral (algebraMap R T) → IsIntegral includeLeftRingHom
[PROOFSTEP]
introv h x
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : IsIntegral (algebraMap R T)
x : S ⊗[R] T
⊢ IsIntegralElem includeLeftRingHom x
[PROOFSTEP]
refine' TensorProduct.induction_on x _ _ _
[GOAL]
case refine'_1
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : IsIntegral (algebraMap R T)
x : S ⊗[R] T
⊢ IsIntegralElem includeLeftRingHom 0
[PROOFSTEP]
apply isIntegral_zero
[GOAL]
case refine'_2
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : IsIntegral (algebraMap R T)
x : S ⊗[R] T
⊢ ∀ (x : S) (y : T), IsIntegralElem includeLeftRingHom (x ⊗ₜ[R] y)
[PROOFSTEP]
intro x y
[GOAL]
case refine'_2
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : IsIntegral (algebraMap R T)
x✝ : S ⊗[R] T
x : S
y : T
⊢ IsIntegralElem includeLeftRingHom (x ⊗ₜ[R] y)
[PROOFSTEP]
exact IsIntegral.tmul x (h y)
[GOAL]
case refine'_3
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : IsIntegral (algebraMap R T)
x : S ⊗[R] T
⊢ ∀ (x y : S ⊗[R] T),
    IsIntegralElem includeLeftRingHom x →
      IsIntegralElem includeLeftRingHom y → IsIntegralElem includeLeftRingHom (x + y)
[PROOFSTEP]
intro x y hx hy
[GOAL]
case refine'_3
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : IsIntegral (algebraMap R T)
x✝ x y : S ⊗[R] T
hx : IsIntegralElem includeLeftRingHom x
hy : IsIntegralElem includeLeftRingHom y
⊢ IsIntegralElem includeLeftRingHom (x + y)
[PROOFSTEP]
exact isIntegral_add hx hy


[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
h : ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P
⊢ ∃! I, Ideal.IsMaximal I
[PROOFSTEP]
rcases h with ⟨P, ⟨hPnonzero, hPnot_top, _⟩, hPunique⟩
[GOAL]
case intro.intro.intro.mk
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
⊢ ∃! I, Ideal.IsMaximal I
[PROOFSTEP]
refine' ⟨P, ⟨⟨hPnot_top, _⟩⟩, fun M hM => hPunique _ ⟨_, Ideal.IsMaximal.isPrime hM⟩⟩
[GOAL]
case intro.intro.intro.mk.refine'_1
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
⊢ ∀ (b : Ideal R), P < b → b = ⊤
[PROOFSTEP]
refine' Ideal.maximal_of_no_maximal fun M hPM hM => ne_of_lt hPM _
[GOAL]
case intro.intro.intro.mk.refine'_1
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
M : Ideal R
hPM : P < M
hM : Ideal.IsMaximal M
⊢ P = M
[PROOFSTEP]
exact (hPunique _ ⟨ne_bot_of_gt hPM, Ideal.IsMaximal.isPrime hM⟩).symm
[GOAL]
case intro.intro.intro.mk.refine'_2
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
M : Ideal R
hM : (fun I => Ideal.IsMaximal I) M
⊢ M ≠ ⊥
[PROOFSTEP]
rintro rfl
[GOAL]
case intro.intro.intro.mk.refine'_2
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ Ideal.IsPrime P) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
hM : Ideal.IsMaximal ⊥
⊢ False
[PROOFSTEP]
exact hPnot_top (hM.1.2 P (bot_lt_iff_ne_bot.2 hPnonzero))
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
a b : R
h : IsUnit (a + b)
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
rcases h with ⟨u, hu⟩
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
a b : R
u : Rˣ
hu : ↑u = a + b
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
rw [← Units.inv_mul_eq_one, mul_add] at hu
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
a b : R
u : Rˣ
hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
apply Or.imp _ _ (isUnit_or_isUnit_of_add_one hu)
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
a b : R
u : Rˣ
hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1
⊢ IsUnit (↑u⁻¹ * a) → IsUnit a
[PROOFSTEP]
exact isUnit_of_mul_isUnit_right
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
a b : R
u : Rˣ
hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1
⊢ IsUnit (↑u⁻¹ * b) → IsUnit b
[PROOFSTEP]
exact isUnit_of_mul_isUnit_right
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
⊢ Ideal.IsMaximal (maximalIdeal R)
[PROOFSTEP]
rw [Ideal.isMaximal_iff]
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
⊢ ¬1 ∈ maximalIdeal R ∧ ∀ (J : Ideal R) (x : R), maximalIdeal R ≤ J → ¬x ∈ maximalIdeal R → x ∈ J → 1 ∈ J
[PROOFSTEP]
constructor
[GOAL]
case left
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
⊢ ¬1 ∈ maximalIdeal R
[PROOFSTEP]
intro h
[GOAL]
case left
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
h : 1 ∈ maximalIdeal R
⊢ False
[PROOFSTEP]
apply h
[GOAL]
case left
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
h : 1 ∈ maximalIdeal R
⊢ IsUnit 1
[PROOFSTEP]
exact isUnit_one
[GOAL]
case right
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
⊢ ∀ (J : Ideal R) (x : R), maximalIdeal R ≤ J → ¬x ∈ maximalIdeal R → x ∈ J → 1 ∈ J
[PROOFSTEP]
intro I x _ hx H
[GOAL]
case right
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
I : Ideal R
x : R
a✝ : maximalIdeal R ≤ I
hx : ¬x ∈ maximalIdeal R
H : x ∈ I
⊢ 1 ∈ I
[PROOFSTEP]
erw [Classical.not_not] at hx
[GOAL]
case right
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
I : Ideal R
x : R
a✝ : maximalIdeal R ≤ I
hx : IsUnit x
H : x ∈ I
⊢ 1 ∈ I
[PROOFSTEP]
rcases hx with ⟨u, rfl⟩
[GOAL]
case right.intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
I : Ideal R
a✝ : maximalIdeal R ≤ I
u : Rˣ
H : ↑u ∈ I
⊢ 1 ∈ I
[PROOFSTEP]
simpa using I.mul_mem_left (↑u⁻¹) H
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
J : Ideal R
hJ : J ≠ ⊤
⊢ J ≤ maximalIdeal R
[PROOFSTEP]
rcases Ideal.exists_le_maximal J hJ with ⟨M, hM1, hM2⟩
[GOAL]
case intro.intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommSemiring R
inst✝ : LocalRing R
J : Ideal R
hJ : J ≠ ⊤
M : Ideal R
hM1 : Ideal.IsMaximal M
hM2 : J ≤ M
⊢ J ≤ maximalIdeal R
[PROOFSTEP]
rwa [← eq_maximalIdeal hM1]
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
⊢ ∀ (a : S), IsUnit a ∨ IsUnit (1 - a)
[PROOFSTEP]
intro b
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
b : S
⊢ IsUnit b ∨ IsUnit (1 - b)
[PROOFSTEP]
obtain ⟨a, rfl⟩ := hf b
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
a : R
⊢ IsUnit (↑f a) ∨ IsUnit (1 - ↑f a)
[PROOFSTEP]
apply (isUnit_or_isUnit_one_sub_self a).imp <| RingHom.isUnit_map _
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
a : R
⊢ IsUnit (1 - a) → IsUnit (1 - ↑f a)
[PROOFSTEP]
rw [← f.map_one, ← f.map_sub]
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommRing R
inst✝² : LocalRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ↑f
a : R
⊢ IsUnit (1 - a) → IsUnit (↑f (1 - a))
[PROOFSTEP]
apply f.isUnit_map
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : LocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ Ideal.jacobson I = maximalIdeal R
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : LocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ Ideal.jacobson I ≤ maximalIdeal R
[PROOFSTEP]
exact sInf_le ⟨LocalRing.le_maximalIdeal h, LocalRing.maximalIdeal.isMaximal R⟩
[GOAL]
case a
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : LocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ maximalIdeal R ≤ Ideal.jacobson I
[PROOFSTEP]
exact le_sInf fun J (hJ : I ≤ J ∧ J.IsMaximal) => le_of_eq (LocalRing.eq_maximalIdeal hJ.2).symm
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R ≃+* S
a : R
ha : IsUnit (↑↑f a)
⊢ IsUnit a
[PROOFSTEP]
convert RingHom.isUnit_map (f.symm : S →+* R) ha
[GOAL]
case h.e'_3
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R ≃+* S
a : R
ha : IsUnit (↑↑f a)
⊢ a = ↑↑(RingEquiv.symm f) (↑↑f a)
[PROOFSTEP]
exact (RingEquiv.symm_apply_apply f a).symm
[GOAL]
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
⊢ LocalRing R
[PROOFSTEP]
haveI : Nontrivial R := pullback_nonzero f f.map_zero f.map_one
[GOAL]
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
this : Nontrivial R
⊢ LocalRing R
[PROOFSTEP]
apply LocalRing.of_nonunits_add
[GOAL]
case h
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
this : Nontrivial R
⊢ ∀ (a b : R), a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R
[PROOFSTEP]
intro a b
[GOAL]
case h
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
this : Nontrivial R
a b : R
⊢ a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R
[PROOFSTEP]
simp_rw [← map_mem_nonunits_iff f, f.map_add]
[GOAL]
case h
R✝ : Type u
S✝ : Type v
T : Type w
K : Type u'
inst✝⁵ : Semiring R✝
inst✝⁴ : Semiring S✝
inst✝³ : Semiring T
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
H : LocalRing S
f : R →+* S
inst✝ : IsLocalRingHom f
this : Nontrivial R
a b : R
⊢ ↑f a ∈ nonunits S → ↑f b ∈ nonunits S → ↑f a + ↑f b ∈ nonunits S
[PROOFSTEP]
exact LocalRing.nonunits_add
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
⊢ List.TFAE
    [IsLocalRingHom f, ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R]
[PROOFSTEP]
tfae_have 1 → 2
[GOAL]
case tfae_1_to_2
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
⊢ IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
[PROOFSTEP]
rintro _ _ ⟨a, ha, rfl⟩
[GOAL]
case tfae_1_to_2.intro.intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
✝ : IsLocalRingHom f
a : R
ha : a ∈ ↑(maximalIdeal R).toAddSubmonoid
⊢ ↑f a ∈ ↑(maximalIdeal S)
[PROOFSTEP]
exact map_nonunit f a ha
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
⊢ List.TFAE
    [IsLocalRingHom f, ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R]
[PROOFSTEP]
tfae_have 2 → 4
[GOAL]
case tfae_2_to_4
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
⊢ ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
[PROOFSTEP]
exact Set.image_subset_iff.1
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ List.TFAE
    [IsLocalRingHom f, ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R]
[PROOFSTEP]
tfae_have 3 ↔ 4
[GOAL]
case tfae_3_iff_4
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
[PROOFSTEP]
exact Ideal.map_le_iff_le_comap
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ List.TFAE
    [IsLocalRingHom f, ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R]
[PROOFSTEP]
tfae_have 4 → 1
[GOAL]
case tfae_4_to_1
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalRingHom f
[PROOFSTEP]
intro h
[GOAL]
case tfae_4_to_1
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
h : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ IsLocalRingHom f
[PROOFSTEP]
constructor
[GOAL]
case tfae_4_to_1.map_nonunit
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
h : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ ∀ (a : R), IsUnit (↑f a) → IsUnit a
[PROOFSTEP]
exact fun x => not_imp_not.1 (@h x)
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalRingHom f
⊢ List.TFAE
    [IsLocalRingHom f, ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R]
[PROOFSTEP]
tfae_have 1 → 5
[GOAL]
case tfae_1_to_5
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalRingHom f
⊢ IsLocalRingHom f → Ideal.comap f (maximalIdeal S) = maximalIdeal R
[PROOFSTEP]
intro
[GOAL]
case tfae_1_to_5
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalRingHom f
✝ : IsLocalRingHom f
⊢ Ideal.comap f (maximalIdeal S) = maximalIdeal R
[PROOFSTEP]
ext
[GOAL]
case tfae_1_to_5.h
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalRingHom f
✝ : IsLocalRingHom f
x✝ : R
⊢ x✝ ∈ Ideal.comap f (maximalIdeal S) ↔ x✝ ∈ maximalIdeal R
[PROOFSTEP]
exact not_iff_not.2 (isUnit_map_iff f _)
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalRingHom f
tfae_1_to_5 : IsLocalRingHom f → Ideal.comap f (maximalIdeal S) = maximalIdeal R
⊢ List.TFAE
    [IsLocalRingHom f, ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R]
[PROOFSTEP]
tfae_have 5 → 4
[GOAL]
case tfae_5_to_4
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalRingHom f
tfae_1_to_5 : IsLocalRingHom f → Ideal.comap f (maximalIdeal S) = maximalIdeal R
⊢ Ideal.comap f (maximalIdeal S) = maximalIdeal R → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
[PROOFSTEP]
exact fun h => le_of_eq h.symm
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝³ : CommSemiring R
inst✝² : LocalRing R
inst✝¹ : CommSemiring S
inst✝ : LocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalRingHom f → ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalRingHom f
tfae_1_to_5 : IsLocalRingHom f → Ideal.comap f (maximalIdeal S) = maximalIdeal R
tfae_5_to_4 : Ideal.comap f (maximalIdeal S) = maximalIdeal R → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ List.TFAE
    [IsLocalRingHom f, ↑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R]
[PROOFSTEP]
tfae_finish
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
⊢ ∀ (a b : S), IsUnit (a + b) → IsUnit a ∨ IsUnit b
[PROOFSTEP]
intro a b hab
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
a b : S
hab : IsUnit (a + b)
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
obtain ⟨a, rfl⟩ := hf a
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
b : S
a : R
hab : IsUnit (↑f a + b)
⊢ IsUnit (↑f a) ∨ IsUnit b
[PROOFSTEP]
obtain ⟨b, rfl⟩ := hf b
[GOAL]
case intro.intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
a b : R
hab : IsUnit (↑f a + ↑f b)
⊢ IsUnit (↑f a) ∨ IsUnit (↑f b)
[PROOFSTEP]
rw [← map_add] at hab
[GOAL]
case intro.intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁴ : CommSemiring R
inst✝³ : LocalRing R
inst✝² : CommSemiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalRingHom f
hf : Function.Surjective ↑f
a b : R
hab : IsUnit (↑f (a + b))
⊢ IsUnit (↑f a) ∨ IsUnit (↑f b)
[PROOFSTEP]
exact (isUnit_or_isUnit_of_isUnit_add <| IsLocalRingHom.map_nonunit _ hab).imp f.isUnit_map f.isUnit_map
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
⊢ Function.Surjective ↑(Units.map ↑f)
[PROOFSTEP]
intro a
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
⊢ ∃ a_1, ↑(Units.map ↑f) a_1 = a
[PROOFSTEP]
obtain ⟨b, hb⟩ := hf (a : S)
[GOAL]
case intro
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ ∃ a_1, ↑(Units.map ↑f) a_1 = a
[PROOFSTEP]
use(isUnit_of_map_unit f b (by rw [hb]; exact Units.isUnit _)).unit
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ IsUnit (↑f b)
[PROOFSTEP]
rw [hb]
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ IsUnit ↑a
[PROOFSTEP]
exact Units.isUnit _
[GOAL]
case h
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ ↑(Units.map ↑f) (IsUnit.unit (_ : IsUnit b)) = a
[PROOFSTEP]
ext
[GOAL]
case h.a
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ↑f
h : IsLocalRingHom f
a : Sˣ
b : R
hb : ↑f b = ↑a
⊢ ↑(↑(Units.map ↑f) (IsUnit.unit (_ : IsUnit b))) = ↑a
[PROOFSTEP]
exact hb
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁶ : CommRing R
inst✝⁵ : LocalRing R
inst✝⁴ : CommRing S
inst✝³ : LocalRing S
inst✝² : CommRing T
inst✝¹ : LocalRing T
f : R →+* S
inst✝ : IsLocalRingHom f
a : R
ha : a ∈ maximalIdeal R
⊢ ↑(RingHom.comp (Ideal.Quotient.mk (maximalIdeal S)) f) a = 0
[PROOFSTEP]
erw [Ideal.Quotient.eq_zero_iff_mem]
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁶ : CommRing R
inst✝⁵ : LocalRing R
inst✝⁴ : CommRing S
inst✝³ : LocalRing S
inst✝² : CommRing T
inst✝¹ : LocalRing T
f : R →+* S
inst✝ : IsLocalRingHom f
a : R
ha : a ∈ maximalIdeal R
⊢ ↑f a ∈ maximalIdeal S
[PROOFSTEP]
exact map_nonunit f a ha
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁵ : CommRing R
inst✝⁴ : LocalRing R
inst✝³ : CommRing S
inst✝² : LocalRing S
inst✝¹ : CommRing T
inst✝ : LocalRing T
f : R ≃+* S
x : ResidueField R
⊢ ↑(map ↑(RingEquiv.symm f)) (↑(map ↑f) x) = x
[PROOFSTEP]
simp only [map_map, RingEquiv.symm_comp, map_id, RingHom.id_apply]
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁵ : CommRing R
inst✝⁴ : LocalRing R
inst✝³ : CommRing S
inst✝² : LocalRing S
inst✝¹ : CommRing T
inst✝ : LocalRing T
f : R ≃+* S
x : ResidueField S
⊢ ↑(map ↑f) (↑(map ↑(RingEquiv.symm f)) x) = x
[PROOFSTEP]
simp only [map_map, RingEquiv.comp_symm, map_id, RingHom.id_apply]
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁵ : CommRing R
inst✝⁴ : LocalRing R
inst✝³ : CommRing S
inst✝² : LocalRing S
inst✝¹ : CommRing T
inst✝ : LocalRing T
⊢ IsLocalRingHom (residue R)
[PROOFSTEP]
constructor
[GOAL]
case map_nonunit
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁵ : CommRing R
inst✝⁴ : LocalRing R
inst✝³ : CommRing S
inst✝² : LocalRing S
inst✝¹ : CommRing T
inst✝ : LocalRing T
⊢ ∀ (a : R), IsUnit (↑(residue R) a) → IsUnit a
[PROOFSTEP]
intro a ha
[GOAL]
case map_nonunit
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁵ : CommRing R
inst✝⁴ : LocalRing R
inst✝³ : CommRing S
inst✝² : LocalRing S
inst✝¹ : CommRing T
inst✝ : LocalRing T
a : R
ha : IsUnit (↑(residue R) a)
⊢ IsUnit a
[PROOFSTEP]
by_contra h
[GOAL]
case map_nonunit
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁵ : CommRing R
inst✝⁴ : LocalRing R
inst✝³ : CommRing S
inst✝² : LocalRing S
inst✝¹ : CommRing T
inst✝ : LocalRing T
a : R
ha : IsUnit (↑(residue R) a)
h : ¬IsUnit a
⊢ False
[PROOFSTEP]
erw [Ideal.Quotient.eq_zero_iff_mem.mpr ((LocalRing.mem_maximalIdeal _).mpr h)] at ha
[GOAL]
case map_nonunit
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝⁵ : CommRing R
inst✝⁴ : LocalRing R
inst✝³ : CommRing S
inst✝² : LocalRing S
inst✝¹ : CommRing T
inst✝ : LocalRing T
a : R
ha : IsUnit 0
h : ¬IsUnit a
⊢ False
[PROOFSTEP]
exact ha.ne_zero rfl
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : Field K
a : K
h : a = 0
⊢ IsUnit (1 - a)
[PROOFSTEP]
rw [h, sub_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
K : Type u'
inst✝ : Field K
a : K
h : a = 0
⊢ IsUnit 1
[PROOFSTEP]
exact isUnit_one