-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem bind₁_rename_expand_wittPolynomial (Φ : 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)

Proof state:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ 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)

Tactic:
rw [key]

Result:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ 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)

Proof state:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ 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)

Tactic:
simp only [expand_bind₁] at key

Result:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ 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)

Proof state:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ 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)

Tactic:
apply eval₂Hom_congr' rfl _ rfl

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
⊢ ∀ i ∈ (W_ ℚ n).vars,
    i ∈ (W_ ℚ n).vars →
      (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i) =
        (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ 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))

Tactic:
simp only [IH i hi]

Result:
no goals

Proof state:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ 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)

Tactic:
apply_fun expand p at key

Result:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ 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)

Proof state:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ 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)

Tactic:
clear key

Result:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ 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)

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
⊢ ∀ i ∈ (W_ ℚ n).vars,
    i ∈ (W_ ℚ n).vars →
      (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i) =
        (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))

Tactic:
rintro i hi -

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
i : ℕ
hi : i ∈ (W_ ℚ n).vars
⊢ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i) =
    (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
i : ℕ
hi : i ∈ (W_ ℚ n).vars
⊢ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i) =
    (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))

Tactic:
rw [wittPolynomial_vars, Finset.mem_range] at hi

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ 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))