awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
a :
  Eq.{u_3 + 1} (α := MvPolynomial (σ × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (σ × ℕ) ℤ) → MvPolynomial (σ × ℕ) ℚ)
        (wittStructureInt p
          (((rename f : AlgHom.{0, u_2, u_3} ℤ (MvPolynomial idx ℤ) (MvPolynomial σ ℤ)) :
              (a : MvPolynomial idx ℤ) → MvPolynomial σ ℤ)
            Φ)
          n) :
      MvPolynomial (σ × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (σ × ℕ) ℤ) → MvPolynomial (σ × ℕ) ℚ)
        (((rename (Prod.map f id) : AlgHom.{0, u_2, u_3} ℤ (MvPolynomial (idx × ℕ) ℤ) (MvPolynomial (σ × ℕ) ℤ)) :
              (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (σ × ℕ) ℤ)
            (wittStructureInt p Φ n) :
          MvPolynomial (σ × ℕ) ℤ) :
      MvPolynomial (σ × ℕ) ℚ)
⊢ Eq.{u_3 + 1} (α := MvPolynomial (σ × ℕ) ℤ)
    (wittStructureInt p
      (((rename f : AlgHom.{0, u_2, u_3} ℤ (MvPolynomial idx ℤ) (MvPolynomial σ ℤ)) :
          (a : MvPolynomial idx ℤ) → MvPolynomial σ ℤ)
        Φ)
      n)
    (((rename (Prod.map f id) : AlgHom.{0, u_2, u_3} ℤ (MvPolynomial (idx × ℕ) ℤ) (MvPolynomial (σ × ℕ) ℤ)) :
        (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (σ × ℕ) ℤ)
      (wittStructureInt p Φ n))

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

Premises used: Rat, MvPolynomial.map_injective, Int.castRingHom, Int.cast_injective
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
a :
  Eq.{u_3 + 1} (α := MvPolynomial (σ × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦
            ((bind₁
                    ((fun (i : σ) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (σ × ℕ) ℚ) (W_ ℚ k)) ∘
                      f) :
                  AlgHom.{0, u_2, u_3} ℚ (MvPolynomial idx ℚ) (MvPolynomial (σ × ℕ) ℚ)) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (σ × ℕ) ℚ)
              ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (σ × ℕ) ℚ)
        (xInTermsOfW p ℚ n) :
      MvPolynomial (σ × ℕ) ℚ)
    ((bind₁ fun (i : ℕ) ↦
            (bind₁ fun (i_1 : idx) ↦
                  (rename (Prod.map f id ∘ Prod.mk i_1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (σ × ℕ) ℚ) (W_ ℚ i) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (σ × ℕ) ℚ)
              ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (σ × ℕ) ℚ)
        (xInTermsOfW p ℚ n) :
      MvPolynomial (σ × ℕ) ℚ)
⊢ Eq.{u_3 + 1} (α := MvPolynomial (σ × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (σ × ℕ) ℤ) → MvPolynomial (σ × ℕ) ℚ)
        (wittStructureInt p
          (((rename f : AlgHom.{0, u_2, u_3} ℤ (MvPolynomial idx ℤ) (MvPolynomial σ ℤ)) :
              (a : MvPolynomial idx ℤ) → MvPolynomial σ ℤ)
            Φ)
          n) :
      MvPolynomial (σ × ℕ) ℚ)
    ((map (Int.castRingHom ℚ) : (a : MvPolynomial (σ × ℕ) ℤ) → MvPolynomial (σ × ℕ) ℚ)
        (((rename (Prod.map f id) : AlgHom.{0, u_2, u_3} ℤ (MvPolynomial (idx × ℕ) ℤ) (MvPolynomial (σ × ℕ) ℤ)) :
              (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (σ × ℕ) ℤ)
            (wittStructureInt p Φ n) :
          MvPolynomial (σ × ℕ) ℤ) :
      MvPolynomial (σ × ℕ) ℚ)

Tactic:
simp only [map_rename, map_wittStructureInt, wittStructureRat, rename_bind₁, rename_rename,
    bind₁_rename]

Premises used: MvPolynomial.rename_rename, MvPolynomial.map_rename, MvPolynomial.bind₁_rename, wittStructureRat, MvPolynomial.rename_bind₁, map_wittStructureInt
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ Eq.{u_3 + 1} (α := MvPolynomial (σ × ℕ) ℚ)
    ((bind₁ fun (k : ℕ) ↦
            ((bind₁
                    ((fun (i : σ) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (σ × ℕ) ℚ) (W_ ℚ k)) ∘
                      f) :
                  AlgHom.{0, u_2, u_3} ℚ (MvPolynomial idx ℚ) (MvPolynomial (σ × ℕ) ℚ)) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (σ × ℕ) ℚ)
              ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (σ × ℕ) ℚ)
        (xInTermsOfW p ℚ n) :
      MvPolynomial (σ × ℕ) ℚ)
    ((bind₁ fun (i : ℕ) ↦
            (bind₁ fun (i_1 : idx) ↦
                  (rename (Prod.map f id ∘ Prod.mk i_1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (σ × ℕ) ℚ) (W_ ℚ i) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (σ × ℕ) ℚ)
              ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (σ × ℕ) ℚ)
        (xInTermsOfW p ℚ n) :
      MvPolynomial (σ × ℕ) ℚ)

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ Eq (α := ℚ) ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℚ) → ℚ) (wittStructureRat p Φ 0) : ℚ)
    ((constantCoeff : (a : MvPolynomial idx ℚ) → ℚ) Φ : ℚ)

Tactic:
simp only [wittStructureRat, bind₁, map_aeval, xInTermsOfW_zero, constantCoeff_rename,
    constantCoeff_wittPolynomial, aeval_X, constantCoeff_comp_algebraMap, eval₂Hom_zero'_apply,
    RingHom.id_apply]

Premises used: MvPolynomial.aeval_X, RingHom.id_apply, MvPolynomial.constantCoeff_rename, MvPolynomial.map_aeval, wittStructureRat, MvPolynomial.eval₂Hom_zero'_apply, constantCoeff_wittPolynomial, MvPolynomial.bind₁, xInTermsOfW_zero, MvPolynomial.constantCoeff_comp_algebraMap
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
h : Eq (α := ℚ) ((constantCoeff : (a : MvPolynomial idx ℚ) → ℚ) Φ : ℚ) (0 : ℚ)
n : ℕ
⊢ Eq (α := ℚ) ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℚ) → ℚ) (wittStructureRat p Φ n) : ℚ) (0 : ℚ)

Tactic:
simp only [wittStructureRat, eval₂Hom_zero'_apply, h, bind₁, map_aeval, constantCoeff_rename,
    constantCoeff_wittPolynomial, constantCoeff_comp_algebraMap, RingHom.id_apply,
    constantCoeff_xInTermsOfW]

Premises used: RingHom.id_apply, MvPolynomial.constantCoeff_rename, MvPolynomial.map_aeval, wittStructureRat, MvPolynomial.eval₂Hom_zero'_apply, constantCoeff_wittPolynomial, MvPolynomial.bind₁, constantCoeff_xInTermsOfW, MvPolynomial.constantCoeff_comp_algebraMap
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
m n : ℤ
⊢ Eq (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) m : ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) n : ℚ) → m = n

Tactic:
Int.cast_inj.mp

Premises used: Int.cast_inj, Iff.mp
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
m n : ℤ
⊢ Eq (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) m : ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) n : ℚ) → m = n

Tactic:
exact Int.cast_inj.mp

Premises used: Int.cast_inj, Iff.mp
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
⊢ Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)

Tactic:
have inj : Function.Injective (Int.castRingHom ℚ) := by intro m n; exact Int.cast_inj.mp
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
a :
  Eq (α := ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
        ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℤ) → ℤ) (wittStructureInt p Φ 0) : ℤ) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℤ) → ℤ) (wittStructureInt p Φ 0) : ℤ)
    ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ)

Tactic:
apply inj
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
inj : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
a :
  Eq (α := ℚ)
    ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℚ) → ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ)
            (wittStructureInt p Φ 0) :
          MvPolynomial (idx × ℕ) ℚ) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
a₁ :
  Eq (α := ℚ)
    ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℚ) → ℚ)
        (wittStructureRat p ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ) 0) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
a₂ :
  Eq (α := ℚ)
    ((constantCoeff : (a : MvPolynomial idx ℚ) → ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
a₃ a₄ :
  Eq (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)
⊢ Eq (α := ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
        ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℤ) → ℤ) (wittStructureInt p Φ 0) : ℤ) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ)

Tactic:
rw [← constantCoeff_map, map_wittStructureInt, constantCoeff_wittStructureRat_zero,
    constantCoeff_map]

Premises used: constantCoeff_wittStructureRat_zero, map_wittStructureInt, MvPolynomial.constantCoeff_map
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) (0 : ℤ)
n_1 : ℕ
m n : ℤ
⊢ Eq (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) m : ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) n : ℚ) → m = n

Tactic:
Int.cast_inj.mp

Premises used: Int.cast_inj, Iff.mp
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) (0 : ℤ)
n_1 : ℕ
m n : ℤ
⊢ Eq (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) m : ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) n : ℚ) → m = n

Tactic:
exact Int.cast_inj.mp

Premises used: Int.cast_inj, Iff.mp
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) (0 : ℤ)
n : ℕ
⊢ Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)

Tactic:
have inj : Function.Injective (Int.castRingHom ℚ) := by intro m n; exact Int.cast_inj.mp
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) (0 : ℤ)
n : ℕ
inj : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
a :
  Eq (α := ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
        ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℤ) → ℤ) (wittStructureInt p Φ n) : ℤ) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) 0 : ℚ)
⊢ Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℤ) → ℤ) (wittStructureInt p Φ n) : ℤ) (0 : ℤ)

Tactic:
apply inj
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) (0 : ℤ)
n : ℕ
inj : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
a :
  Eq (α := ℚ)
    ((constantCoeff : (a : MvPolynomial idx ℚ) → ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
      ℚ)
    (0 : ℚ)
⊢ Eq (α := ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ)
        ((constantCoeff : (a : MvPolynomial (idx × ℕ) ℤ) → ℤ) (wittStructureInt p Φ n) : ℤ) :
      ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) 0 : ℚ)

Tactic:
rw [← constantCoeff_map, map_wittStructureInt, constantCoeff_wittStructureRat, map_zero]

Premises used: constantCoeff_wittStructureRat, map_zero, map_wittStructureInt, MvPolynomial.constantCoeff_map
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
h : Eq (α := ℤ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) (0 : ℤ)
n : ℕ
inj : Function.Injective (α := ℤ) (β := ℚ) (⇑(Int.castRingHom ℚ) : (a : ℤ) → ℚ)
a : Eq (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) ((constantCoeff : (a : MvPolynomial idx ℤ) → ℤ) Φ : ℤ) : ℚ) (0 : ℚ)
a₁ : Eq (α := ℚ) ((Int.castRingHom ℚ : (a : ℤ) → ℚ) 0 : ℚ) (0 : ℚ)
a₂ a₃ : Eq (α := ℚ) 0 0
⊢ Eq (α := ℚ)
    ((constantCoeff : (a : MvPolynomial idx ℚ) → ℚ)
        ((map (Int.castRingHom ℚ) : (a : MvPolynomial idx ℤ) → MvPolynomial idx ℚ) Φ : MvPolynomial idx ℚ) :
      ℚ)
    (0 : ℚ)

Tactic:
rw [constantCoeff_map, h, map_zero]

Premises used: map_zero, MvPolynomial.constantCoeff_map
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (xInTermsOfW p ℚ n)))
    x
simp : x.2 < n + 1
⊢ x ∈ SProd.sprod (α := Finset idx) Finset.univ (Finset.range (n + 1))

Tactic:
simp only [Finset.mem_product, true_and, Finset.mem_univ, Finset.mem_range]

Premises used: Finset.mem_univ, Finset.mem_range, Finset.mem_product, true_and
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (xInTermsOfW p ℚ n)))
    x
obtain :
  ∀ (k : ℕ) (hk : k ∈ vars (xInTermsOfW p ℚ n))
    (hx' :
      Membership.mem (γ := Finset (idx × ℕ))
        (vars (R := ℚ)
          ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
              (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
            Φ))
        x),
    x.2 < n + 1
⊢ x.2 < n + 1

Tactic:
obtain ⟨k, hk, hx'⟩ := mem_vars_bind₁ _ _ hx

Premises used: MvPolynomial.mem_vars_bind₁
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (xInTermsOfW p ℚ n)))
    x
k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
hx' :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        Φ))
    x
obtain :
  ∀ (i : idx)
    (hx'' :
      Membership.mem (γ := Finset (idx × ℕ))
        (vars (R := ℚ) ((rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k))) x),
    x.2 < n + 1
⊢ x.2 < n + 1

Tactic:
obtain ⟨i, -, hx''⟩ := mem_vars_bind₁ _ _ hx'

Premises used: MvPolynomial.mem_vars_bind₁
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (xInTermsOfW p ℚ n)))
    x
k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
hx' :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        Φ))
    x
i : idx
hx'' :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ) ((rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k))) x
obtain :
  ∀ (j : ℕ) (hj : j ∈ vars (W_ ℚ k))
    (hx :
      Membership.mem (γ := Finset (idx × ℕ))
        (vars (R := ℚ)
          ((bind₁ fun (k : ℕ) ↦
                (bind₁ fun (i : idx) ↦
                      (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                    (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
                  Φ :
              (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
            (xInTermsOfW p ℚ n)))
        (i, j))
    (hx' :
      Membership.mem (γ := Finset (idx × ℕ))
        (vars (R := ℚ)
          ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
              (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
            Φ))
        (i, j))
    (hx'' :
      Membership.mem (γ := Finset (idx × ℕ))
        (vars (R := ℚ) ((rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k))) (i, j)),
    (i, j).2 < n + 1
⊢ x.2 < n + 1

Tactic:
obtain ⟨j, hj, rfl⟩ := mem_vars_rename _ _ hx''

Premises used: MvPolynomial.mem_vars_rename, rfl
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
i : idx
j : ℕ
hj : j ∈ vars (W_ ℚ k)
hx :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (xInTermsOfW p ℚ n)))
    (i, j)
hx' :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        Φ))
    (i, j)
hx'' :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ) ((rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k))) (i, j)
⊢ j < k + 1

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

Premises used: wittPolynomial_vars, Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
i : idx
j : ℕ
hj : j ∈ vars (W_ ℚ k)
hx :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (xInTermsOfW p ℚ n)))
    (i, j)
hx' :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        Φ))
    (i, j)
hx'' :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ) ((rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k))) (i, j)
hj₁ : j < k + 1
⊢ Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (xInTermsOfW p ℚ n)))
    (i, j)

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

Premises used: wittPolynomial_vars, Finset.mem_range
-- Module: Mathlib.RingTheory.WittVector.StructurePolynomial
Goal:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
i : idx
j : ℕ
hj : j ∈ vars (W_ ℚ k)
hx :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (xInTermsOfW p ℚ n)))
    (i, j)
hx' :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        Φ))
    (i, j)
hx'' :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ) ((rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k))) (i, j)
hj₁ : j < k + 1
hx₁ :
  Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (k : ℕ) ↦
            (bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
                (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
              Φ :
          (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ)
        (xInTermsOfW p ℚ n)))
    (i, j)
⊢ Membership.mem (γ := Finset (idx × ℕ))
    (vars (R := ℚ)
      ((bind₁ fun (i : idx) ↦ (rename (Prod.mk i) : (a : MvPolynomial ℕ ℚ) → MvPolynomial (idx × ℕ) ℚ) (W_ ℚ k) :
          (a : MvPolynomial idx ℚ) → MvPolynomial (idx × ℕ) ℚ)
        Φ))
    (i, j)

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

Premises used: wittPolynomial_vars, Finset.mem_range