case h
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ φ k = wittStructureInt p Φ k
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ φ = wittStructureInt p Φ
funext k
case h.a
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (φ k) = ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ k)
case h
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ φ k = wittStructureInt p Φ k
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
case h.a
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k
case h.a
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (φ k) = ↑(map (Int.castRingHom ℚ)) (wittStructureInt p Φ k)
rw [map_wittStructureInt]
case h.a
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ∀ (k : ℕ), ↑(map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k
case h.a
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k
revert k
case h.a
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ (fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) = fun k => wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k
case h.a
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ∀ (k : ℕ), ↑(map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k
refine' congr_fun _
case h.a.py₁
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ∀ (n : ℕ),
    ↑(bind₁ fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
      ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)

case h.a.py₂
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ∀ (n : ℕ),
    ↑(bind₁ fun k => wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k) (W_ ℚ n) =
      ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
case h.a
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ (fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) = fun k => wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k
apply ExistsUnique.unique (wittStructureRat_existsUnique p (map (Int.castRingHom ℚ) Φ))
case h.a.py₁
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
n : ℕ
⊢ ↑(bind₁ fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
case h.a.py₁
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ∀ (n : ℕ),
    ↑(bind₁ fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
      ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
intro n
case h.a.py₁
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
n : ℕ
h : ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ↑(bind₁ fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
case h.a.py₁
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
n : ℕ
⊢ ↑(bind₁ fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
specialize h n
case h.a.py₁
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
n : ℕ
h :
  ↑(map (Int.castRingHom ℚ)) (↑(bind₁ φ) (W_ ℤ n)) =
    ↑(map (Int.castRingHom ℚ)) (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ)
⊢ ↑(bind₁ fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
case h.a.py₁
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
n : ℕ
h : ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ↑(bind₁ fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
apply_fun map (Int.castRingHom ℚ)  at h
no goals
case h.a.py₁
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
n : ℕ
h :
  ↑(map (Int.castRingHom ℚ)) (↑(bind₁ φ) (W_ ℤ n)) =
    ↑(map (Int.castRingHom ℚ)) (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ)
⊢ ↑(bind₁ fun k => ↑(map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
simpa only [map_bind₁, ← eval₂Hom_map_hom, eval₂Hom_C_left, map_rename, map_wittPolynomial,
  AlgHom.coe_toRingHom] using h
case h.a.py₂
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
n : ℕ
⊢ ↑(bind₁ fun k => wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
case h.a.py₂
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ∀ (n : ℕ),
    ↑(bind₁ fun k => wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k) (W_ ℚ n) =
      ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
intro n
no goals
case h.a.py₂
p : ℕ
R : Type ?u.1579762
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℤ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℤ n)) Φ
n : ℕ
⊢ ↑(bind₁ fun k => wittStructureRat p (↑(map (Int.castRingHom ℚ)) Φ) k) (W_ ℚ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) (↑(map (Int.castRingHom ℚ)) Φ)
apply wittStructureRat_prop