[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : AddMonoid ι
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : ⨁ (i : ι), { x // x ∈ 𝒜 i }
i : ι
⊢ ↑(proj 𝒜 i) (↑(decompose 𝒜).symm a) = ↑(decompose 𝒜).symm (↑(of (fun i => (fun i => { x // x ∈ 𝒜 i }) i) i) (↑a i))
[PROOFSTEP]
rw [GradedRing.proj_apply, decompose_symm_of, Equiv.apply_symm_apply]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddLeftCancelMonoid ι
inst✝ : GradedRing 𝒜
a b : A
a_mem : a ∈ 𝒜 i
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) (i + j)) = a * ↑(↑(↑(decompose 𝒜) b) j)
[PROOFSTEP]
lift a to 𝒜 i using a_mem
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddLeftCancelMonoid ι
inst✝ : GradedRing 𝒜
b : A
a : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (↑a * b)) (i + j)) = ↑a * ↑(↑(↑(decompose 𝒜) b) j)
[PROOFSTEP]
rw [decompose_mul, decompose_coe, coe_of_mul_apply_add]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddRightCancelMonoid ι
inst✝ : GradedRing 𝒜
a b : A
b_mem : b ∈ 𝒜 j
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) (i + j)) = ↑(↑(↑(decompose 𝒜) a) i) * b
[PROOFSTEP]
lift b to 𝒜 j using b_mem
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddRightCancelMonoid ι
inst✝ : GradedRing 𝒜
a : A
b : { x // x ∈ 𝒜 j }
⊢ ↑(↑(↑(decompose 𝒜) (a * ↑b)) (i + j)) = ↑(↑(↑(decompose 𝒜) a) i) * ↑b
[PROOFSTEP]
rw [decompose_mul, decompose_coe, coe_mul_of_apply_add]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), { x // x ∈ 𝒜 i }
right_inv : AlgHom.comp (coeAlgHom 𝒜) decompose = AlgHom.id R A
left_inv : ∀ (i : ι) (x : { x // x ∈ 𝒜 i }), ↑decompose ↑x = ↑(of (fun i => { x // x ∈ 𝒜 i }) i) x
⊢ Function.RightInverse ↑(DirectSum.coeAddMonoidHom 𝒜) ↑decompose
[PROOFSTEP]
suffices decompose.comp (DirectSum.coeAlgHom 𝒜) = AlgHom.id _ _ from AlgHom.congr_fun this
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), { x // x ∈ 𝒜 i }
right_inv : AlgHom.comp (coeAlgHom 𝒜) decompose = AlgHom.id R A
left_inv : ∀ (i : ι) (x : { x // x ∈ 𝒜 i }), ↑decompose ↑x = ↑(of (fun i => { x // x ∈ 𝒜 i }) i) x
⊢ AlgHom.comp decompose (coeAlgHom 𝒜) = AlgHom.id R (⨁ (i : ι), { x // x ∈ 𝒜 i })
[PROOFSTEP]
refine DirectSum.algHom_ext' _ _ fun i => ?_
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), { x // x ∈ 𝒜 i }
right_inv : AlgHom.comp (coeAlgHom 𝒜) decompose = AlgHom.id R A
left_inv : ∀ (i : ι) (x : { x // x ∈ 𝒜 i }), ↑decompose ↑x = ↑(of (fun i => { x // x ∈ 𝒜 i }) i) x
i : ι
⊢ LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp decompose (coeAlgHom 𝒜))) (lof R ι (fun i => { x // x ∈ 𝒜 i }) i) =
    LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (⨁ (i : ι), { x // x ∈ 𝒜 i })))
      (lof R ι (fun i => { x // x ∈ 𝒜 i }) i)
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), { x // x ∈ 𝒜 i }
right_inv : AlgHom.comp (coeAlgHom 𝒜) decompose = AlgHom.id R A
left_inv : ∀ (i : ι) (x : { x // x ∈ 𝒜 i }), ↑decompose ↑x = ↑(of (fun i => { x // x ∈ 𝒜 i }) i) x
i : ι
x : { x // x ∈ 𝒜 i }
⊢ ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp decompose (coeAlgHom 𝒜))) (lof R ι (fun i => { x // x ∈ 𝒜 i }) i))
      x =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (⨁ (i : ι), { x // x ∈ 𝒜 i })))
          (lof R ι (fun i => { x // x ∈ 𝒜 i }) i))
      x
[PROOFSTEP]
exact (decompose.congr_arg <| DirectSum.coeAlgHom_of _ _ _).trans (left_inv i x)
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
a : ⨁ (i : ι), { x // x ∈ 𝒜 i }
i : ι
⊢ ↑(proj 𝒜 i) (↑(decompose 𝒜).symm a) = ↑(decompose 𝒜).symm (↑(of (fun i => (fun i => { x // x ∈ 𝒜 i }) i) i) (↑a i))
[PROOFSTEP]
rw [GradedAlgebra.proj_apply, decompose_symm_of, Equiv.apply_symm_apply]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ∀ (x y : A),
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (x * y) =
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } x *
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y
[PROOFSTEP]
refine' DirectSum.Decomposition.inductionOn 𝒜 (fun x => _) _ _
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : A
⊢ OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } (0 * x) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } 0 *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } x
[PROOFSTEP]
simp only [zero_mul, decompose_zero, zero_apply, ZeroMemClass.coe_zero]
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ∀ {i : ι} (m : { x // x ∈ 𝒜 i }) (y : A),
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (↑m * y) =
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } ↑m *
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y
[PROOFSTEP]
rintro i ⟨c, hc⟩
[GOAL]
case refine'_2.mk
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
⊢ ∀ (y : A),
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (↑{ val := c, property := hc } * y) =
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
          ↑{ val := c, property := hc } *
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y
[PROOFSTEP]
refine' DirectSum.Decomposition.inductionOn 𝒜 _ _ _
[GOAL]
case refine'_2.mk.refine'_1
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
⊢ OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
      (↑{ val := c, property := hc } * 0) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        ↑{ val := c, property := hc } *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } 0
[PROOFSTEP]
simp only [mul_zero, decompose_zero, zero_apply, ZeroMemClass.coe_zero]
[GOAL]
case refine'_2.mk.refine'_2
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
⊢ ∀ {i_1 : ι} (m : { x // x ∈ 𝒜 i_1 }),
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (↑{ val := c, property := hc } * ↑m) =
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
          ↑{ val := c, property := hc } *
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } ↑m
[PROOFSTEP]
rintro j ⟨c', hc'⟩
[GOAL]
case refine'_2.mk.refine'_2.mk
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
⊢ OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
      (↑{ val := c, property := hc } * ↑{ val := c', property := hc' }) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        ↑{ val := c, property := hc } *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        ↑{ val := c', property := hc' }
[PROOFSTEP]
simp only [Subtype.coe_mk]
[GOAL]
case refine'_2.mk.refine'_2.mk
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
⊢ ↑(↑(↑(decompose 𝒜) (c * c')) 0) = ↑(↑(↑(decompose 𝒜) c) 0) * ↑(↑(↑(decompose 𝒜) c') 0)
[PROOFSTEP]
by_cases h : i + j = 0
[GOAL]
case pos
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : i + j = 0
⊢ ↑(↑(↑(decompose 𝒜) (c * c')) 0) = ↑(↑(↑(decompose 𝒜) c) 0) * ↑(↑(↑(decompose 𝒜) c') 0)
[PROOFSTEP]
rw [decompose_of_mem_same 𝒜 (show c * c' ∈ 𝒜 0 from h ▸ SetLike.GradedMul.mul_mem hc hc'),
  decompose_of_mem_same 𝒜 (show c ∈ 𝒜 0 from (add_eq_zero_iff.mp h).1 ▸ hc),
  decompose_of_mem_same 𝒜 (show c' ∈ 𝒜 0 from (add_eq_zero_iff.mp h).2 ▸ hc')]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
⊢ ↑(↑(↑(decompose 𝒜) (c * c')) 0) = ↑(↑(↑(decompose 𝒜) c) 0) * ↑(↑(↑(decompose 𝒜) c') 0)
[PROOFSTEP]
rw [decompose_of_mem_ne 𝒜 (SetLike.GradedMul.mul_mem hc hc') h]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
⊢ 0 = ↑(↑(↑(decompose 𝒜) c) 0) * ↑(↑(↑(decompose 𝒜) c') 0)
[PROOFSTEP]
cases' show i ≠ 0 ∨ j ≠ 0 by rwa [add_eq_zero_iff, not_and_or] at h  with h' h'
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
⊢ i ≠ 0 ∨ j ≠ 0
[PROOFSTEP]
rwa [add_eq_zero_iff, not_and_or] at h
[GOAL]
case neg.inl
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
h' : i ≠ 0
⊢ 0 = ↑(↑(↑(decompose 𝒜) c) 0) * ↑(↑(↑(decompose 𝒜) c') 0)
[PROOFSTEP]
simp only [decompose_of_mem_ne 𝒜 hc h', zero_mul]
[GOAL]
case neg.inr
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
h' : j ≠ 0
⊢ 0 = ↑(↑(↑(decompose 𝒜) c) 0) * ↑(↑(↑(decompose 𝒜) c') 0)
[PROOFSTEP]
simp only [decompose_of_mem_ne 𝒜 hc' h', mul_zero]
[GOAL]
case refine'_2.mk.refine'_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
⊢ ∀ (m m' : A),
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
          (↑{ val := c, property := hc } * m) =
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
            ↑{ val := c, property := hc } *
          OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
            m →
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
            (↑{ val := c, property := hc } * m') =
          OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
              ↑{ val := c, property := hc } *
            OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
              m' →
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
            (↑{ val := c, property := hc } * (m + m')) =
          OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
              ↑{ val := c, property := hc } *
            OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
              (m + m')
[PROOFSTEP]
intro _ _ hd he
[GOAL]
case refine'_2.mk.refine'_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
m✝ m'✝ : A
hd :
  OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
      (↑{ val := c, property := hc } * m✝) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        ↑{ val := c, property := hc } *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } m✝
he :
  OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
      (↑{ val := c, property := hc } * m'✝) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        ↑{ val := c, property := hc } *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } m'✝
⊢ OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
      (↑{ val := c, property := hc } * (m✝ + m'✝)) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        ↑{ val := c, property := hc } *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (m✝ + m'✝)
[PROOFSTEP]
simp only at hd he
[GOAL]
case refine'_2.mk.refine'_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
m✝ m'✝ : A
hd : ↑(↑(↑(decompose 𝒜) (c * m✝)) 0) = ↑(↑(↑(decompose 𝒜) c) 0) * ↑(↑(↑(decompose 𝒜) m✝) 0)
he : ↑(↑(↑(decompose 𝒜) (c * m'✝)) 0) = ↑(↑(↑(decompose 𝒜) c) 0) * ↑(↑(↑(decompose 𝒜) m'✝) 0)
⊢ OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
      (↑{ val := c, property := hc } * (m✝ + m'✝)) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        ↑{ val := c, property := hc } *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (m✝ + m'✝)
[PROOFSTEP]
simp only [mul_add, decompose_add, add_apply, AddMemClass.coe_add, hd, he]
[GOAL]
case refine'_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ∀ (m m' : A),
    (∀ (y : A),
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
            (m * y) =
          OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
              m *
            OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
              y) →
      (∀ (y : A),
          OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
              (m' * y) =
            OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                m' *
              OneHom.toFun
                { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y) →
        ∀ (y : A),
          OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
              ((m + m') * y) =
            OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                (m + m') *
              OneHom.toFun
                { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y
[PROOFSTEP]
rintro _ _ ha hb _
[GOAL]
case refine'_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
m✝ m'✝ : A
ha :
  ∀ (y : A),
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (m✝ * y) =
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } m✝ *
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y
hb :
  ∀ (y : A),
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (m'✝ * y) =
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } m'✝ *
        OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y
y✝ : A
⊢ OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
      ((m✝ + m'✝) * y✝) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (m✝ + m'✝) *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y✝
[PROOFSTEP]
simp only at ha hb
[GOAL]
case refine'_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
m✝ m'✝ : A
ha : ∀ (y : A), ↑(↑(↑(decompose 𝒜) (m✝ * y)) 0) = ↑(↑(↑(decompose 𝒜) m✝) 0) * ↑(↑(↑(decompose 𝒜) y) 0)
hb : ∀ (y : A), ↑(↑(↑(decompose 𝒜) (m'✝ * y)) 0) = ↑(↑(↑(decompose 𝒜) m'✝) 0) * ↑(↑(↑(decompose 𝒜) y) 0)
y✝ : A
⊢ OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
      ((m✝ + m'✝) * y✝) =
    OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
        (m✝ + m'✝) *
      OneHom.toFun { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } y✝
[PROOFSTEP]
simp only [add_mul, decompose_add, add_apply, AddMemClass.coe_add, ha, hb]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) },
          map_mul' :=
            (_ :
              ∀ (m y : A),
                OneHom.toFun
                    { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                    (m * y) =
                  OneHom.toFun
                      { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } m *
                    OneHom.toFun
                      { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                      y) })
      0 =
    0
[PROOFSTEP]
simp only
  -- Porting note: added
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ↑(↑(↑(decompose 𝒜) 0) 0) = 0
[PROOFSTEP]
rw [decompose_zero]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ↑(↑0 0) = 0
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x✝¹ x✝ : A
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) },
          map_mul' :=
            (_ :
              ∀ (m y : A),
                OneHom.toFun
                    { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                    (m * y) =
                  OneHom.toFun
                      { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) } m *
                    OneHom.toFun
                      { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                      y) })
      (x✝¹ + x✝) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) },
            map_mul' :=
              (_ :
                ∀ (m y : A),
                  OneHom.toFun
                      { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                      (m * y) =
                    OneHom.toFun
                        { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                        m *
                      OneHom.toFun
                        { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                        y) })
        x✝¹ +
      OneHom.toFun
        (↑{ toOneHom := { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) },
            map_mul' :=
              (_ :
                ∀ (m y : A),
                  OneHom.toFun
                      { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                      (m * y) =
                    OneHom.toFun
                        { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                        m *
                      OneHom.toFun
                        { toFun := fun a => ↑(↑(↑(decompose 𝒜) a) 0), map_one' := (_ : ↑(↑(↑(decompose 𝒜) 1) 0) = 1) }
                        y) })
        x✝
[PROOFSTEP]
simp only
  -- Porting note: added
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x✝¹ x✝ : A
⊢ ↑(↑(↑(decompose 𝒜) (x✝¹ + x✝)) 0) = ↑(↑(↑(decompose 𝒜) x✝¹) 0) + ↑(↑(↑(decompose 𝒜) x✝) 0)
[PROOFSTEP]
rw [decompose_add]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x✝¹ x✝ : A
⊢ ↑(↑(↑(decompose 𝒜) x✝¹ + ↑(decompose 𝒜) x✝) 0) = ↑(↑(↑(decompose 𝒜) x✝¹) 0) + ↑(↑(↑(decompose 𝒜) x✝) 0)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a b : A
n i : ι
a_mem : a ∈ 𝒜 i
h : ¬i ≤ n
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) n) = 0
[PROOFSTEP]
lift a to 𝒜 i using a_mem
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
b : A
n i : ι
h : ¬i ≤ n
a : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (↑a * b)) n) = 0
[PROOFSTEP]
rwa [decompose_mul, decompose_coe, coe_of_mul_apply_of_not_le]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a b : A
n i : ι
b_mem : b ∈ 𝒜 i
h : ¬i ≤ n
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) n) = 0
[PROOFSTEP]
lift b to 𝒜 i using b_mem
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : CanonicallyOrderedAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : A
n i : ι
h : ¬i ≤ n
b : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (a * ↑b)) n) = 0
[PROOFSTEP]
rwa [decompose_mul, decompose_coe, coe_mul_of_apply_of_not_le]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁸ : Semiring A
inst✝⁷ : DecidableEq ι
inst✝⁶ : CanonicallyOrderedAddMonoid ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
a b : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a_mem : a ∈ 𝒜 i
h : i ≤ n
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) n) = a * ↑(↑(↑(decompose 𝒜) b) (n - i))
[PROOFSTEP]
lift a to 𝒜 i using a_mem
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁸ : Semiring A
inst✝⁷ : DecidableEq ι
inst✝⁶ : CanonicallyOrderedAddMonoid ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
b : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : i ≤ n
a : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (↑a * b)) n) = ↑a * ↑(↑(↑(decompose 𝒜) b) (n - i))
[PROOFSTEP]
rwa [decompose_mul, decompose_coe, coe_of_mul_apply_of_le]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁸ : Semiring A
inst✝⁷ : DecidableEq ι
inst✝⁶ : CanonicallyOrderedAddMonoid ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
a b : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b_mem : b ∈ 𝒜 i
h : i ≤ n
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) n) = ↑(↑(↑(decompose 𝒜) a) (n - i)) * b
[PROOFSTEP]
lift b to 𝒜 i using b_mem
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁸ : Semiring A
inst✝⁷ : DecidableEq ι
inst✝⁶ : CanonicallyOrderedAddMonoid ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
a : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : i ≤ n
b : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (a * ↑b)) n) = ↑(↑(↑(decompose 𝒜) a) (n - i)) * ↑b
[PROOFSTEP]
rwa [decompose_mul, decompose_coe, coe_mul_of_apply_of_le]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁹ : Semiring A
inst✝⁸ : DecidableEq ι
inst✝⁷ : CanonicallyOrderedAddMonoid ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a b : A
n✝ i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : ι
inst✝ : Decidable (i ≤ n)
a_mem : a ∈ 𝒜 i
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) n) = if i ≤ n then a * ↑(↑(↑(decompose 𝒜) b) (n - i)) else 0
[PROOFSTEP]
lift a to 𝒜 i using a_mem
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁹ : Semiring A
inst✝⁸ : DecidableEq ι
inst✝⁷ : CanonicallyOrderedAddMonoid ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
b : A
n✝ i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : ι
inst✝ : Decidable (i ≤ n)
a : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (↑a * b)) n) = if i ≤ n then ↑a * ↑(↑(↑(decompose 𝒜) b) (n - i)) else 0
[PROOFSTEP]
rw [decompose_mul, decompose_coe, coe_of_mul_apply]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁹ : Semiring A
inst✝⁸ : DecidableEq ι
inst✝⁷ : CanonicallyOrderedAddMonoid ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a b : A
n✝ i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : ι
inst✝ : Decidable (i ≤ n)
b_mem : b ∈ 𝒜 i
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) n) = if i ≤ n then ↑(↑(↑(decompose 𝒜) a) (n - i)) * b else 0
[PROOFSTEP]
lift b to 𝒜 i using b_mem
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁹ : Semiring A
inst✝⁸ : DecidableEq ι
inst✝⁷ : CanonicallyOrderedAddMonoid ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a : A
n✝ i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : ι
inst✝ : Decidable (i ≤ n)
b : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (a * ↑b)) n) = if i ≤ n then ↑(↑(↑(decompose 𝒜) a) (n - i)) * ↑b else 0
[PROOFSTEP]
rw [decompose_mul, decompose_coe, coe_mul_of_apply]


[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
n : ℕ
⊢ coeff (verschiebungFun x) n = if n = 0 then 0 else coeff x (n - 1)
[PROOFSTEP]
simp only [verschiebungFun, ge_iff_le]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
⊢ coeff (verschiebungFun x) 0 = 0
[PROOFSTEP]
rw [verschiebungFun_coeff, if_pos rfl]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
⊢ ↑(ghostComponent 0) (verschiebungFun x) = 0
[PROOFSTEP]
rw [ghostComponent_apply, aeval_wittPolynomial, Finset.range_one, Finset.sum_singleton, verschiebungFun_coeff_zero,
  pow_zero, pow_zero, pow_one, one_mul]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
n : ℕ
⊢ ↑(ghostComponent (n + 1)) (verschiebungFun x) = ↑p * ↑(ghostComponent n) x
[PROOFSTEP]
simp only [ghostComponent_apply, aeval_wittPolynomial]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
n : ℕ
⊢ (Finset.sum (Finset.range (n + 1 + 1)) fun i => ↑p ^ i * coeff (verschiebungFun x) i ^ p ^ (n + 1 - i)) =
    ↑p * Finset.sum (Finset.range (n + 1)) fun i => ↑p ^ i * coeff x i ^ p ^ (n - i)
[PROOFSTEP]
rw [Finset.sum_range_succ', verschiebungFun_coeff, if_pos rfl, zero_pow (pow_pos hp.1.pos _), mul_zero, add_zero,
  Finset.mul_sum, Finset.sum_congr rfl]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
n : ℕ
⊢ ∀ (x_1 : ℕ),
    x_1 ∈ Finset.range (n + 1) →
      ↑p ^ (x_1 + 1) * coeff (verschiebungFun x) (x_1 + 1) ^ p ^ (n + 1 - (x_1 + 1)) =
        ↑p * (↑p ^ x_1 * coeff x x_1 ^ p ^ (n - x_1))
[PROOFSTEP]
rintro i -
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
n i : ℕ
⊢ ↑p ^ (i + 1) * coeff (verschiebungFun x) (i + 1) ^ p ^ (n + 1 - (i + 1)) = ↑p * (↑p ^ i * coeff x i ^ p ^ (n - i))
[PROOFSTEP]
simp only [pow_succ, mul_assoc, verschiebungFun_coeff, if_neg (Nat.succ_ne_zero i), Nat.succ_sub_succ, tsub_zero]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
n : ℕ
⊢ ↑(aeval x.coeff) (verschiebungPoly n) = coeff (verschiebungFun x) n
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
⊢ ↑(aeval x.coeff) (verschiebungPoly Nat.zero) = coeff (verschiebungFun x) Nat.zero
[PROOFSTEP]
simp only [verschiebungPoly, Nat.zero_eq, ge_iff_le, tsub_eq_zero_of_le, ite_true, map_zero, verschiebungFun_coeff_zero]
[GOAL]
case succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : 𝕎 R
n : ℕ
⊢ ↑(aeval x.coeff) (verschiebungPoly (Nat.succ n)) = coeff (verschiebungFun x) (Nat.succ n)
[PROOFSTEP]
rw [verschiebungPoly, verschiebungFun_coeff_succ, if_neg n.succ_ne_zero, aeval_X, Nat.succ_eq_add_one,
  add_tsub_cancel_right]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ IsPoly p fun R _Rcr => verschiebungFun
[PROOFSTEP]
use verschiebungPoly
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ ⦃R : Type ?u.111740⦄ [inst : CommRing R] (x : 𝕎 R),
    (verschiebungFun x).coeff = fun n => ↑(aeval x.coeff) (verschiebungPoly n)
[PROOFSTEP]
simp only [aeval_verschiebung_poly', eq_self_iff_true, forall₃_true_iff]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ verschiebungFun 0 = 0
[PROOFSTEP]
ext ⟨⟩
[GOAL]
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ coeff (verschiebungFun 0) Nat.zero = coeff 0 Nat.zero
[PROOFSTEP]
rw [verschiebungFun_coeff]
[GOAL]
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ coeff (verschiebungFun 0) (Nat.succ n✝) = coeff 0 (Nat.succ n✝)
[PROOFSTEP]
rw [verschiebungFun_coeff]
[GOAL]
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ (if Nat.zero = 0 then 0 else coeff 0 (Nat.zero - 1)) = coeff 0 Nat.zero
[PROOFSTEP]
simp only [if_true, eq_self_iff_true, zero_coeff, ite_self]
[GOAL]
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ (if Nat.succ n✝ = 0 then 0 else coeff 0 (Nat.succ n✝ - 1)) = coeff 0 (Nat.succ n✝)
[PROOFSTEP]
simp only [if_true, eq_self_iff_true, zero_coeff, ite_self]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (x y : 𝕎 R),
    ZeroHom.toFun { toFun := verschiebungFun, map_zero' := (_ : verschiebungFun 0 = 0) } (x + y) =
      ZeroHom.toFun { toFun := verschiebungFun, map_zero' := (_ : verschiebungFun 0 = 0) } x +
        ZeroHom.toFun { toFun := verschiebungFun, map_zero' := (_ : verschiebungFun 0 = 0) } y
[PROOFSTEP]
dsimp
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (x y : 𝕎 R), verschiebungFun (x + y) = verschiebungFun x + verschiebungFun y
[PROOFSTEP]
ghost_calc _ _
[GOAL]
case refine_3
p : ℕ
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : CommRing S
R : Type u_1
R._inst : CommRing R
x✝ y✝ : 𝕎 R
⊢ ∀ (n : ℕ),
    ↑(ghostComponent n) (verschiebungFun (x✝ + y✝)) = ↑(ghostComponent n) (verschiebungFun x✝ + verschiebungFun y✝)
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case refine_3.zero
p : ℕ
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : CommRing S
R : Type u_1
R._inst : CommRing R
x✝ y✝ : 𝕎 R
⊢ ↑(ghostComponent Nat.zero) (verschiebungFun (x✝ + y✝)) =
    ↑(ghostComponent Nat.zero) (verschiebungFun x✝ + verschiebungFun y✝)
[PROOFSTEP]
ghost_simp
[GOAL]
case refine_3.succ
p : ℕ
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : CommRing S
R : Type u_1
R._inst : CommRing R
x✝ y✝ : 𝕎 R
n✝ : ℕ
⊢ ↑(ghostComponent (Nat.succ n✝)) (verschiebungFun (x✝ + y✝)) =
    ↑(ghostComponent (Nat.succ n✝)) (verschiebungFun x✝ + verschiebungFun y✝)
[PROOFSTEP]
ghost_simp
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x : 𝕎 R
⊢ ↑(map f) (↑verschiebung x) = ↑verschiebung (↑(map f) x)
[PROOFSTEP]
ext ⟨-, -⟩
[GOAL]
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x : 𝕎 R
⊢ coeff (↑(map f) (↑verschiebung x)) Nat.zero = coeff (↑verschiebung (↑(map f) x)) Nat.zero
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x : 𝕎 R
n✝ : ℕ
⊢ coeff (↑(map f) (↑verschiebung x)) (Nat.succ n✝) = coeff (↑verschiebung (↑(map f) x)) (Nat.succ n✝)
[PROOFSTEP]
exact f.map_zero
[GOAL]
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x : 𝕎 R
n✝ : ℕ
⊢ coeff (↑(map f) (↑verschiebung x)) (Nat.succ n✝) = coeff (↑verschiebung (↑(map f) x)) (Nat.succ n✝)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑(bind₁ verschiebungPoly) (wittPolynomial p ℤ n) = if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1)
[PROOFSTEP]
apply MvPolynomial.funext
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ∀ (x : ℕ → ℤ),
    ↑(MvPolynomial.eval x) (↑(bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
      ↑(MvPolynomial.eval x) (if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1))
[PROOFSTEP]
intro x
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
x : ℕ → ℤ
⊢ ↑(MvPolynomial.eval x) (↑(bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
    ↑(MvPolynomial.eval x) (if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1))
[PROOFSTEP]
split_ifs with hn
[GOAL]
case pos
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
x : ℕ → ℤ
hn : n = 0
⊢ ↑(MvPolynomial.eval x) (↑(bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
    ↑(MvPolynomial.eval x) (if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1))
[PROOFSTEP]
simp only [hn, wittPolynomial_zero, bind₁_X_right, verschiebungPoly_zero, map_zero, ite_true]
[GOAL]
case neg
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
x : ℕ → ℤ
hn : ¬n = 0
⊢ ↑(MvPolynomial.eval x) (↑(bind₁ verschiebungPoly) (wittPolynomial p ℤ n)) =
    ↑(MvPolynomial.eval x) (if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1))
[PROOFSTEP]
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn
[GOAL]
case neg.intro
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ ↑(MvPolynomial.eval x) (↑(bind₁ verschiebungPoly) (wittPolynomial p ℤ (Nat.succ n))) =
    ↑(MvPolynomial.eval x) (if Nat.succ n = 0 then 0 else ↑p * wittPolynomial p ℤ (Nat.succ n - 1))
[PROOFSTEP]
rw [Nat.succ_eq_add_one, add_tsub_cancel_right]
[GOAL]
case neg.intro
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ ↑(MvPolynomial.eval x) (↑(bind₁ verschiebungPoly) (wittPolynomial p ℤ (n + 1))) =
    ↑(MvPolynomial.eval x) (if n + 1 = 0 then 0 else ↑p * wittPolynomial p ℤ n)
[PROOFSTEP]
simp only [add_eq_zero, and_false, ite_false, map_mul]
[GOAL]
case neg.intro
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ ↑(MvPolynomial.eval x) (↑(bind₁ verschiebungPoly) (wittPolynomial p ℤ (n + 1))) =
    ↑(MvPolynomial.eval x) ↑p * ↑(MvPolynomial.eval x) (wittPolynomial p ℤ n)
[PROOFSTEP]
rw [map_natCast, hom_bind₁]
[GOAL]
case neg.intro
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ ↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (verschiebungPoly i))
      (wittPolynomial p ℤ (n + 1)) =
    ↑p * ↑(MvPolynomial.eval x) (wittPolynomial p ℤ n)
[PROOFSTEP]
calc
  _ = ghostComponent (n + 1) (verschiebung <| mk p x) :=
    by
    apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
    simp only [← aeval_verschiebungPoly, coeff_mk]
    funext k
    exact eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl
  _ = _ := by rw [ghostComponent_verschiebung]; rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ ↑(eval₂Hom (RingHom.comp (MvPolynomial.eval x) C) fun i => ↑(MvPolynomial.eval x) (verschiebungPoly i))
      (wittPolynomial p ℤ (n + 1)) =
    ↑(ghostComponent (n + 1)) (↑verschiebung (mk p x))
[PROOFSTEP]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ (fun i => ↑(MvPolynomial.eval x) (verschiebungPoly i)) = fun n => coeff (↑verschiebung (mk p x)) n
[PROOFSTEP]
simp only [← aeval_verschiebungPoly, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ (fun i => ↑(MvPolynomial.eval x) (verschiebungPoly i)) = fun n => ↑(aeval x) (verschiebungPoly n)
[PROOFSTEP]
funext k
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
k : ℕ
⊢ ↑(MvPolynomial.eval x) (verschiebungPoly k) = ↑(aeval x) (verschiebungPoly k)
[PROOFSTEP]
exact eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ ↑(ghostComponent (n + 1)) (↑verschiebung (mk p x)) = ↑p * ↑(MvPolynomial.eval x) (wittPolynomial p ℤ n)
[PROOFSTEP]
rw [ghostComponent_verschiebung]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ℕ → ℤ
n : ℕ
hn : ¬Nat.succ n = 0
⊢ ↑p * ↑(ghostComponent n) (mk p x) = ↑p * ↑(MvPolynomial.eval x) (wittPolynomial p ℤ n)
[PROOFSTEP]
rfl


[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
n : ℕ
⊢ wittPolynomial p R n = ∑ i in range (n + 1), ↑C (↑p ^ i) * X i ^ p ^ (n - i)
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range (n + 1) → ↑(monomial (single x (p ^ (n - x)))) (↑p ^ x) = ↑C (↑p ^ x) * X x ^ p ^ (n - x)
[PROOFSTEP]
rintro i -
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
n i : ℕ
⊢ ↑(monomial (single i (p ^ (n - i)))) (↑p ^ i) = ↑C (↑p ^ i) * X i ^ p ^ (n - i)
[PROOFSTEP]
rw [monomial_eq, Finsupp.prod_single_index]
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
n i : ℕ
⊢ X i ^ 0 = 1
[PROOFSTEP]
rw [pow_zero]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ ↑(map f) (W_ R n) = W_ S n
[PROOFSTEP]
rw [wittPolynomial, map_sum, wittPolynomial]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ ∑ x in range (n + 1), ↑(map f) (↑(monomial (single x (p ^ (n - x)))) (↑p ^ x)) =
    ∑ i in range (n + 1), ↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)
[PROOFSTEP]
refine sum_congr rfl fun i _ => ?_
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ ↑(map f) (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = ↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)
[PROOFSTEP]
rw [map_monomial, RingHom.map_pow, map_natCast]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑constantCoeff (W_ R n) = 0
[PROOFSTEP]
simp only [wittPolynomial, map_sum, constantCoeff_monomial]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ x in range (n + 1), if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0
[PROOFSTEP]
rw [sum_eq_zero]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range (n + 1) → (if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0
[PROOFSTEP]
rintro i _
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ (if single i (p ^ (n - i)) = 0 then ↑p ^ i else 0) = 0
[PROOFSTEP]
rw [if_neg]
[GOAL]
case hnc
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬single i (p ^ (n - i)) = 0
[PROOFSTEP]
rw [Finsupp.single_eq_zero]
[GOAL]
case hnc
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬p ^ (n - i) = 0
[PROOFSTEP]
exact ne_of_gt (pow_pos hp.1.pos _)
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
⊢ W_ R 0 = X 0
[PROOFSTEP]
simp only [wittPolynomial, X, sum_singleton, range_one, pow_zero, zero_add, tsub_self]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
⊢ W_ R 1 = ↑C ↑p * X 1 + X 0 ^ p
[PROOFSTEP]
simp only [wittPolynomial_eq_sum_C_mul_X_pow, sum_range_succ_comm, range_one, sum_singleton, one_mul, pow_one, C_1,
  pow_zero, tsub_self, tsub_zero]
[GOAL]
p : ℕ
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : DecidableEq R
S : Type u_2
inst✝² : CommRing S
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ℕ → A
n : ℕ
⊢ ↑(aeval f) (W_ R n) = ∑ i in range (n + 1), ↑p ^ i * f i ^ p ^ (n - i)
[PROOFSTEP]
simp [wittPolynomial, AlgHom.map_sum, aeval_monomial, Finsupp.prod_single_index]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
n : ℕ
⊢ W_ (ZMod (p ^ (n + 1))) (n + 1) = ↑(expand p) (W_ (ZMod (p ^ (n + 1))) n)
[PROOFSTEP]
simp only [wittPolynomial_eq_sum_C_mul_X_pow]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
n : ℕ
⊢ ∑ x in range (n + 1 + 1), ↑C (↑p ^ x) * X x ^ p ^ (n + 1 - x) =
    ↑(expand p) (∑ x in range (n + 1), ↑C (↑p ^ x) * X x ^ p ^ (n - x))
[PROOFSTEP]
rw [sum_range_succ, ← Nat.cast_pow, CharP.cast_eq_zero (ZMod (p ^ (n + 1))) (p ^ (n + 1)), C_0, zero_mul, add_zero,
  AlgHom.map_sum, sum_congr rfl]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range (n + 1) → ↑C (↑p ^ x) * X x ^ p ^ (n + 1 - x) = ↑(expand p) (↑C (↑p ^ x) * X x ^ p ^ (n - x))
[PROOFSTEP]
intro k hk
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
n k : ℕ
hk : k ∈ range (n + 1)
⊢ ↑C (↑p ^ k) * X k ^ p ^ (n + 1 - k) = ↑(expand p) (↑C (↑p ^ k) * X k ^ p ^ (n - k))
[PROOFSTEP]
rw [AlgHom.map_mul, AlgHom.map_pow, expand_X, algHom_C, ← pow_mul, ← pow_succ]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
n k : ℕ
hk : k ∈ range (n + 1)
⊢ ↑C (↑p ^ k) * X k ^ p ^ (n + 1 - k) = ↑C (↑p ^ k) * X k ^ p ^ (n - k + 1)
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a.e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
n k : ℕ
hk : k ∈ range (n + 1)
⊢ n + 1 - k = n - k + 1
[PROOFSTEP]
rw [mem_range] at hk
[GOAL]
case e_a.e_a.e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
n k : ℕ
hk : k < n + 1
⊢ n + 1 - k = n - k + 1
[PROOFSTEP]
rw [add_comm, add_tsub_assoc_of_le (Nat.lt_succ_iff.mp hk), ← add_comm]
[GOAL]
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
⊢ vars (W_ R n) = range (n + 1)
[PROOFSTEP]
have : ∀ i, (monomial (Finsupp.single i (p ^ (n - i))) ((p : R) ^ i)).vars = { i } :=
  by
  intro i
  refine' vars_monomial_single i (pow_ne_zero _ hp.1) _
  rw [← Nat.cast_pow, Nat.cast_ne_zero]
  exact pow_ne_zero i hp.1
[GOAL]
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
⊢ ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
[PROOFSTEP]
intro i
[GOAL]
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
[PROOFSTEP]
refine' vars_monomial_single i (pow_ne_zero _ hp.1) _
[GOAL]
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ ↑p ^ i ≠ 0
[PROOFSTEP]
rw [← Nat.cast_pow, Nat.cast_ne_zero]
[GOAL]
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n i : ℕ
⊢ p ^ i ≠ 0
[PROOFSTEP]
exact pow_ne_zero i hp.1
[GOAL]
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
⊢ vars (W_ R n) = range (n + 1)
[PROOFSTEP]
rw [wittPolynomial, vars_sum_of_disjoint]
[GOAL]
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
⊢ (Finset.biUnion (range (n + 1)) fun i => vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i))) = range (n + 1)
[PROOFSTEP]
simp only [this, biUnion_singleton_eq_self]
[GOAL]
case h
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
⊢ Pairwise (Disjoint on fun i => vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)))
[PROOFSTEP]
simp only [this]
[GOAL]
case h
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
⊢ Pairwise (Disjoint on fun i => {i})
[PROOFSTEP]
intro a b h
[GOAL]
case h
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
a b : ℕ
h : a ≠ b
⊢ (Disjoint on fun i => {i}) a b
[PROOFSTEP]
apply disjoint_singleton_left.mpr
[GOAL]
case h
p : ℕ
R : Type u_1
inst✝³ : CommRing R
inst✝² : DecidableEq R
S : Type u_2
inst✝¹ : CommRing S
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), vars (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = {i}
a b : ℕ
h : a ≠ b
⊢ ¬a ∈ (fun i => {i}) b
[PROOFSTEP]
rwa [mem_singleton]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
hp : NeZero p
n : ℕ
⊢ vars (W_ R n) ⊆ range (n + 1)
[PROOFSTEP]
rw [← map_wittPolynomial p (Int.castRingHom R), ← wittPolynomial_vars p ℤ]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
hp : NeZero p
n : ℕ
⊢ vars (↑(map (Int.castRingHom R)) (W_ ℤ n)) ⊆ vars (W_ ℤ n)
[PROOFSTEP]
apply vars_map
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
⊢ xInTermsOfW p R n = (X n - ∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * ↑C (⅟↑p ^ n)
[PROOFSTEP]
rw [xInTermsOfW, ← Fin.sum_univ_eq_sum_range]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
⊢ ↑constantCoeff (xInTermsOfW p R n) = 0
[PROOFSTEP]
apply Nat.strongInductionOn n
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
⊢ ∀ (n : ℕ), (∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0) → ↑constantCoeff (xInTermsOfW p R n) = 0
[PROOFSTEP]
clear n
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
⊢ ∀ (n : ℕ), (∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0) → ↑constantCoeff (xInTermsOfW p R n) = 0
[PROOFSTEP]
intro n IH
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
⊢ ↑constantCoeff (xInTermsOfW p R n) = 0
[PROOFSTEP]
rw [xInTermsOfW_eq, mul_comm, RingHom.map_mul, RingHom.map_sub, map_sum, constantCoeff_C, constantCoeff_X, zero_sub,
  mul_neg, neg_eq_zero]
  -- porting note: here, we should be able to do `rw [sum_eq_zero]`, but the goal that
    -- is created is not what we expect, and the sum is not replaced by zero...
    -- is it a bug in `rw` tactic?
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
⊢ ⅟↑p ^ n * ∑ x in range n, ↑constantCoeff (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = 0
[PROOFSTEP]
refine' Eq.trans (_ : _ = ((⅟↑p : R) ^ n) * 0) (mul_zero _)
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
⊢ ⅟↑p ^ n * ∑ x in range n, ↑constantCoeff (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = ⅟↑p ^ n * 0
[PROOFSTEP]
congr 1
[GOAL]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
⊢ ∑ x in range n, ↑constantCoeff (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = 0
[PROOFSTEP]
rw [sum_eq_zero]
[GOAL]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
⊢ ∀ (x : ℕ), x ∈ range n → ↑constantCoeff (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = 0
[PROOFSTEP]
intro m H
[GOAL]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m ∈ range n
⊢ ↑constantCoeff (↑C (↑p ^ m) * xInTermsOfW p R m ^ p ^ (n - m)) = 0
[PROOFSTEP]
rw [mem_range] at H
[GOAL]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m < n
⊢ ↑constantCoeff (↑C (↑p ^ m) * xInTermsOfW p R m ^ p ^ (n - m)) = 0
[PROOFSTEP]
simp only [RingHom.map_mul, RingHom.map_pow, map_natCast, IH m H]
[GOAL]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m < n
⊢ ↑p ^ m * 0 ^ p ^ (n - m) = 0
[PROOFSTEP]
rw [zero_pow, mul_zero]
[GOAL]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ (m : ℕ), m < n → ↑constantCoeff (xInTermsOfW p R m) = 0
m : ℕ
H : m < n
⊢ 0 < p ^ (n - m)
[PROOFSTEP]
apply pow_pos hp.1.pos
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
⊢ xInTermsOfW p R 0 = X 0
[PROOFSTEP]
rw [xInTermsOfW_eq, range_zero, sum_empty, pow_zero, C_1, mul_one, sub_zero]
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
[PROOFSTEP]
apply Nat.strongInductionOn n
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)) →
      n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
[PROOFSTEP]
clear n
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)) →
      n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
[PROOFSTEP]
intro n ih
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
[PROOFSTEP]
rw [xInTermsOfW_eq, mul_comm, vars_C_mul _ (nonzero_of_invertible _), vars_sub_of_disjoint, vars_X, range_succ,
  insert_eq]
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ n ∈ {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ∧
    {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ⊆ {n} ∪ range n
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Disjoint (vars (X n)) (vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)))
[PROOFSTEP]
on_goal 1 =>
  simp only [true_and_iff, true_or_iff, eq_self_iff_true, mem_union, mem_singleton]
  intro i
  rw [mem_union, mem_union]
  apply Or.imp id
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ n ∈ {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ∧
    {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ⊆ {n} ∪ range n
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Disjoint (vars (X n)) (vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)))
[PROOFSTEP]
on_goal 1 =>
  simp only [true_and_iff, true_or_iff, eq_self_iff_true, mem_union, mem_singleton]
  intro i
  rw [mem_union, mem_union]
  apply Or.imp id
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ n ∈ {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ∧
    {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ⊆ {n} ∪ range n
[PROOFSTEP]
simp only [true_and_iff, true_or_iff, eq_self_iff_true, mem_union, mem_singleton]
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ {n} ∪ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) ⊆ {n} ∪ range n
[PROOFSTEP]
intro i
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∪ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ {n} ∪ range n
[PROOFSTEP]
rw [mem_union, mem_union]
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∨ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ {n} ∨ i ∈ range n
[PROOFSTEP]
apply Or.imp id
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ range n
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Disjoint (vars (X n)) (vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)))
[PROOFSTEP]
on_goal 2 => rw [vars_X, disjoint_singleton_left]
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ range n
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Disjoint (vars (X n)) (vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)))
[PROOFSTEP]
on_goal 2 => rw [vars_X, disjoint_singleton_left]
[GOAL]
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Disjoint (vars (X n)) (vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)))
[PROOFSTEP]
rw [vars_X, disjoint_singleton_left]
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ range n
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ ¬n ∈ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
[PROOFSTEP]
all_goals
  intro H
  replace H := vars_sum_subset _ _ H
  rw [mem_biUnion] at H
  rcases H with ⟨j, hj, H⟩
  rw [vars_C_mul] at H
  swap
  · apply pow_ne_zero
    exact_mod_cast hp.1.ne_zero
  rw [mem_range] at hj
  replace H := (ih j hj).2 (vars_pow _ _ H)
  rw [mem_range] at H
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ range n
[PROOFSTEP]
intro H
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
H : i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x))
⊢ i ∈ range n
[PROOFSTEP]
replace H := vars_sum_subset _ _ H
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
H : i ∈ Finset.biUnion (range n) fun i => vars (↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ i ∈ range n
[PROOFSTEP]
rw [mem_biUnion] at H
[GOAL]
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
H : ∃ a, a ∈ range n ∧ i ∈ vars (↑C (↑p ^ a) * xInTermsOfW p ℚ a ^ p ^ (n - a))
⊢ i ∈ range n
[PROOFSTEP]
rcases H with ⟨j, hj, H⟩
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ i ∈ range n
[PROOFSTEP]
rw [vars_C_mul] at H
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ i ∈ range n
case intro.intro.ha
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ^ j ≠ 0
[PROOFSTEP]
swap
[GOAL]
case intro.intro.ha
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ^ j ≠ 0
[PROOFSTEP]
apply pow_ne_zero
[GOAL]
case intro.intro.ha.h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast hp.1.ne_zero
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ i ∈ range n
[PROOFSTEP]
rw [mem_range] at hj
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ i ∈ range n
[PROOFSTEP]
replace H := (ih j hj).2 (vars_pow _ _ H)
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i ∈ range (j + 1)
⊢ i ∈ range n
[PROOFSTEP]
rw [mem_range] at H
[GOAL]
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ ¬n ∈ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
[PROOFSTEP]
intro H
[GOAL]
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
H : n ∈ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ False
[PROOFSTEP]
replace H := vars_sum_subset _ _ H
[GOAL]
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
H : n ∈ Finset.biUnion (range n) fun i => vars (↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ False
[PROOFSTEP]
rw [mem_biUnion] at H
[GOAL]
case hpq
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
H : ∃ a, a ∈ range n ∧ n ∈ vars (↑C (↑p ^ a) * xInTermsOfW p ℚ a ^ p ^ (n - a))
⊢ False
[PROOFSTEP]
rcases H with ⟨j, hj, H⟩
[GOAL]
case hpq.intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False
[PROOFSTEP]
rw [vars_C_mul] at H
[GOAL]
case hpq.intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False
case hpq.intro.intro.ha
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ^ j ≠ 0
[PROOFSTEP]
swap
[GOAL]
case hpq.intro.intro.ha
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ^ j ≠ 0
[PROOFSTEP]
apply pow_ne_zero
[GOAL]
case hpq.intro.intro.ha.h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast hp.1.ne_zero
[GOAL]
case hpq.intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False
[PROOFSTEP]
rw [mem_range] at hj
[GOAL]
case hpq.intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False
[PROOFSTEP]
replace H := (ih j hj).2 (vars_pow _ _ H)
[GOAL]
case hpq.intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n ∈ range (j + 1)
⊢ False
[PROOFSTEP]
rw [mem_range] at H
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i < j + 1
⊢ i ∈ range n
[PROOFSTEP]
rw [mem_range]
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i < j + 1
⊢ i < n
[PROOFSTEP]
linarith
[GOAL]
case hpq.intro.intro
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n < j + 1
⊢ False
[PROOFSTEP]
linarith
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
⊢ xInTermsOfW p R n * ↑C (↑p ^ n) = X n - ∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)
[PROOFSTEP]
rw [xInTermsOfW_eq, mul_assoc, ← C_mul, ← mul_pow, invOf_mul_self, one_pow, C_1, mul_one]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
k : ℕ
⊢ ↑(bind₁ (xInTermsOfW p R)) (W_ R k) = X k
[PROOFSTEP]
rw [wittPolynomial_eq_sum_C_mul_X_pow, AlgHom.map_sum]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
k : ℕ
⊢ ∑ x in range (k + 1), ↑(bind₁ (xInTermsOfW p R)) (↑C (↑p ^ x) * X x ^ p ^ (k - x)) = X k
[PROOFSTEP]
simp only [Nat.cast_pow, AlgHom.map_pow, C_pow, AlgHom.map_mul, algHom_C]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
k : ℕ
⊢ ∑ x in range (k + 1), ↑C ↑p ^ x * ↑(bind₁ (xInTermsOfW p R)) (X x) ^ p ^ (k - x) = X k
[PROOFSTEP]
rw [sum_range_succ_comm, tsub_self, pow_zero, pow_one, bind₁_X_right, mul_comm, ← C_pow, xInTermsOfW_aux]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
k : ℕ
⊢ X k - ∑ i in range k, ↑C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (k - i) +
      ∑ x in range k, ↑C ↑p ^ x * ↑(bind₁ (xInTermsOfW p R)) (X x) ^ p ^ (k - x) =
    X k
[PROOFSTEP]
simp only [Nat.cast_pow, C_pow, bind₁_X_right, sub_add_cancel]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
⊢ ↑(bind₁ (W_ R)) (xInTermsOfW p R n) = X n
[PROOFSTEP]
apply Nat.strongInductionOn n
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
⊢ ∀ (n : ℕ), (∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m) → ↑(bind₁ (W_ R)) (xInTermsOfW p R n) = X n
[PROOFSTEP]
clear n
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
⊢ ∀ (n : ℕ), (∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m) → ↑(bind₁ (W_ R)) (xInTermsOfW p R n) = X n
[PROOFSTEP]
intro n H
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ ↑(bind₁ (W_ R)) (xInTermsOfW p R n) = X n
[PROOFSTEP]
rw [xInTermsOfW_eq, AlgHom.map_mul, AlgHom.map_sub, bind₁_X_right, algHom_C, AlgHom.map_sum,
  show X n = (X n * C ((p : R) ^ n)) * C ((⅟p : R) ^ n) by
    rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ X n = X n * ↑C (↑p ^ n) * ↑C (⅟↑p ^ n)
[PROOFSTEP]
rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]
[GOAL]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ (W_ R n - ∑ x in range n, ↑(bind₁ (W_ R)) (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))) * ↑C (⅟↑p ^ n) =
    X n * ↑C (↑p ^ n) * ↑C (⅟↑p ^ n)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ W_ R n - ∑ x in range n, ↑(bind₁ (W_ R)) (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = X n * ↑C (↑p ^ n)
[PROOFSTEP]
rw [wittPolynomial_eq_sum_C_mul_X_pow, sum_range_succ_comm, tsub_self, pow_zero, pow_one, mul_comm (X n), add_sub_assoc,
  add_right_eq_self, sub_eq_zero]
[GOAL]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ ∑ x in range n, ↑C (↑p ^ x) * X x ^ p ^ (n - x) =
    ∑ x in range n, ↑(bind₁ (W_ R)) (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ ∀ (x : ℕ),
    x ∈ range n → ↑C (↑p ^ x) * X x ^ p ^ (n - x) = ↑(bind₁ (W_ R)) (↑C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))
[PROOFSTEP]
intro i h
[GOAL]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
i : ℕ
h : i ∈ range n
⊢ ↑C (↑p ^ i) * X i ^ p ^ (n - i) = ↑(bind₁ (W_ R)) (↑C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i))
[PROOFSTEP]
rw [mem_range] at h
[GOAL]
case e_a
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ (m : ℕ), m < n → ↑(bind₁ (W_ R)) (xInTermsOfW p R m) = X m
i : ℕ
h : i < n
⊢ ↑C (↑p ^ i) * X i ^ p ^ (n - i) = ↑(bind₁ (W_ R)) (↑C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i))
[PROOFSTEP]
rw [AlgHom.map_mul, AlgHom.map_pow, algHom_C, H i h]