[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
⊢ ↑frobenius (↑verschiebung x) = x * ↑p
[PROOFSTEP]
simp only []
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
⊢ ↑frobenius (↑verschiebung x) = x * ↑p
[PROOFSTEP]
have : IsPoly p fun {R} [CommRing R] x ↦ frobenius (verschiebung x) :=
  IsPoly.comp (hg := frobenius_isPoly p) (hf := verschiebung_isPoly)
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
this : IsPoly p fun {R} [CommRing R] x => ↑frobenius (↑verschiebung x)
⊢ ↑frobenius (↑verschiebung x) = x * ↑p
[PROOFSTEP]
have : IsPoly p fun {R} [CommRing R] x ↦ x * p := mulN_isPoly p p
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
this✝ : IsPoly p fun {R} [CommRing R] x => ↑frobenius (↑verschiebung x)
this : IsPoly p fun {R} [CommRing R] x => x * ↑p
⊢ ↑frobenius (↑verschiebung x) = x * ↑p
[PROOFSTEP]
ghost_calc x
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
this✝ : IsPoly p fun {R} [CommRing R] x => ↑frobenius (↑verschiebung x)
this : IsPoly p fun {R} [CommRing R] x => x * ↑p
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
⊢ ∀ (n : ℕ), ↑(ghostComponent n) (↑frobenius (↑verschiebung x)) = ↑(ghostComponent n) (x * ↑p)
[PROOFSTEP]
ghost_simp [mul_comm]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 (ZMod p)
⊢ ↑verschiebung x = x * ↑p
[PROOFSTEP]
rw [← frobenius_verschiebung, frobenius_zmodp]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
⊢ coeff (↑p ^ i) i = 1
[PROOFSTEP]
induction' i with i h
[GOAL]
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
⊢ coeff (↑p ^ Nat.zero) Nat.zero = 1
[PROOFSTEP]
simp only [Nat.zero_eq, one_coeff_zero, Ne.def, pow_zero]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
h : coeff (↑p ^ i) i = 1
⊢ coeff (↑p ^ Nat.succ i) (Nat.succ i) = 1
[PROOFSTEP]
rw [pow_succ', ← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_succ, h, one_pow]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i j : ℕ
hj : j ≠ i
⊢ coeff (↑p ^ i) j = 0
[PROOFSTEP]
induction' i with i hi generalizing j
[GOAL]
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i j✝ : ℕ
hj✝ : j✝ ≠ i
j : ℕ
hj : j ≠ Nat.zero
⊢ coeff (↑p ^ Nat.zero) j = 0
[PROOFSTEP]
rw [Nat.zero_eq, pow_zero, one_coeff_eq_of_pos]
[GOAL]
case zero.hn
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i j✝ : ℕ
hj✝ : j✝ ≠ i
j : ℕ
hj : j ≠ Nat.zero
⊢ 0 < j
[PROOFSTEP]
exact Nat.pos_of_ne_zero hj
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i✝ j✝ : ℕ
hj✝ : j✝ ≠ i✝
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → coeff (↑p ^ i) j = 0
j : ℕ
hj : j ≠ Nat.succ i
⊢ coeff (↑p ^ Nat.succ i) j = 0
[PROOFSTEP]
rw [pow_succ', ← frobenius_verschiebung, coeff_frobenius_charP]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i✝ j✝ : ℕ
hj✝ : j✝ ≠ i✝
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → coeff (↑p ^ i) j = 0
j : ℕ
hj : j ≠ Nat.succ i
⊢ coeff (↑verschiebung (↑p ^ i)) j ^ p = 0
[PROOFSTEP]
cases j
[GOAL]
case succ.zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i✝ j : ℕ
hj✝ : j ≠ i✝
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → coeff (↑p ^ i) j = 0
hj : Nat.zero ≠ Nat.succ i
⊢ coeff (↑verschiebung (↑p ^ i)) Nat.zero ^ p = 0
[PROOFSTEP]
rw [verschiebung_coeff_zero, zero_pow]
[GOAL]
case succ.zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i✝ j : ℕ
hj✝ : j ≠ i✝
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → coeff (↑p ^ i) j = 0
hj : Nat.zero ≠ Nat.succ i
⊢ 0 < p
[PROOFSTEP]
exact Nat.Prime.pos hp.out
[GOAL]
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i✝ j : ℕ
hj✝ : j ≠ i✝
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → coeff (↑p ^ i) j = 0
n✝ : ℕ
hj : Nat.succ n✝ ≠ Nat.succ i
⊢ coeff (↑verschiebung (↑p ^ i)) (Nat.succ n✝) ^ p = 0
[PROOFSTEP]
rw [verschiebung_coeff_succ, hi, zero_pow]
[GOAL]
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i✝ j : ℕ
hj✝ : j ≠ i✝
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → coeff (↑p ^ i) j = 0
n✝ : ℕ
hj : Nat.succ n✝ ≠ Nat.succ i
⊢ 0 < p
[PROOFSTEP]
exact Nat.Prime.pos hp.out
[GOAL]
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i✝ j : ℕ
hj✝ : j ≠ i✝
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → coeff (↑p ^ i) j = 0
n✝ : ℕ
hj : Nat.succ n✝ ≠ Nat.succ i
⊢ n✝ ≠ i
[PROOFSTEP]
exact ne_of_apply_ne (fun j : ℕ => j.succ) hj
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
⊢ coeff (↑p) i = if i = 1 then 1 else 0
[PROOFSTEP]
split_ifs with hi
[GOAL]
case pos
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : i = 1
⊢ coeff (↑p) i = 1
[PROOFSTEP]
simpa only [hi, pow_one] using coeff_p_pow p R 1
[GOAL]
case neg
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : ¬i = 1
⊢ coeff (↑p) i = 0
[PROOFSTEP]
simpa only [pow_one] using coeff_p_pow_eq_zero p R hi
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
⊢ coeff (↑p) 0 = 0
[PROOFSTEP]
rw [coeff_p, if_neg]
[GOAL]
case hnc
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
⊢ ¬0 = 1
[PROOFSTEP]
exact zero_ne_one
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
⊢ coeff (↑p) 1 = 1
[PROOFSTEP]
rw [coeff_p, if_pos rfl]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : CharP R p
⊢ ↑p ≠ 0
[PROOFSTEP]
intro h
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : CharP R p
h : ↑p = 0
⊢ False
[PROOFSTEP]
simpa only [h, zero_coeff, zero_ne_one] using coeff_p_one p R
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : CharP R p
⊢ ↑p ≠ 0
[PROOFSTEP]
simpa using (IsFractionRing.injective (𝕎 R) (FractionRing (𝕎 R))).ne (WittVector.p_nonzero _ _)
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
⊢ ↑verschiebung (x * ↑frobenius y) = ↑verschiebung x * y
[PROOFSTEP]
simp only []
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
⊢ ↑verschiebung (x * ↑frobenius y) = ↑verschiebung x * y
[PROOFSTEP]
have : IsPoly₂ p fun {R} [Rcr : CommRing R] x y ↦ verschiebung (x * frobenius y) :=
  IsPoly.comp₂ (hg := verschiebung_isPoly) (hf :=
    IsPoly₂.comp (hh := mulIsPoly₂) (hf := idIsPolyI' p) (hg := frobenius_isPoly p))
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
this : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung (x * ↑frobenius y)
⊢ ↑verschiebung (x * ↑frobenius y) = ↑verschiebung x * y
[PROOFSTEP]
have : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung x * y :=
  IsPoly₂.comp (hh := mulIsPoly₂) (hf := verschiebung_isPoly) (hg := idIsPolyI' p)
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
this✝ : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung (x * ↑frobenius y)
this : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung x * y
⊢ ↑verschiebung (x * ↑frobenius y) = ↑verschiebung x * y
[PROOFSTEP]
ghost_calc x y
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
this✝ : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung (x * ↑frobenius y)
this : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung x * y
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
⊢ ∀ (n : ℕ), ↑(ghostComponent n) (↑verschiebung (x * ↑frobenius y)) = ↑(ghostComponent n) (↑verschiebung x * y)
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case refine_3.zero
p : ℕ
hp : Fact (Nat.Prime p)
this✝ : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung (x * ↑frobenius y)
this : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung x * y
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
⊢ ↑(ghostComponent Nat.zero) (↑verschiebung (x * ↑frobenius y)) = ↑(ghostComponent Nat.zero) (↑verschiebung x * y)
[PROOFSTEP]
ghost_simp [mul_assoc]
[GOAL]
case refine_3.succ
p : ℕ
hp : Fact (Nat.Prime p)
this✝ : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung (x * ↑frobenius y)
this : IsPoly₂ p fun {R} [CommRing R] x y => ↑verschiebung x * y
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
n✝ : ℕ
⊢ ↑(ghostComponent (Nat.succ n✝)) (↑verschiebung (x * ↑frobenius y)) =
    ↑(ghostComponent (Nat.succ n✝)) (↑verschiebung x * y)
[PROOFSTEP]
ghost_simp [mul_assoc]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ coeff (x * ↑p) 0 = 0
[PROOFSTEP]
rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_zero, zero_pow]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ 0 < p
[PROOFSTEP]
exact Nat.Prime.pos hp.out
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
i : ℕ
⊢ coeff (x * ↑p) (i + 1) = coeff x i ^ p
[PROOFSTEP]
rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_succ]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ ↑verschiebung (↑frobenius x) = x * ↑p
[PROOFSTEP]
ext ⟨i⟩
[GOAL]
case h.zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ coeff (↑verschiebung (↑frobenius x)) Nat.zero = coeff (x * ↑p) Nat.zero
[PROOFSTEP]
rw [mul_charP_coeff_zero, verschiebung_coeff_zero]
[GOAL]
case h.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n✝ : ℕ
⊢ coeff (↑verschiebung (↑frobenius x)) (Nat.succ n✝) = coeff (x * ↑p) (Nat.succ n✝)
[PROOFSTEP]
rw [mul_charP_coeff_succ, verschiebung_coeff_succ, coeff_frobenius_charP]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ ↑verschiebung (↑frobenius x) = ↑frobenius (↑verschiebung x)
[PROOFSTEP]
rw [verschiebung_frobenius, frobenius_verschiebung]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n k : ℕ
⊢ coeff ((↑verschiebung)^[n] x) (k + n) = coeff x k
[PROOFSTEP]
induction' n with k ih
[GOAL]
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
⊢ coeff ((↑verschiebung)^[Nat.zero] x) (k + Nat.zero) = coeff x k
[PROOFSTEP]
simp
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ k : ℕ
ih : coeff ((↑verschiebung)^[k] x) (k✝ + k) = coeff x k✝
⊢ coeff ((↑verschiebung)^[Nat.succ k] x) (k✝ + Nat.succ k) = coeff x k✝
[PROOFSTEP]
rw [iterate_succ_apply', Nat.add_succ, verschiebung_coeff_succ]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ k : ℕ
ih : coeff ((↑verschiebung)^[k] x) (k✝ + k) = coeff x k✝
⊢ coeff ((↑verschiebung)^[k] x) (k✝ + k) = coeff x k✝
[PROOFSTEP]
exact ih
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
i : ℕ
⊢ (↑verschiebung)^[i] x * y = (↑verschiebung)^[i] (x * (↑frobenius)^[i] y)
[PROOFSTEP]
induction' i with i ih generalizing y
[GOAL]
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y✝ y : 𝕎 R
⊢ (↑verschiebung)^[Nat.zero] x * y = (↑verschiebung)^[Nat.zero] (x * (↑frobenius)^[Nat.zero] y)
[PROOFSTEP]
simp
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y✝ : 𝕎 R
i : ℕ
ih : ∀ (y : 𝕎 R), (↑verschiebung)^[i] x * y = (↑verschiebung)^[i] (x * (↑frobenius)^[i] y)
y : 𝕎 R
⊢ (↑verschiebung)^[Nat.succ i] x * y = (↑verschiebung)^[Nat.succ i] (x * (↑frobenius)^[Nat.succ i] y)
[PROOFSTEP]
rw [iterate_succ_apply', ← verschiebung_mul_frobenius, ih, iterate_succ_apply']
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y✝ : 𝕎 R
i : ℕ
ih : ∀ (y : 𝕎 R), (↑verschiebung)^[i] x * y = (↑verschiebung)^[i] (x * (↑frobenius)^[i] y)
y : 𝕎 R
⊢ ↑verschiebung ((↑verschiebung)^[i] (x * (↑frobenius)^[i] (↑frobenius y))) =
    ↑verschiebung ((↑verschiebung)^[i] (x * (↑frobenius)^[Nat.succ i] y))
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (↑verschiebung)^[i] x * (↑verschiebung)^[j] y = (↑verschiebung)^[i + j] ((↑frobenius)^[j] x * (↑frobenius)^[i] y)
[PROOFSTEP]
calc
  _ = verschiebung^[i] (x * frobenius^[i] (verschiebung^[j] y)) := ?_
  _ = verschiebung^[i] (x * verschiebung^[j] (frobenius^[i] y)) := ?_
  _ = verschiebung^[i] (verschiebung^[j] (frobenius^[i] y) * x) := ?_
  _ = verschiebung^[i] (verschiebung^[j] (frobenius^[i] y * frobenius^[j] x)) := ?_
  _ = verschiebung^[i + j] (frobenius^[i] y * frobenius^[j] x) := ?_
  _ = _ := ?_
[GOAL]
case calc_1
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (↑verschiebung)^[i] x * (↑verschiebung)^[j] y = (↑verschiebung)^[i] (x * (↑frobenius)^[i] ((↑verschiebung)^[j] y))
[PROOFSTEP]
apply iterate_verschiebung_mul_left
[GOAL]
case calc_2
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (↑verschiebung)^[i] (x * (↑frobenius)^[i] ((↑verschiebung)^[j] y)) =
    (↑verschiebung)^[i] (x * (↑verschiebung)^[j] ((↑frobenius)^[i] y))
[PROOFSTEP]
rw [verschiebung_frobenius_comm.iterate_iterate]
[GOAL]
case calc_3
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (↑verschiebung)^[i] (x * (↑verschiebung)^[j] ((↑frobenius)^[i] y)) =
    (↑verschiebung)^[i] ((↑verschiebung)^[j] ((↑frobenius)^[i] y) * x)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case calc_4
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (↑verschiebung)^[i] ((↑verschiebung)^[j] ((↑frobenius)^[i] y) * x) =
    (↑verschiebung)^[i] ((↑verschiebung)^[j] ((↑frobenius)^[i] y * (↑frobenius)^[j] x))
[PROOFSTEP]
rw [iterate_verschiebung_mul_left]
[GOAL]
case calc_5
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (↑verschiebung)^[i] ((↑verschiebung)^[j] ((↑frobenius)^[i] y * (↑frobenius)^[j] x)) =
    (↑verschiebung)^[i + j] ((↑frobenius)^[i] y * (↑frobenius)^[j] x)
[PROOFSTEP]
rw [iterate_add_apply]
[GOAL]
case calc_6
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ (↑verschiebung)^[i + j] ((↑frobenius)^[i] y * (↑frobenius)^[j] x) =
    (↑verschiebung)^[i + j] ((↑frobenius)^[j] x * (↑frobenius)^[i] y)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
i k : ℕ
⊢ coeff ((↑frobenius)^[i] x) k = coeff x k ^ p ^ i
[PROOFSTEP]
induction' i with i ih
[GOAL]
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k : ℕ
⊢ coeff ((↑frobenius)^[Nat.zero] x) k = coeff x k ^ p ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k i : ℕ
ih : coeff ((↑frobenius)^[i] x) k = coeff x k ^ p ^ i
⊢ coeff ((↑frobenius)^[Nat.succ i] x) k = coeff x k ^ p ^ Nat.succ i
[PROOFSTEP]
rw [iterate_succ_apply', coeff_frobenius_charP, ih, Nat.pow_succ]
[GOAL]
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
k i : ℕ
ih : coeff ((↑frobenius)^[i] x) k = coeff x k ^ p ^ i
⊢ (coeff x k ^ p ^ i) ^ p = coeff x k ^ (p ^ i * p)
[PROOFSTEP]
ring_nf
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ coeff ((↑verschiebung)^[i] x * (↑verschiebung)^[j] y) (i + j) = coeff x 0 ^ p ^ j * coeff y 0 ^ p ^ i
[PROOFSTEP]
calc
  _ = (verschiebung^[i + j] (frobenius^[j] x * frobenius^[i] y)).coeff (i + j) := ?_
  _ = (frobenius^[j] x * frobenius^[i] y).coeff 0 := ?_
  _ = (frobenius^[j] x).coeff 0 * (frobenius^[i] y).coeff 0 := ?_
  _ = _ := ?_
[GOAL]
case calc_1
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ coeff ((↑verschiebung)^[i] x * (↑verschiebung)^[j] y) (i + j) =
    coeff ((↑verschiebung)^[i + j] ((↑frobenius)^[j] x * (↑frobenius)^[i] y)) (i + j)
[PROOFSTEP]
rw [iterate_verschiebung_mul]
[GOAL]
case calc_2
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ coeff ((↑verschiebung)^[i + j] ((↑frobenius)^[j] x * (↑frobenius)^[i] y)) (i + j) =
    coeff ((↑frobenius)^[j] x * (↑frobenius)^[i] y) 0
[PROOFSTEP]
convert iterate_verschiebung_coeff (p := p) (R := R) _ _ _ using 2
[GOAL]
case h.e'_2.h.e'_4
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ i + j = 0 + (i + j)
[PROOFSTEP]
rw [zero_add]
[GOAL]
case calc_3
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ coeff ((↑frobenius)^[j] x * (↑frobenius)^[i] y) 0 = coeff ((↑frobenius)^[j] x) 0 * coeff ((↑frobenius)^[i] y) 0
[PROOFSTEP]
apply mul_coeff_zero
[GOAL]
case calc_4
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ coeff ((↑frobenius)^[j] x) 0 * coeff ((↑frobenius)^[i] y) 0 = coeff x 0 ^ p ^ j * coeff y 0 ^ p ^ i
[PROOFSTEP]
simp only [iterate_frobenius_coeff]


[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : SetLike S R
inst✝ : NonUnitalSubsemiringClass S R
s : S
⊢ ∀ (x y : { x // x ∈ s }), ↑(x + y) = ↑x + ↑y
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u
S : Type v
T : Type w
inst✝⁵ : NonUnitalNonAssocSemiring R✝
M : Subsemigroup R✝
inst✝⁴ : SetLike S R✝
inst✝³ : NonUnitalSubsemiringClass S R✝
s : S
R : Type ?u.22770
inst✝² : NonUnitalSemiring R
inst✝¹ : SetLike S R
inst✝ : NonUnitalSubsemiringClass S R
⊢ ∀ (x y : { x // x ∈ s }), ↑(x + y) = ↑x + ↑y
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u
S : Type v
T : Type w
inst✝⁵ : NonUnitalNonAssocSemiring R✝
M : Subsemigroup R✝
inst✝⁴ : SetLike S R✝
inst✝³ : NonUnitalSubsemiringClass S R✝
s : S
R : Type ?u.28609
inst✝² : NonUnitalCommSemiring R
inst✝¹ : SetLike S R
inst✝ : NonUnitalSubsemiringClass S R
⊢ ∀ (x y : { x // x ∈ s }), ↑(x + y) = ↑x + ↑y
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
p q : NonUnitalSubsemiring R
h : (fun s => s.carrier) p = (fun s => s.carrier) q
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
q : NonUnitalSubsemiring R
toAddSubmonoid✝ : AddSubmonoid R
mul_mem'✝ : ∀ {a b : R}, a ∈ toAddSubmonoid✝.carrier → b ∈ toAddSubmonoid✝.carrier → a * b ∈ toAddSubmonoid✝.carrier
h : (fun s => s.carrier) { toAddSubmonoid := toAddSubmonoid✝, mul_mem' := mul_mem'✝ } = (fun s => s.carrier) q
⊢ { toAddSubmonoid := toAddSubmonoid✝, mul_mem' := mul_mem'✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
toAddSubmonoid✝¹ : AddSubmonoid R
mul_mem'✝¹ : ∀ {a b : R}, a ∈ toAddSubmonoid✝¹.carrier → b ∈ toAddSubmonoid✝¹.carrier → a * b ∈ toAddSubmonoid✝¹.carrier
toAddSubmonoid✝ : AddSubmonoid R
mul_mem'✝ : ∀ {a b : R}, a ∈ toAddSubmonoid✝.carrier → b ∈ toAddSubmonoid✝.carrier → a * b ∈ toAddSubmonoid✝.carrier
h :
  (fun s => s.carrier) { toAddSubmonoid := toAddSubmonoid✝¹, mul_mem' := mul_mem'✝¹ } =
    (fun s => s.carrier) { toAddSubmonoid := toAddSubmonoid✝, mul_mem' := mul_mem'✝ }
⊢ { toAddSubmonoid := toAddSubmonoid✝¹, mul_mem' := mul_mem'✝¹ } =
    { toAddSubmonoid := toAddSubmonoid✝, mul_mem' := mul_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toAddSubmonoid
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
toAddSubmonoid✝¹ : AddSubmonoid R
mul_mem'✝¹ : ∀ {a b : R}, a ∈ toAddSubmonoid✝¹.carrier → b ∈ toAddSubmonoid✝¹.carrier → a * b ∈ toAddSubmonoid✝¹.carrier
toAddSubmonoid✝ : AddSubmonoid R
mul_mem'✝ : ∀ {a b : R}, a ∈ toAddSubmonoid✝.carrier → b ∈ toAddSubmonoid✝.carrier → a * b ∈ toAddSubmonoid✝.carrier
h :
  (fun s => s.carrier) { toAddSubmonoid := toAddSubmonoid✝¹, mul_mem' := mul_mem'✝¹ } =
    (fun s => s.carrier) { toAddSubmonoid := toAddSubmonoid✝, mul_mem' := mul_mem'✝ }
⊢ toAddSubmonoid✝¹ = toAddSubmonoid✝
[PROOFSTEP]
exact SetLike.coe_injective' h
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
s : Set R
sg : Subsemigroup R
hg : ↑sg = s
sa : AddSubmonoid R
ha : ↑sa = s
⊢ ∀ {a b : R}, a ∈ s → b ∈ s → a + b ∈ s
[PROOFSTEP]
subst ha
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
sg : Subsemigroup R
sa : AddSubmonoid R
hg : ↑sg = ↑sa
⊢ ∀ {a b : R}, a ∈ ↑sa → b ∈ ↑sa → a + b ∈ ↑sa
[PROOFSTEP]
exact sa.add_mem
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
s : Set R
sg : Subsemigroup R
hg : ↑sg = s
sa : AddSubmonoid R
ha : ↑sa = s
⊢ 0 ∈ { carrier := s, add_mem' := (_ : ∀ {a b : R}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier
[PROOFSTEP]
subst ha
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
sg : Subsemigroup R
sa : AddSubmonoid R
hg : ↑sg = ↑sa
⊢ 0 ∈ { carrier := ↑sa, add_mem' := (_ : ∀ {a b : R}, a ∈ ↑sa → b ∈ ↑sa → a + b ∈ ↑sa) }.carrier
[PROOFSTEP]
exact sa.zero_mem
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
s : Set R
sg : Subsemigroup R
hg : ↑sg = s
sa : AddSubmonoid R
ha : ↑sa = s
⊢ ∀ {a b : R},
    a ∈
        { toAddSubsemigroup := { carrier := s, add_mem' := (_ : ∀ {a b : R}, a ∈ s → b ∈ s → a + b ∈ s) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := s,
                        add_mem' :=
                          (_ : ∀ {a b : R}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier) }.toAddSubsemigroup.carrier →
      b ∈
          { toAddSubsemigroup := { carrier := s, add_mem' := (_ : ∀ {a b : R}, a ∈ s → b ∈ s → a + b ∈ s) },
                zero_mem' :=
                  (_ :
                    0 ∈
                      { carrier := s,
                          add_mem' :=
                            (_ : ∀ {a b : R}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier) }.toAddSubsemigroup.carrier →
        a * b ∈
          { toAddSubsemigroup := { carrier := s, add_mem' := (_ : ∀ {a b : R}, a ∈ s → b ∈ s → a + b ∈ s) },
                zero_mem' :=
                  (_ :
                    0 ∈
                      { carrier := s,
                          add_mem' :=
                            (_ : ∀ {a b : R}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
subst hg
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
sg : Subsemigroup R
sa : AddSubmonoid R
ha : ↑sa = ↑sg
⊢ ∀ {a b : R},
    a ∈
        { toAddSubsemigroup := { carrier := ↑sg, add_mem' := (_ : ∀ {a b : R}, a ∈ ↑sg → b ∈ ↑sg → a + b ∈ ↑sg) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := ↑sg,
                        add_mem' :=
                          (_ : ∀ {a b : R}, a ∈ ↑sg → b ∈ ↑sg → a + b ∈ ↑sg) }.carrier) }.toAddSubsemigroup.carrier →
      b ∈
          { toAddSubsemigroup := { carrier := ↑sg, add_mem' := (_ : ∀ {a b : R}, a ∈ ↑sg → b ∈ ↑sg → a + b ∈ ↑sg) },
                zero_mem' :=
                  (_ :
                    0 ∈
                      { carrier := ↑sg,
                          add_mem' :=
                            (_ : ∀ {a b : R}, a ∈ ↑sg → b ∈ ↑sg → a + b ∈ ↑sg) }.carrier) }.toAddSubsemigroup.carrier →
        a * b ∈
          { toAddSubsemigroup := { carrier := ↑sg, add_mem' := (_ : ∀ {a b : R}, a ∈ ↑sg → b ∈ ↑sg → a + b ∈ ↑sg) },
                zero_mem' :=
                  (_ :
                    0 ∈
                      { carrier := ↑sg,
                          add_mem' :=
                            (_ : ∀ {a b : R}, a ∈ ↑sg → b ∈ ↑sg → a + b ∈ ↑sg) }.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
exact sg.mul_mem
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝⁴ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝³ : NonUnitalNonAssocSemiring S
inst✝² : NonUnitalNonAssocSemiring T
F : Type u_1
G : Type u_2
inst✝¹ : NonUnitalRingHomClass F R S
inst✝ : NonUnitalRingHomClass G S T
s✝ : NonUnitalSubsemiring R
f : F
s : NonUnitalSubsemiring R
y : S
⊢ y ∈ map f s ↔ ∃ x, x ∈ s ∧ ↑f x = y
[PROOFSTEP]
convert Set.mem_image_iff_bex
[GOAL]
case h.e'_2.h.e'_2.h.a
R : Type u
S : Type v
T : Type w
inst✝⁴ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝³ : NonUnitalNonAssocSemiring S
inst✝² : NonUnitalNonAssocSemiring T
F : Type u_1
G : Type u_2
inst✝¹ : NonUnitalRingHomClass F R S
inst✝ : NonUnitalRingHomClass G S T
s✝ : NonUnitalSubsemiring R
f : F
s : NonUnitalSubsemiring R
y : S
x✝ : R
⊢ x✝ ∈ s ∧ ↑f x✝ = y ↔ ∃ x, ↑f x✝ = y
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝⁴ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝³ : NonUnitalNonAssocSemiring S
inst✝² : NonUnitalNonAssocSemiring T
F : Type u_1
G : Type u_2
inst✝¹ : NonUnitalRingHomClass F R S
inst✝ : NonUnitalRingHomClass G S T
f : F
g : G
⊢ srange f = map f ⊤
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S : Type v
T : Type w
inst✝⁴ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝³ : NonUnitalNonAssocSemiring S
inst✝² : NonUnitalNonAssocSemiring T
F : Type u_1
G : Type u_2
inst✝¹ : NonUnitalRingHomClass F R S
inst✝ : NonUnitalRingHomClass G S T
f : F
g : G
x✝ : S
⊢ x✝ ∈ srange f ↔ x✝ ∈ map f ⊤
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝⁴ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝³ : NonUnitalNonAssocSemiring S
inst✝² : NonUnitalNonAssocSemiring T
F : Type u_1
G : Type u_2
inst✝¹ : NonUnitalRingHomClass F R S
inst✝ : NonUnitalRingHomClass G S T
f✝ : F
g✝ : G
g : S →ₙ+* T
f : R →ₙ+* S
⊢ map g (srange f) = srange (comp g f)
[PROOFSTEP]
simpa only [srange_eq_map] using (⊤ : NonUnitalSubsemiring R).map_map g f
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
a✝ b✝ : R
x✝¹ : a✝ ∈ {0}
x✝ : b✝ ∈ {0}
⊢ a✝ + b✝ ∈ {0}
[PROOFSTEP]
simp_all
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
a✝ b✝ : R
x✝¹ :
  a✝ ∈
    { toAddSubsemigroup := { carrier := {0}, add_mem' := (_ : ∀ {a b : R}, a ∈ {0} → b ∈ {0} → a + b ∈ {0}) },
          zero_mem' := (_ : 0 ∈ {0}) }.toAddSubsemigroup.carrier
x✝ :
  b✝ ∈
    { toAddSubsemigroup := { carrier := {0}, add_mem' := (_ : ∀ {a b : R}, a ∈ {0} → b ∈ {0} → a + b ∈ {0}) },
          zero_mem' := (_ : 0 ∈ {0}) }.toAddSubsemigroup.carrier
⊢ a✝ * b✝ ∈
    { toAddSubsemigroup := { carrier := {0}, add_mem' := (_ : ∀ {a b : R}, a ∈ {0} → b ∈ {0} → a + b ∈ {0}) },
          zero_mem' := (_ : 0 ∈ {0}) }.toAddSubsemigroup.carrier
[PROOFSTEP]
simp_all
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
s : Set (NonUnitalSubsemiring R)
⊢ ↑(⨅ (t : NonUnitalSubsemiring R) (_ : t ∈ s), toSubsemigroup t) = ⋂ (t : NonUnitalSubsemiring R) (_ : t ∈ s), ↑t
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
s : Set (NonUnitalSubsemiring R)
⊢ ↑(⨅ (t : NonUnitalSubsemiring R) (_ : t ∈ s), t.toAddSubmonoid) = ⋂ (t : NonUnitalSubsemiring R) (_ : t ∈ s), ↑t
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
f : R ≃+* S
K : NonUnitalSubsemiring R
x : S
⊢ x ∈ map (↑f) K ↔ ↑(RingEquiv.symm f) x ∈ K
[PROOFSTEP]
convert @Set.mem_image_equiv _ _ (↑K) f.toEquiv x
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
⊢ nonUnitalSubsemiringClosure M = NonUnitalSubsemiring.closure ↑M
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
x✝ : R
⊢ x✝ ∈ nonUnitalSubsemiringClosure M ↔ x✝ ∈ NonUnitalSubsemiring.closure ↑M
[PROOFSTEP]
refine ⟨fun hx => ?_, fun hx => (NonUnitalSubsemiring.mem_closure.mp hx) M.nonUnitalSubsemiringClosure fun s sM => ?_⟩
[GOAL]
case h.refine_1
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
x✝ : R
hx : x✝ ∈ nonUnitalSubsemiringClosure M
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M
[PROOFSTEP]
rintro - ⟨H1, rfl⟩
[GOAL]
case h.refine_2
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
⊢ s ∈ ↑(nonUnitalSubsemiringClosure M)
[PROOFSTEP]
rintro - ⟨H1, rfl⟩
[GOAL]
case h.refine_1.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
x✝ : R
hx : x✝ ∈ nonUnitalSubsemiringClosure M
H1 : NonUnitalSubsemiring R
⊢ x✝ ∈ (fun t => ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1
[PROOFSTEP]
rintro - ⟨H2, rfl⟩
[GOAL]
case h.refine_2.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
⊢ s ∈ (fun t => ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1
[PROOFSTEP]
rintro - ⟨H2, rfl⟩
[GOAL]
case h.refine_1.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
x✝ : R
hx : x✝ ∈ nonUnitalSubsemiringClosure M
H1 : NonUnitalSubsemiring R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ x✝ ∈ (fun h => ↑H1) H2
[PROOFSTEP]
exact AddSubmonoid.mem_closure.mp hx H1.toAddSubmonoid H2
[GOAL]
case h.refine_2.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ s ∈ (fun h => ↑H1) H2
[PROOFSTEP]
exact H2 sM
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
s : Set R
⊢ ↑(closure s) = ↑(AddSubmonoid.closure ↑(Subsemigroup.closure s))
[PROOFSTEP]
simp [← Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid, Subsemigroup.nonUnitalSubsemiringClosure_eq_closure]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
s : Set R
⊢ closure ↑(AddSubmonoid.closure s) = closure s
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
s : Set R
x : R
⊢ x ∈ closure ↑(AddSubmonoid.closure s) ↔ x ∈ closure s
[PROOFSTEP]
refine' ⟨fun hx => _, fun hx => closure_mono AddSubmonoid.subset_closure hx⟩
[GOAL]
case h
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
⊢ x ∈ closure s
[PROOFSTEP]
rintro - ⟨H, rfl⟩
[GOAL]
case h.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : NonUnitalSubsemiring R
⊢ x ∈ (fun t => ⋂ (_ : t ∈ {S | s ⊆ ↑S}), ↑t) H
[PROOFSTEP]
rintro - ⟨J, rfl⟩
[GOAL]
case h.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : NonUnitalSubsemiring R
J : H ∈ {S | s ⊆ ↑S}
⊢ x ∈ (fun h => ↑H) J
[PROOFSTEP]
refine' (AddSubmonoid.mem_closure.mp (mem_closure_iff.mp hx)) H.toAddSubmonoid fun y hy => _
[GOAL]
case h.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : NonUnitalSubsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Subsemigroup.closure ↑(AddSubmonoid.closure s))
⊢ y ∈ ↑H.toAddSubmonoid
[PROOFSTEP]
refine' (Subsemigroup.mem_closure.mp hy) H.toSubsemigroup fun z hz => _
[GOAL]
case h.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : NonUnitalSubsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Subsemigroup.closure ↑(AddSubmonoid.closure s))
z : R
hz : z ∈ ↑(AddSubmonoid.closure s)
⊢ z ∈ ↑(toSubsemigroup H)
[PROOFSTEP]
exact (AddSubmonoid.mem_closure.mp hz) H.toAddSubmonoid fun w hw => J hw
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type u_1
inst✝ : NonUnitalRingHomClass F R S
s : NonUnitalSubsemiring R
x : R × S
⊢ x ∈ prod s ⊤ ↔ x ∈ comap (NonUnitalRingHom.fst R S) s
[PROOFSTEP]
simp [mem_prod, MonoidHom.coe_fst]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type u_1
inst✝ : NonUnitalRingHomClass F R S
s : NonUnitalSubsemiring S
x : R × S
⊢ x ∈ prod ⊤ s ↔ x ∈ comap (NonUnitalRingHom.snd R S) s
[PROOFSTEP]
simp [mem_prod, MonoidHom.coe_snd]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type u_1
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ⨆ (i : ι), S i ↔ ∃ i, x ∈ S i
[PROOFSTEP]
refine' ⟨_, fun ⟨i, hi⟩ => (SetLike.le_def.1 <| le_iSup S i) hi⟩
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type u_1
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
let U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ i, (S i : Set R)) (⨆ i, (S i).toSubsemigroup)
    (Subsemigroup.coe_iSup_of_directed <| hS.mono_comp _ fun _ _ => id) (⨆ i, (S i).toAddSubmonoid)
    (AddSubmonoid.coe_iSup_of_directed <| hS.mono_comp _ fun _ _ => id)
      -- Porting note `@this` doesn't work
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type u_1
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i))) (⨆ (i : ι), (S i).toAddSubmonoid)
    (_ : ↑(⨆ (i : ι), (S i).toAddSubmonoid) = ⋃ (i : ι), ↑(S i).toAddSubmonoid)
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
[PROOFSTEP]
suffices H : ⨆ i, S i ≤ U
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type u_1
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i))) (⨆ (i : ι), (S i).toAddSubmonoid)
    (_ : ↑(⨆ (i : ι), (S i).toAddSubmonoid) = ⋃ (i : ι), ↑(S i).toAddSubmonoid)
H : ⨆ (i : ι), S i ≤ U
⊢ x ∈ ⨆ (i : ι), S i → ∃ i, x ∈ S i
case H
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type u_1
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i))) (⨆ (i : ι), (S i).toAddSubmonoid)
    (_ : ↑(⨆ (i : ι), (S i).toAddSubmonoid) = ⋃ (i : ι), ↑(S i).toAddSubmonoid)
⊢ ⨆ (i : ι), S i ≤ U
[PROOFSTEP]
simpa using @H x
[GOAL]
case H
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type u_1
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ (i : ι), ↑(S i)) (⨆ (i : ι), toSubsemigroup (S i))
    (_ : ↑(⨆ (i : ι), toSubsemigroup (S i)) = ⋃ (i : ι), ↑(toSubsemigroup (S i))) (⨆ (i : ι), (S i).toAddSubmonoid)
    (_ : ↑(⨆ (i : ι), (S i).toAddSubmonoid) = ⋃ (i : ι), ↑(S i).toAddSubmonoid)
⊢ ⨆ (i : ι), S i ≤ U
[PROOFSTEP]
exact iSup_le fun i x hx => Set.mem_iUnion.2 ⟨i, hx⟩
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type u_1
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ↑(⨆ (i : ι), S i) ↔ x ∈ ⋃ (i : ι), ↑(S i)
[PROOFSTEP]
simp [mem_iSup_of_directed hS]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type u_1
inst✝ : NonUnitalRingHomClass F R S✝
S : Set (NonUnitalSubsemiring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
[PROOFSTEP]
haveI : Nonempty S := Sne.to_subtype
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type u_1
inst✝ : NonUnitalRingHomClass F R S✝
S : Set (NonUnitalSubsemiring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
[PROOFSTEP]
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, Subtype.exists, exists_prop]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type u_1
inst✝ : NonUnitalRingHomClass F R S✝
S : Set (NonUnitalSubsemiring R)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ (s : NonUnitalSubsemiring R) (_ : s ∈ S), ↑s
[PROOFSTEP]
simp [mem_sSup_of_directedOn Sne hS]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝⁶ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝⁵ : NonUnitalNonAssocSemiring S
inst✝⁴ : NonUnitalNonAssocSemiring T
F : Type u_1
inst✝³ : NonUnitalNonAssocSemiring T
inst✝² : NonUnitalRingHomClass F R S
S' : Type u_2
inst✝¹ : SetLike S' S
inst✝ : NonUnitalSubsemiringClass S' S
s : NonUnitalSubsemiring R
f : F
⊢ ↑(srange f) = ↑⊤ ↔ Set.range ↑f = Set.univ
[PROOFSTEP]
rw [coe_srange, coe_top]
[GOAL]
R : Type u
S : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S
inst✝¹ : NonUnitalNonAssocSemiring T
s t : NonUnitalSubsemiring R
F : Type u_1
inst✝ : NonUnitalRingHomClass F R S
g : S → R
f : F
h : Function.LeftInverse g ↑f
src✝ : R →ₙ+* { x // x ∈ srange f } := srangeRestrict f
x : { x // x ∈ srange f }
x' : R
hx' : ↑f x' = ↑x
⊢ ↑f (g ↑x) = ↑x
[PROOFSTEP]
rw [← hx', h x']


[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : α → β
hf : Injective f
⊢ Injective (mapFun f)
[PROOFSTEP]
intros _ _ h
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : α → β
hf : Injective f
a₁✝ a₂✝ : 𝕎 α
h : mapFun f a₁✝ = mapFun f a₂✝
⊢ a₁✝ = a₂✝
[PROOFSTEP]
ext p
[GOAL]
case h
p✝ : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p✝)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : α → β
hf : Injective f
a₁✝ a₂✝ : WittVector p✝ α
h : mapFun f a₁✝ = mapFun f a₂✝
p : ℕ
⊢ coeff a₁✝ p = coeff a₂✝ p
[PROOFSTEP]
exact hf (congr_arg (fun x => coeff x p) h : _)
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : α → β
hf : Surjective f
x : 𝕎 β
⊢ mapFun f (mk p fun n => Classical.choose (_ : ∃ a, f a = coeff x n)) = x
[PROOFSTEP]
ext n
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : α → β
hf : Surjective f
x : 𝕎 β
n : ℕ
⊢ coeff (mapFun f (mk p fun n => Classical.choose (_ : ∃ a, f a = coeff x n))) n = coeff x n
[PROOFSTEP]
simp only [mapFun, coeff_mk, comp_apply, Classical.choose_spec (hf (x.coeff n))]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
⊢ mapFun (↑f) 0 = 0
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
⊢ mapFun (↑f) 1 = 1
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
⊢ mapFun (↑f) (x + y) = mapFun (↑f) x + mapFun (↑f) y
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
⊢ mapFun (↑f) (x - y) = mapFun (↑f) x - mapFun (↑f) y
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
⊢ mapFun (↑f) (x * y) = mapFun (↑f) x * mapFun (↑f) y
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
⊢ mapFun (↑f) (-x) = -mapFun (↑f) x
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
n : ℕ
⊢ mapFun (↑f) (n • x) = n • mapFun (↑f) x
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
z : ℤ
⊢ mapFun (↑f) (z • x) = z • mapFun (↑f) x
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
n : ℕ
⊢ mapFun (↑f) (x ^ n) = mapFun (↑f) x ^ n
[PROOFSTEP]
map_fun_tac
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
n : ℕ
⊢ mapFun (↑f) (Nat.unaryCast n) = ↑n
[PROOFSTEP]
induction n
[GOAL]
case zero
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
⊢ mapFun (↑f) (Nat.unaryCast Nat.zero) = ↑Nat.zero
[PROOFSTEP]
simp [*, Nat.unaryCast, add, one, zero]
[GOAL]
case succ
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
n✝ : ℕ
n_ih✝ : mapFun (↑f) (Nat.unaryCast n✝) = ↑n✝
⊢ mapFun (↑f) (Nat.unaryCast (Nat.succ n✝)) = ↑(Nat.succ n✝)
[PROOFSTEP]
simp [*, Nat.unaryCast, add, one, zero]
[GOAL]
case zero
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
⊢ 0 = ↑0
[PROOFSTEP]
rfl
[GOAL]
case succ
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
n✝ : ℕ
n_ih✝ : mapFun (↑f) (Nat.unaryCast n✝) = ↑n✝
⊢ ↑n✝ + 1 = ↑(Nat.succ n✝)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
n : ℤ
⊢ mapFun (↑f) (Int.castDef n) = ↑n
[PROOFSTEP]
cases n
[GOAL]
case ofNat
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
a✝ : ℕ
⊢ mapFun (↑f) (Int.castDef (Int.ofNat a✝)) = ↑(Int.ofNat a✝)
[PROOFSTEP]
simp [*, Int.castDef, add, one, neg, zero, nat_cast]
[GOAL]
case negSucc
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
a✝ : ℕ
⊢ mapFun (↑f) (Int.castDef (Int.negSucc a✝)) = ↑(Int.negSucc a✝)
[PROOFSTEP]
simp [*, Int.castDef, add, one, neg, zero, nat_cast]
[GOAL]
case ofNat
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
a✝ : ℕ
⊢ ↑a✝ = ↑↑a✝
[PROOFSTEP]
rfl
[GOAL]
case negSucc
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
f : R →+* S
x y : 𝕎 R
a✝ : ℕ
⊢ -↑(a✝ + 1) = ↑(Int.negSucc a✝)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R✝ : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R✝
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R✝
R : Type u_6
i : Fin 0
j : ℕ
⊢ coeff ![] j = ![]
[PROOFSTEP]
rcases i with ⟨_ | _ | _ | _ | i_val, ⟨⟩⟩
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
⊢ WittVector.ghostFun 0 = 0
[PROOFSTEP]
ghost_fun_tac 0,![]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
⊢ WittVector.ghostFun 1 = 1
[PROOFSTEP]
ghost_fun_tac 1,![]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
⊢ WittVector.ghostFun (x + y) = WittVector.ghostFun x + WittVector.ghostFun y
[PROOFSTEP]
ghost_fun_tac X 0 + X 1,![x.coeff, y.coeff]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
i : ℕ
⊢ WittVector.ghostFun (Nat.unaryCast i) = ↑i
[PROOFSTEP]
induction i
[GOAL]
case zero
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
⊢ WittVector.ghostFun (Nat.unaryCast Nat.zero) = ↑Nat.zero
[PROOFSTEP]
simp [*, Nat.unaryCast, ghostFun_zero, ghostFun_one, ghostFun_add, -Pi.coe_nat]
[GOAL]
case succ
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
n✝ : ℕ
n_ih✝ : WittVector.ghostFun (Nat.unaryCast n✝) = ↑n✝
⊢ WittVector.ghostFun (Nat.unaryCast (Nat.succ n✝)) = ↑(Nat.succ n✝)
[PROOFSTEP]
simp [*, Nat.unaryCast, ghostFun_zero, ghostFun_one, ghostFun_add, -Pi.coe_nat]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
⊢ WittVector.ghostFun (x - y) = WittVector.ghostFun x - WittVector.ghostFun y
[PROOFSTEP]
ghost_fun_tac X 0 - X 1,![x.coeff, y.coeff]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
⊢ WittVector.ghostFun (x * y) = WittVector.ghostFun x * WittVector.ghostFun y
[PROOFSTEP]
ghost_fun_tac X 0 * X 1,![x.coeff, y.coeff]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
⊢ WittVector.ghostFun (-x) = -WittVector.ghostFun x
[PROOFSTEP]
ghost_fun_tac-X 0,![x.coeff]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
i : ℤ
⊢ WittVector.ghostFun (Int.castDef i) = ↑i
[PROOFSTEP]
cases i
[GOAL]
case ofNat
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
a✝ : ℕ
⊢ WittVector.ghostFun (Int.castDef (Int.ofNat a✝)) = ↑(Int.ofNat a✝)
[PROOFSTEP]
simp [*, Int.castDef, ghostFun_nat_cast, ghostFun_neg, -Pi.coe_nat, -Pi.coe_int]
[GOAL]
case negSucc
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
a✝ : ℕ
⊢ WittVector.ghostFun (Int.castDef (Int.negSucc a✝)) = ↑(Int.negSucc a✝)
[PROOFSTEP]
simp [*, Int.castDef, ghostFun_nat_cast, ghostFun_neg, -Pi.coe_nat, -Pi.coe_int]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
m : ℕ
⊢ WittVector.ghostFun (m • x) = m • WittVector.ghostFun x
[PROOFSTEP]
ghost_fun_tac m • (X 0 : MvPolynomial _ ℤ),![x.coeff]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
m : ℤ
⊢ WittVector.ghostFun (m • x) = m • WittVector.ghostFun x
[PROOFSTEP]
ghost_fun_tac m • (X 0 : MvPolynomial _ ℤ),![x.coeff]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
x y : 𝕎 R
m : ℕ
⊢ WittVector.ghostFun (x ^ m) = WittVector.ghostFun x ^ m
[PROOFSTEP]
ghost_fun_tac X 0 ^ m,![x.coeff]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
⊢ LeftInverse (fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) WittVector.ghostFun
[PROOFSTEP]
intro x
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
x : 𝕎 R
⊢ (fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) (WittVector.ghostFun x) = x
[PROOFSTEP]
ext n
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
x : 𝕎 R
n : ℕ
⊢ coeff ((fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) (WittVector.ghostFun x)) n = coeff x n
[PROOFSTEP]
have := bind₁_wittPolynomial_xInTermsOfW p R n
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
x : 𝕎 R
n : ℕ
this : ↑(bind₁ (W_ R)) (xInTermsOfW p R n) = X n
⊢ coeff ((fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) (WittVector.ghostFun x)) n = coeff x n
[PROOFSTEP]
apply_fun aeval x.coeff at this
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
x : 𝕎 R
n : ℕ
this : ↑(aeval x.coeff) (↑(bind₁ (W_ R)) (xInTermsOfW p R n)) = ↑(aeval x.coeff) (X n)
⊢ coeff ((fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) (WittVector.ghostFun x)) n = coeff x n
[PROOFSTEP]
simpa only [aeval_bind₁, aeval_X, ghostFun, aeval_wittPolynomial]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
⊢ Function.RightInverse (fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) WittVector.ghostFun
[PROOFSTEP]
intro x
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
x : ℕ → R
⊢ WittVector.ghostFun ((fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) x) = x
[PROOFSTEP]
ext n
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
x : ℕ → R
n : ℕ
⊢ WittVector.ghostFun ((fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) x) n = x n
[PROOFSTEP]
have := bind₁_xInTermsOfW_wittPolynomial p R n
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
x : ℕ → R
n : ℕ
this : ↑(bind₁ (xInTermsOfW p R)) (W_ R n) = X n
⊢ WittVector.ghostFun ((fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) x) n = x n
[PROOFSTEP]
apply_fun aeval x at this
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : CommRing T
α : Type u_4
β : Type u_5
inst✝ : Invertible ↑p
x : ℕ → R
n : ℕ
this : ↑(aeval x) (↑(bind₁ (xInTermsOfW p R)) (W_ R n)) = ↑(aeval x) (X n)
⊢ WittVector.ghostFun ((fun x => mk p fun n => ↑(aeval x) (xInTermsOfW p R n)) x) n = x n
[PROOFSTEP]
simpa only [aeval_bind₁, aeval_X, ghostFun, aeval_wittPolynomial]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
⊢ (fun x => coeff x 0) 1 = 1
[PROOFSTEP]
simp
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
T : Type u_3
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_4
β : Type u_5
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun x => coeff x 0, map_one' := (_ : coeff 1 0 = 1) },
          map_mul' := (_ : ∀ (x y : 𝕎 R), coeff (x * y) 0 = coeff x 0 * coeff y 0) })
      0 =
    0
[PROOFSTEP]
simp