-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem eq_wittStructureInt (Φ : MvPolynomial idx ℤ) (φ : ℕ → MvPolynomial (idx × ℕ) ℤ)
    (h : ∀ n, bind₁ φ (wittPolynomial p ℤ n) = bind₁ (fun i => rename (Prod.mk i) (W_ ℤ n)) Φ) :
    φ = wittStructureInt p Φ

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)) Φ
⊢ φ = wittStructureInt p Φ

Tactic:
funext k

Result:
case 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)) Φ
k : ℕ
⊢ φ k = wittStructureInt p Φ k

Proof state:
case h.a.py₁
p : ℕ
idx : Type u_2
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 ℚ)) Φ)

Tactic:
simpa only [map_bind₁, ← eval₂Hom_map_hom, eval₂Hom_C_left, map_rename, map_wittPolynomial,
  AlgHom.coe_toRingHom] using h

Result:
no goals

Proof state:
case h.a
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)) Φ
k : ℕ
⊢ (map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) k

Tactic:
revert k

Result:
case h.a
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)) Φ
⊢ ∀ (k : ℕ), (map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) k

Proof state:
case h.a.py₁
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 k => (map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
    (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)

Tactic:
specialize h n

Result:
case h.a.py₁
p : ℕ
idx : Type u_2
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 ℚ)) Φ)

Proof state:
case h.a
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)) Φ
⊢ ∀ (k : ℕ), (map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) k

Tactic:
refine congr_fun ?_

Result:
case h.a
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)) Φ
⊢ (fun k => (map (Int.castRingHom ℚ)) (φ k)) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ)

Proof state:
case h.a.py₁
p : ℕ
idx : Type u_2
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 ℚ)) Φ)

Tactic:
apply_fun map (Int.castRingHom ℚ) at h

Result:
case h.a.py₁
p : ℕ
idx : Type u_2
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 ℚ)) Φ)

Proof state:
case h.a.py₂
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₁ (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n) =
      (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)

Tactic:
intro n

Result:
case h.a.py₂
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₁ (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n) =
    (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)

Proof state:
case 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)) Φ
k : ℕ
⊢ φ k = wittStructureInt p Φ k

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Result:
case h.a
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)) Φ
k : ℕ
⊢ (map (Int.castRingHom ℚ)) (φ k) = (map (Int.castRingHom ℚ)) (wittStructureInt p Φ k)

Proof state:
case h.a.py₁
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 k => (map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
      (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)

Tactic:
intro n

Result:
case h.a.py₁
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 k => (map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
    (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)

Proof state:
case h.a
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)) Φ
⊢ (fun k => (map (Int.castRingHom ℚ)) (φ k)) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ)

Tactic:
apply ExistsUnique.unique (wittStructureRat_existsUnique p (map (Int.castRingHom ℚ) Φ))

Result:
case h.a.py₁
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 k => (map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
      (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)

case h.a.py₂
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₁ (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n) =
      (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)

Proof state:
case h.a.py₂
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₁ (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n) =
    (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)

Tactic:
apply wittStructureRat_prop

Result:
no goals