awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f x x_1 : MvPolynomial σ R
ha :
  (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x) =
    x ^ p
hb :
  (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1) =
    x_1 ^ p
rw :
  (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x : MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1 : MvPolynomial σ R)) =
    (x + x_1) ^ p
rw₁ :
  HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x) :
        MvPolynomial σ R)
      ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1) :
        MvPolynomial σ R) =
    (x + x_1) ^ p
rw₂ :
  HAdd.hAdd (β := MvPolynomial σ R) (x ^ p)
      ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1) :
        MvPolynomial σ R) =
    (x + x_1) ^ p
⊢ (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) (x + x_1)) =
    (x + x_1) ^ p
have rw₃ : x ^ p + x_1 ^ p = (x + x_1) ^ p
Tactic: rw [map_add, map_add, ha, hb, add_pow_expChar]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f x x_1 : MvPolynomial σ R
ha :
  (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x) =
    x ^ p
hb :
  (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1) =
    x_1 ^ p
rw :
  (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x : MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1 : MvPolynomial σ R)) =
    (x + x_1) ^ p
rw₁ :
  HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x) :
        MvPolynomial σ R)
      ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1) :
        MvPolynomial σ R) =
    (x + x_1) ^ p
rw₂ :
  HAdd.hAdd (β := MvPolynomial σ R) (x ^ p)
      ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1) :
        MvPolynomial σ R) =
    (x + x_1) ^ p
rw₃ : x ^ p + x_1 ^ p = (x + x_1) ^ p
⊢ (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) (x + x_1)) =
    (x + x_1) ^ p
have rw₄ : x ^ p + x_1 ^ p = x ^ p + x_1 ^ p
Tactic: rw [map_add, map_add, ha, hb, add_pow_expChar]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ p ^ k
⊢ (map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ p ^ (k + 1)
have succ : f ^ p ^ (k + 1) =
  (map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
    ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f)
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ p ^ k
| f ^ p ^ (k + 1)
have rw : HPow.hPow (α := MvPolynomial σ R)
  ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
    MvPolynomial σ R)
  p
Tactic: rw [pow_succ, pow_mul, ← n_ih]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ p ^ k
⊢ f ^ p ^ (k + 1) =
    (map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f)
have succ : HPow.hPow (α := MvPolynomial σ R)
    ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
    p =
  (map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
    ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f)
Tactic: conv_lhs => rw [pow_succ, pow_mul, ← n_ih]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ p ^ k
⊢ HPow.hPow (α := MvPolynomial σ R)
      ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
        MvPolynomial σ R)
      p =
    (map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f)
have succ : Eq (α := MvPolynomial σ R)
  ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f))) :
    MvPolynomial σ R)
  ((map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
    MvPolynomial σ R)
Tactic: simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ p ^ k
succ :
  Eq (α := MvPolynomial σ R)
    ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f))) :
      MvPolynomial σ R)
    ((map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
⊢ HPow.hPow (α := MvPolynomial σ R)
      ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
        MvPolynomial σ R)
      p =
    (map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f)
have succ₁ : Eq (α := MvPolynomial σ R)
  ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f))) :
    MvPolynomial σ R)
  ((map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p * p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
    MvPolynomial σ R)
Tactic: simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ p ^ k
succ :
  Eq (α := MvPolynomial σ R)
    ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f))) :
      MvPolynomial σ R)
    ((map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
succ₁ :
  Eq (α := MvPolynomial σ R)
    ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f))) :
      MvPolynomial σ R)
    ((map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand (p * p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
⊢ HPow.hPow (α := MvPolynomial σ R)
      ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
        MvPolynomial σ R)
      p =
    (map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f)
have succ₂ : Eq (α := MvPolynomial σ R)
  ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f))) :
    MvPolynomial σ R)
  ((map (iterateFrobenius R p (1 + k)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p * p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
    MvPolynomial σ R)
Tactic: simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ p ^ k
succ :
  Eq (α := MvPolynomial σ R)
    ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f))) :
      MvPolynomial σ R)
    ((map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
succ₁ :
  Eq (α := MvPolynomial σ R)
    ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f))) :
      MvPolynomial σ R)
    ((map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand (p * p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
succ₂ :
  Eq (α := MvPolynomial σ R)
    ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f))) :
      MvPolynomial σ R)
    ((map (iterateFrobenius R p (1 + k)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand (p * p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
⊢ HPow.hPow (α := MvPolynomial σ R)
      ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
        MvPolynomial σ R)
      p =
    (map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f)
have succ₃ : Eq (α := MvPolynomial σ R)
  ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f))) :
    MvPolynomial σ R)
  ((map (RingHom.comp (iterateFrobenius R p 1) (iterateFrobenius R p k)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p * p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
    MvPolynomial σ R)
Tactic: simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : MvPolynomial σ R
n : ℕ
⊢ (map (iterateFrobenius R p n) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ n) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ p ^ n
have zero : (map (iterateFrobenius R p 0) : (a : MvPolynomial σ R) → MvPolynomial σ R)
    ((expand (HPow.hPow (β := ℕ) p 0) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
  f ^ HPow.hPow (β := ℕ) p 0
Tactic: induction n with
  | zero => simp [map_id]
  | succ k n_ih =>
    symm
    conv_lhs => rw [pow_succ, pow_mul, ← n_ih]
    simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : MvPolynomial σ R
n : ℕ
zero :
  (map (iterateFrobenius R p 0) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (HPow.hPow (β := ℕ) p 0) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ HPow.hPow (β := ℕ) p 0
⊢ (map (iterateFrobenius R p n) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ n) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ p ^ n
have succ : ∀ (k : ℕ)
  (n_ih :
    (map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
      f ^ p ^ k),
  (map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ p ^ (k + 1)
Tactic: induction n with
  | zero => simp [map_id]
  | succ k n_ih =>
    symm
    conv_lhs => rw [pow_succ, pow_mul, ← n_ih]
    simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.FreeCommRing (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }
⊢ (fun (p : (i : ι) × ↥(monoms i) → R) ↦
        (Subtype.mk (p := fun (p : ι → MvPolynomial κ R) ↦ ∀ (i : ι), (p i).support ⊆ monoms i)
            (fun (i : ι) ↦
              {
                support :=
                  {m ∈ monoms i |
                    ∃ (hm : m ∈ monoms i),
                      p
                          (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                            (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm)) ≠
                        0},
                toFun := fun (m : κ →₀ ℕ) ↦
                  if hm : m ∈ monoms i then
                    p
                      (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                        (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm))
                  else 0,
                mem_support_toFun := ⋯ })
            ⋯ :
          { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }))
      ((fun (p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }) (i : (i : ι) × ↥(monoms i)) ↦
          coeff (↑(i.snd (β := fun (i : ι) ↦ ↥(monoms i))) : κ →₀ ℕ)
            ((↑p : ι → MvPolynomial κ R) (i.fst (β := fun (i : ι) ↦ ↥(monoms i)))))
        p) =
    p
have a : ∀ (i : ι) (m : κ →₀ ℕ),
  coeff m
      ((↑((fun (p : (i : ι) × ↥(monoms i) → R) ↦
                (Subtype.mk (p := fun (p : ι → MvPolynomial κ R) ↦ ∀ (i : ι), (p i).support ⊆ monoms i)
                    (fun (i : ι) ↦
                      {
                        support :=
                          {m ∈ monoms i |
                            ∃ (hm : m ∈ monoms i),
                              p
                                  (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                                    (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm)) ≠
                                0},
                        toFun := fun (m : κ →₀ ℕ) ↦
                          if hm : m ∈ monoms i then
                            p
                              (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                                (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm))
                          else 0,
                        mem_support_toFun := sorry })
                    sorry :
                  { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }))
              ((fun (p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i })
                    (i : (i : ι) × ↥(monoms i)) ↦
                  coeff (↑(i.snd (β := fun (i : ι) ↦ ↥(monoms i))) : κ →₀ ℕ)
                    ((↑p : ι → MvPolynomial κ R) (i.fst (β := fun (i : ι) ↦ ↥(monoms i)))))
                p)) :
          ι → MvPolynomial κ R)
        i) =
    coeff m ((↑p : ι → MvPolynomial κ R) i)
Tactic: ext i m
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.FreeCommRing (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }
i : ι
m : κ →₀ ℕ
⊢ coeff m
      ((↑((fun (p : (i : ι) × ↥(monoms i) → R) ↦
                (Subtype.mk (p := fun (p : ι → MvPolynomial κ R) ↦ ∀ (i : ι), (p i).support ⊆ monoms i)
                    (fun (i : ι) ↦
                      {
                        support :=
                          {m ∈ monoms i |
                            ∃ (hm : m ∈ monoms i),
                              p
                                  (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                                    (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm)) ≠
                                0},
                        toFun := fun (m : κ →₀ ℕ) ↦
                          if hm : m ∈ monoms i then
                            p
                              (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                                (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm))
                          else 0,
                        mem_support_toFun := ⋯ })
                    ⋯ :
                  { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }))
              ((fun (p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i })
                    (i : (i : ι) × ↥(monoms i)) ↦
                  coeff (↑(i.snd (β := fun (i : ι) ↦ ↥(monoms i))) : κ →₀ ℕ)
                    ((↑p : ι → MvPolynomial κ R) (i.fst (β := fun (i : ι) ↦ ↥(monoms i)))))
                p)) :
          ι → MvPolynomial κ R)
        i) =
    coeff m ((↑p : ι → MvPolynomial κ R) i)
have a : m ∉ monoms i → Eq.{u_3 + 1} (α := R) (0 : R) (((↑p : ι → MvPolynomial κ R) i : (a : κ →₀ ℕ) → R) m : R)
Tactic: simp only [coeff, ne_eq, exists_prop, dite_eq_ite, Finsupp.coe_mk, ite_eq_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.FreeCommRing (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }
i : ι
m : κ →₀ ℕ
hm : m ∉ monoms i
⊢ Eq.{u_3 + 1} (α := R) (0 : R) (((↑p : ι → MvPolynomial κ R) i : (a : κ →₀ ℕ) → R) m : R)
have this : m ∉ ((↑p : ι → MvPolynomial κ R) i).support
Tactic: have : m ∉ (p.1 i).support := fun h => hm (p.2 i h)