case refine'_1
p : ℕ
R : Type ?u.216558
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ (fun φ => ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ) (wittStructureRat p Φ)

case refine'_2
p : ℕ
R : Type ?u.216558
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ ∀ (y : ℕ → MvPolynomial (idx × ℕ) ℚ),
    (fun φ => ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ) y →
      y = wittStructureRat p Φ
p : ℕ
R : Type ?u.216558
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ ∃! φ, ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
refine' ⟨wittStructureRat p Φ, _, _⟩
case refine'_1
p : ℕ
R : Type ?u.216558
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ (wittStructureRat p Φ)) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
case refine'_1
p : ℕ
R : Type ?u.216558
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ (fun φ => ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ) (wittStructureRat p Φ)
intro n
no goals
case refine'_1
p : ℕ
R : Type ?u.216558
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ↑(bind₁ (wittStructureRat p Φ)) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ
apply wittStructureRat_prop
case refine'_2
p : ℕ
R : Type ?u.216558
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)) Φ
⊢ φ = wittStructureRat p Φ
case refine'_2
p : ℕ
R : Type ?u.216558
idx : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ ∀ (y : ℕ → MvPolynomial (idx × ℕ) ℚ),
    (fun φ => ∀ (n : ℕ), ↑(bind₁ φ) (W_ ℚ n) = ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ n)) Φ) y →
      y = wittStructureRat p Φ
intro φ H
case refine'_2.h
p : ℕ
R : Type ?u.216558
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 : ℕ
⊢ φ n = wittStructureRat p Φ n
case refine'_2
p : ℕ
R : Type ?u.216558
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)) Φ
⊢ φ = wittStructureRat p Φ
funext n
case refine'_2.h
p : ℕ
R : Type ?u.216558
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₁ φ) (↑(bind₁ (W_ ℚ)) (xInTermsOfW p ℚ n)) = wittStructureRat p Φ n
case refine'_2.h
p : ℕ
R : Type ?u.216558
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 : ℕ
⊢ φ n = wittStructureRat p Φ n
rw [show φ n = bind₁ φ (bind₁ (W_ ℚ) (xInTermsOfW p ℚ n)) by
    rw [bind₁_wittPolynomial_xInTermsOfW p, bind₁_X_right]]
case refine'_2.h
p : ℕ
R : Type ?u.216558
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 i => ↑(bind₁ φ) (W_ ℚ i)) (xInTermsOfW p ℚ n) = wittStructureRat p Φ n
case refine'_2.h
p : ℕ
R : Type ?u.216558
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₁ φ) (↑(bind₁ (W_ ℚ)) (xInTermsOfW p ℚ n)) = wittStructureRat p Φ n
rw [bind₁_bind₁]
no goals
case refine'_2.h
p : ℕ
R : Type ?u.216558
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 i => ↑(bind₁ φ) (W_ ℚ i)) (xInTermsOfW p ℚ n) = wittStructureRat p Φ n
exact eval₂Hom_congr (RingHom.ext_rat _ _) (funext H) rfl
no goals
p : ℕ
R : Type ?u.216558
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 : ℕ
⊢ φ n = ↑(bind₁ φ) (↑(bind₁ (W_ ℚ)) (xInTermsOfW p ℚ n))
rw [bind₁_wittPolynomial_xInTermsOfW p, bind₁_X_right]