-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem wittStructureRat_existsUnique (Φ : MvPolynomial idx ℚ) :
    ∃! φ : ℕ → MvPolynomial (idx × ℕ) ℚ,
      ∀ n : ℕ, bind₁ φ (W_ ℚ n) = bind₁ (fun i => rename (Prod.mk i) (W_ ℚ n)) Φ

Proof state:
case refine_2
p : ℕ
idx : Type u_2
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 Φ

Tactic:
intro φ H

Result:
case refine_2
p : ℕ
idx : Type u_2
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 Φ

Proof state:
case refine_2
p : ℕ
idx : Type u_2
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 Φ

Tactic:
funext n

Result:
case refine_2.h
p : ℕ
idx : Type u_2
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

Proof state:
p : ℕ
idx : Type u_2
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))

Tactic:
rw [bind₁_wittPolynomial_xInTermsOfW p, bind₁_X_right]

Result:
no goals

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ ∃! φ, ∀ (n : ℕ), (bind₁ φ) (W_ ℚ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) Φ

Tactic:
refine ⟨wittStructureRat p Φ, ?_, ?_⟩

Result:
case refine_1
p : ℕ
idx : Type u_2
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 : ℕ
idx : Type u_2
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 Φ

Proof state:
case refine_1
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ (wittStructureRat p Φ)) (W_ ℚ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) Φ

Tactic:
apply wittStructureRat_prop

Result:
no goals

Proof state:
case refine_1
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ (fun φ => ∀ (n : ℕ), (bind₁ φ) (W_ ℚ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) Φ) (wittStructureRat p Φ)

Tactic:
intro n

Result:
case refine_1
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ (wittStructureRat p Φ)) (W_ ℚ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) Φ

Proof state:
case refine_2.h
p : ℕ
idx : Type u_2
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

Tactic:
rw [bind₁_bind₁]

Result:
case refine_2.h
p : ℕ
idx : Type u_2
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

Proof state:
case refine_2.h
p : ℕ
idx : Type u_2
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

Tactic:
rw [show φ n = bind₁ φ (bind₁ (W_ ℚ) (xInTermsOfW p ℚ n)) by
    rw [bind₁_wittPolynomial_xInTermsOfW p, bind₁_X_right]]

Result:
case refine_2.h
p : ℕ
idx : Type u_2
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

Proof state:
case refine_2.h
p : ℕ
idx : Type u_2
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

Tactic:
exact eval₂Hom_congr (RingHom.ext_rat _ _) (funext H) rfl

Result:
no goals