diff --git a/src/ring_theory/witt_vector/structure_polynomial.lean b/src/ring_theory/witt_vector/structure_polynomial.lean
index 90050cec32131..51863dfdbb23d 100644
--- a/src/ring_theory/witt_vector/structure_polynomial.lean
+++ b/src/ring_theory/witt_vector/structure_polynomial.lean
@@ -63,6 +63,10 @@ dvd_sub_pow_of_dvd_sub {R : Type*} [comm_ring R] {p : ℕ} {a b : R} :
 * `witt_structure_rat Φ`: the family of polynomials `ℕ → mv_polynomial (idx × ℕ) ℚ`
   associated with `Φ : mv_polynomial idx ℚ` and satisfying the property explained above.
 * `witt_structure_rat_prop`: the proof that `witt_structure_rat` indeed satisfies the property.
+* `witt_structure_int Φ`: the family of polynomials `ℕ → mv_polynomial (idx × ℕ) ℤ`
+  associated with `Φ : mv_polynomial idx ℤ` and satisfying the property explained above.
+* `map_witt_structure_int`: the proof that the integral polynomials `with_structure_int Φ`
+  are equal to `witt_structure_rat Φ` when mapped to polynomials with rational coefficients.
 
 -/
 
@@ -128,9 +132,140 @@ begin
         exact eval₂_hom_congr (ring_hom.ext_rat _ _) (funext H) rfl },
 end
 
+lemma witt_structure_rat_rec_aux (Φ : mv_polynomial idx ℚ) (n : ℕ) :
+  witt_structure_rat p Φ n * C (p ^ n : ℚ) =
+    bind₁ (λ b, rename (λ i, (b, i)) (W_ ℚ n)) Φ -
+      ∑ i in range n, C (p ^ i : ℚ) * (witt_structure_rat p Φ i) ^ p ^ (n - i) :=
+begin
+  have := X_in_terms_of_W_aux p ℚ n,
+  replace := congr_arg (bind₁ (λ k : ℕ, bind₁ (λ i, rename (prod.mk i) (W_ ℚ k)) Φ)) this,
+  rw [alg_hom.map_mul, bind₁_C_right] at this,
+  convert this, clear this,
+  conv_rhs { simp only [alg_hom.map_sub, bind₁_X_right] },
+  rw sub_right_inj,
+  simp only [alg_hom.map_sum, alg_hom.map_mul, bind₁_C_right, alg_hom.map_pow],
+  refl
+end
+
+/-- Write `witt_structure_rat p φ n` in terms of `witt_structure_rat p φ i` for `i < n`. -/
+lemma witt_structure_rat_rec (Φ : mv_polynomial idx ℚ) (n : ℕ) :
+  (witt_structure_rat p Φ n) = C (1 / p ^ n : ℚ) *
+  (bind₁ (λ b, (rename (λ i, (b, i)) (W_ ℚ n))) Φ -
+  ∑ i in range n, C (p ^ i : ℚ) * (witt_structure_rat p Φ i) ^ p ^ (n - i)) :=
+begin
+  calc witt_structure_rat p Φ n
+      = C (1 / p ^ n : ℚ) * (witt_structure_rat p Φ n * C (p ^ n : ℚ)) : _
+  ... = _ : by rw witt_structure_rat_rec_aux,
+  rw [mul_left_comm, ← C_mul, div_mul_cancel, C_1, mul_one],
+  exact pow_ne_zero _ (nat.cast_ne_zero.2 $ ne_of_gt (nat.prime.pos ‹_›)),
+end
+
+/-- `witt_structure_int Φ` is a family of polynomials `ℕ → mv_polynomial (idx × ℕ) ℚ`
+that are uniquely characterised by the property that
+`bind₁ (witt_structure_int p Φ) (witt_polynomial p ℚ n) = bind₁ (λ i, (rename (prod.mk i) (witt_polynomial p ℚ n))) Φ`.
+In other words: evaluating the `n`-th Witt polynomial on the family `witt_structure_int Φ`
+is the same as evaluating `Φ` on the (appropriately renamed) `n`-th Witt polynomials.
+
+See `witt_structure_int_prop` for this property,
+and `witt_structure_int_exists_unique` for the fact that `witt_structure_int`
+gives the unique family of polynomials with this property. -/
+noncomputable def witt_structure_int (Φ : mv_polynomial idx ℤ) (n : ℕ) : mv_polynomial (idx × ℕ) ℤ :=
+finsupp.map_range rat.num (rat.coe_int_num 0)
+  (witt_structure_rat p (map (int.cast_ring_hom ℚ) Φ) n)
+
+variable {p}
+
+lemma bind₁_rename_expand_witt_polynomial (Φ : mv_polynomial idx ℤ) (n : ℕ)
+  (IH : ∀ m : ℕ, m < (n + 1) →
+    map (int.cast_ring_hom ℚ) (witt_structure_int p Φ m) =
+      witt_structure_rat p (map (int.cast_ring_hom ℚ) Φ) m) :
+  bind₁ (λ b, rename (λ i, (b, i)) (expand p (W_ ℤ n))) Φ =
+    bind₁ (λ i, expand p (witt_structure_int p Φ i)) (W_ ℤ n) :=
+begin
+  apply mv_polynomial.map_injective (int.cast_ring_hom ℚ) int.cast_injective,
+  simp only [map_bind₁, map_rename, map_expand, rename_expand, map_witt_polynomial],
+  have key := (witt_structure_rat_prop p (map (int.cast_ring_hom ℚ) Φ) n).symm,
+  apply_fun expand p at key,
+  simp only [expand_bind₁] at key,
+  rw key, clear key,
+  apply eval₂_hom_congr' rfl _ rfl,
+  rintro i hi -,
+  rw [witt_polynomial_vars, finset.mem_range] at hi,
+  simp only [IH i hi],
+end
+
+lemma C_p_pow_dvd_bind₁_rename_witt_polynomial_sub_sum (Φ : mv_polynomial idx ℤ) (n : ℕ)
+  (IH : ∀ m : ℕ, m < n →
+    map (int.cast_ring_hom ℚ) (witt_structure_int p Φ m) =
+      witt_structure_rat p (map (int.cast_ring_hom ℚ) Φ) m) :
+  C ↑(p ^ n) ∣
+    (bind₁ (λ (b : idx), rename (λ i, (b, i)) (witt_polynomial p ℤ n)) Φ -
+      ∑ i in range n, C (↑p ^ i) * witt_structure_int p Φ i ^ p ^ (n - i)) :=
+begin
+  cases n,
+  { simp only [is_unit_one, int.coe_nat_zero, int.coe_nat_succ, zero_add, pow_zero, C_1, is_unit.dvd] },
+
+  -- prepare a useful equation for rewriting
+  have key := bind₁_rename_expand_witt_polynomial Φ n IH,
+  apply_fun (map (int.cast_ring_hom (zmod (p ^ (n + 1))))) at key,
+  conv_lhs at key { simp only [map_bind₁, map_rename, map_expand, map_witt_polynomial] },
+
+  -- clean up and massage
+  rw [nat.succ_eq_add_one, C_dvd_iff_zmod, ring_hom.map_sub, sub_eq_zero, map_bind₁],
+  simp only [map_rename, map_witt_polynomial, witt_polynomial_zmod_self],
+  rw key, clear key IH,
+  rw [bind₁, aeval_witt_polynomial, ring_hom.map_sum, ring_hom.map_sum, finset.sum_congr rfl],
+  intros k hk,
+  rw finset.mem_range at hk,
+  simp only [← sub_eq_zero, ← ring_hom.map_sub, ← C_dvd_iff_zmod, C_eq_coe_nat, ← mul_sub,
+    ← int.nat_cast_eq_coe_nat, ← nat.cast_pow],
+  rw show p ^ (n + 1) = p ^ k * p ^ (n - k + 1),
+  { rw ← pow_add, congr' 1, omega },
+  rw [nat.cast_mul, nat.cast_pow, nat.cast_pow],
+  apply mul_dvd_mul_left,
+  rw show p ^ (n + 1 - k) = p * p ^ (n - k),
+  { rw ← pow_succ, congr' 1, omega },
+  rw [pow_mul],
+  -- the machine!
+  apply dvd_sub_pow_of_dvd_sub,
+  rw [← C_eq_coe_nat, int.nat_cast_eq_coe_nat, C_dvd_iff_zmod, ring_hom.map_sub,
+      sub_eq_zero, map_expand, ring_hom.map_pow, mv_polynomial.expand_zmod],
+end
+
+variables (p)
+
+@[simp] lemma map_witt_structure_int (Φ : mv_polynomial idx ℤ) (n : ℕ) :
+  map (int.cast_ring_hom ℚ) (witt_structure_int p Φ n) =
+    witt_structure_rat p (map (int.cast_ring_hom ℚ) Φ) n :=
+begin
+  apply nat.strong_induction_on n, clear n,
+  intros n IH,
+  rw [witt_structure_int, map_map_range_eq_iff, int.coe_cast_ring_hom],
+  intro c,
+  rw [witt_structure_rat_rec, coeff_C_mul, mul_comm, mul_div_assoc', mul_one],
+  have sum_induction_steps : map (int.cast_ring_hom ℚ)
+   (∑ i in range n, C (p ^ i : ℤ) *
+     (witt_structure_int p Φ i) ^ p ^ (n - i)) =
+    ∑ i in range n, C (p ^ i : ℚ) *
+      (witt_structure_rat p (map (int.cast_ring_hom ℚ) Φ) i) ^ p ^ (n - i),
+  { rw [ring_hom.map_sum],
+    apply finset.sum_congr rfl,
+    intros i hi,
+    rw finset.mem_range at hi,
+    simp only [IH i hi, ring_hom.map_mul, ring_hom.map_pow, map_C],
+    refl },
+  simp only [← sum_induction_steps, ← map_witt_polynomial p (int.cast_ring_hom ℚ),
+    ← map_rename, ← map_bind₁, ← ring_hom.map_sub, coeff_map],
+  rw show (p : ℚ)^n = ((p^n : ℕ) : ℤ), by norm_cast,
+  rw [← rat.denom_eq_one_iff, ring_hom.eq_int_cast, rat.denom_div_cast_eq_one_iff],
+  swap, { exact_mod_cast pow_ne_zero n hp.ne_zero },
+  revert c, rw [← C_dvd_iff_dvd_coeff],
+  exact C_p_pow_dvd_bind₁_rename_witt_polynomial_sub_sum Φ n IH,
+end
+
 /-
-TODO: In a follow-up PR we define `witt_structure_int`
-and prove that it satisfies the properties claimed above.
+TODO: in a follow-up PR, we deduce `witt_structure_int_prop` from `witt_structure_rat_prop`
+using `map_witt_structure_int` (easy, 5 lines) and some other properties.
 -/
 
 end p_prime