case a
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑(map (Int.castRingHom ℚ)) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ) =
    ↑(map (Int.castRingHom ℚ)) (↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ =
    ↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n)
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
case a
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑(bind₁ fun i => ↑(expand p) (↑(rename fun i_1 => (i, i_1)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
case a
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑(map (Int.castRingHom ℚ)) (↑(bind₁ fun b => ↑(rename fun i => (b, i)) (↑(expand p) (W_ ℤ n))) Φ) =
    ↑(map (Int.castRingHom ℚ)) (↑(bind₁ fun i => ↑(expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
simp only [map_bind₁, map_rename, map_expand, rename_expand, map_wittPolynomial]
case a
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n)
⊢ ↑(bind₁ fun i => ↑(expand p) (↑(rename fun i_1 => (i, i_1)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
case a
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑(bind₁ fun i => ↑(expand p) (↑(rename fun i_1 => (i, i_1)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
have key := (wittStructureRat_prop p (map (Int.castRingHom ℚ) Φ) n).symm
case a
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(expand p) (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)) =
    ↑(expand p) (↑(bind₁ (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n))
⊢ ↑(bind₁ fun i => ↑(expand p) (↑(rename fun i_1 => (i, i_1)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
case a
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n)
⊢ ↑(bind₁ fun i => ↑(expand p) (↑(rename fun i_1 => (i, i_1)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
apply_fun expand p  at key
case a
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(bind₁ fun i => ↑(expand p) (↑(rename (Prod.mk i)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n)
⊢ ↑(bind₁ fun i => ↑(expand p) (↑(rename fun i_1 => (i, i_1)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
case a
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(expand p) (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)) =
    ↑(expand p) (↑(bind₁ (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n))
⊢ ↑(bind₁ fun i => ↑(expand p) (↑(rename fun i_1 => (i, i_1)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
simp only [expand_bind₁] at key
case a
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(bind₁ fun i => ↑(expand p) (↑(rename (Prod.mk i)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n)
⊢ ↑(bind₁ fun i => ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
case a
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(bind₁ fun i => ↑(expand p) (↑(rename (Prod.mk i)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n)
⊢ ↑(bind₁ fun i => ↑(expand p) (↑(rename fun i_1 => (i, i_1)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
rw [key]
case a
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑(bind₁ fun i => ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
case a
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
key :
  ↑(bind₁ fun i => ↑(expand p) (↑(rename (Prod.mk i)) (W_ ℚ n))) (↑(map (Int.castRingHom ℚ)) Φ) =
    ↑(bind₁ fun i => ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n)
⊢ ↑(bind₁ fun i => ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
clear key
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ∀ (i : ℕ),
    i ∈ vars (W_ ℚ n) →
      i ∈ vars (W_ ℚ n) →
        ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i) =
          ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
case a
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ↑(bind₁ fun i => ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)
apply eval₂Hom_congr' rfl _ rfl
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
i : ℕ
hi : i ∈ vars (W_ ℚ n)
⊢ ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i) =
    ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
⊢ ∀ (i : ℕ),
    i ∈ vars (W_ ℚ n) →
      i ∈ vars (W_ ℚ n) →
        ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i) =
          ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
rintro i hi -
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
i : ℕ
hi : i < n + 1
⊢ ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i) =
    ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
i : ℕ
hi : i ∈ vars (W_ ℚ n)
⊢ ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i) =
    ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
rw [wittPolynomial_vars, Finset.mem_range] at hi
no goals
p : ℕ
R : Type ?u.755142
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n + 1 →
      ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) m
i : ℕ
hi : i < n + 1
⊢ ↑(expand p) (wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) i) =
    ↑(expand p) (↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))
simp only [IH i hi]