awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
C :
  ∀ (a : R),
    Eq (α := MvPolynomial (τ × σ) R)
      ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R)
          (eval₂ MvPolynomial.C g ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        MvPolynomial (τ × σ) R)
      (eval₂ MvPolynomial.C (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x))
          ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) :
        MvPolynomial (τ × σ) R)
⊢ Eq (α := MvPolynomial (τ × σ) R)
    ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ MvPolynomial.C g p) :
      MvPolynomial (τ × σ) R)
    (eval₂ MvPolynomial.C (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x))
        p :
      MvPolynomial (τ × σ) R)
have add : ∀ (p q : MvPolynomial σ R),
  Eq (α := MvPolynomial (τ × σ) R)
      ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ MvPolynomial.C g p) :
        MvPolynomial (τ × σ) R)
      (eval₂ MvPolynomial.C (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x))
          p :
        MvPolynomial (τ × σ) R) →
    Eq (α := MvPolynomial (τ × σ) R)
        ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ MvPolynomial.C g q) :
          MvPolynomial (τ × σ) R)
        (eval₂ MvPolynomial.C
            (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x)) q :
          MvPolynomial (τ × σ) R) →
      Eq (α := MvPolynomial (τ × σ) R)
        ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ MvPolynomial.C g (p + q)) :
          MvPolynomial (τ × σ) R)
        (eval₂ MvPolynomial.C
            (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x)) (p + q) :
          MvPolynomial (τ × σ) R)
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
C :
  ∀ (a : R),
    Eq (α := MvPolynomial (τ × σ) R)
      ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R)
          (eval₂ MvPolynomial.C g ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        MvPolynomial (τ × σ) R)
      (eval₂ MvPolynomial.C (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x))
          ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) :
        MvPolynomial (τ × σ) R)
add :
  ∀ (p q : MvPolynomial σ R),
    Eq (α := MvPolynomial (τ × σ) R)
        ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ MvPolynomial.C g p) :
          MvPolynomial (τ × σ) R)
        (eval₂ MvPolynomial.C
            (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x)) p :
          MvPolynomial (τ × σ) R) →
      Eq (α := MvPolynomial (τ × σ) R)
          ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ MvPolynomial.C g q) :
            MvPolynomial (τ × σ) R)
          (eval₂ MvPolynomial.C
              (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x)) q :
            MvPolynomial (τ × σ) R) →
        Eq (α := MvPolynomial (τ × σ) R)
          ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ MvPolynomial.C g (p + q)) :
            MvPolynomial (τ × σ) R)
          (eval₂ MvPolynomial.C
              (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x)) (p + q) :
            MvPolynomial (τ × σ) R)
⊢ Eq (α := MvPolynomial (τ × σ) R)
    ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ MvPolynomial.C g p) :
      MvPolynomial (τ × σ) R)
    (eval₂ MvPolynomial.C (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x))
        p :
      MvPolynomial (τ × σ) R)
have mul_X : ∀ (p : MvPolynomial σ R) (n : σ),
  Eq (α := MvPolynomial (τ × σ) R)
      ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ MvPolynomial.C g p) :
        MvPolynomial (τ × σ) R)
      (eval₂ MvPolynomial.C (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x))
          p :
        MvPolynomial (τ × σ) R) →
    Eq (α := MvPolynomial (τ × σ) R)
      ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ MvPolynomial.C g (p * X n)) :
        MvPolynomial (τ × σ) R)
      (eval₂ MvPolynomial.C (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x))
          (p * X n) :
        MvPolynomial (τ × σ) R)
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ eval₂ f g ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R) p) =
    eval₂ f (fun (j : τ) ↦ g (i, j)) p
have C : ∀ (a : R),
  eval₂ f g
      ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R) ((C : (a : R) → MvPolynomial τ R) a)) =
    eval₂ f (fun (j : τ) ↦ g (i, j)) ((C : (a : R) → MvPolynomial τ R) a)
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p : MvPolynomial τ R
C :
  ∀ (a : R),
    eval₂ f g
        ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R)
          ((MvPolynomial.C : (a : R) → MvPolynomial τ R) a)) =
      eval₂ f (fun (j : τ) ↦ g (i, j)) ((MvPolynomial.C : (a : R) → MvPolynomial τ R) a)
⊢ eval₂ f g ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R) p) =
    eval₂ f (fun (j : τ) ↦ g (i, j)) p
have add : ∀ (p q : MvPolynomial τ R),
  eval₂ f g ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R) p) =
      eval₂ f (fun (j : τ) ↦ g (i, j)) p →
    eval₂ f g ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R) q) =
        eval₂ f (fun (j : τ) ↦ g (i, j)) q →
      eval₂ f g ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R) (p + q)) =
        eval₂ f (fun (j : τ) ↦ g (i, j)) (p + q)
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p : MvPolynomial τ R
C :
  ∀ (a : R),
    eval₂ f g
        ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R)
          ((MvPolynomial.C : (a : R) → MvPolynomial τ R) a)) =
      eval₂ f (fun (j : τ) ↦ g (i, j)) ((MvPolynomial.C : (a : R) → MvPolynomial τ R) a)
add :
  ∀ (p q : MvPolynomial τ R),
    eval₂ f g ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R) p) =
        eval₂ f (fun (j : τ) ↦ g (i, j)) p →
      eval₂ f g ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R) q) =
          eval₂ f (fun (j : τ) ↦ g (i, j)) q →
        eval₂ f g ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R) (p + q)) =
          eval₂ f (fun (j : τ) ↦ g (i, j)) (p + q)
⊢ eval₂ f g ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R) p) =
    eval₂ f (fun (j : τ) ↦ g (i, j)) p
have mul_X : ∀ (p : MvPolynomial τ R) (n : τ),
  eval₂ f g ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R) p) =
      eval₂ f (fun (j : τ) ↦ g (i, j)) p →
    eval₂ f g ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R) (p * X n)) =
      eval₂ f (fun (j : τ) ↦ g (i, j)) (p * X n)
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
⊢ ∃ (s : Finset σ) (q : MvPolynomial.{u_1, u_4} (↥s) R),
    p = (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q
have C : ∀ (a : R),
  ∃ (s : Finset σ) (q : MvPolynomial.{u_1, u_4} (↥s) R),
    Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q :
        MvPolynomial σ R)
Tactic: apply induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
C :
  ∀ (a : R),
    ∃ (s : Finset σ) (q : MvPolynomial.{u_1, u_4} (↥s) R),
      Eq (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q :
          MvPolynomial σ R)
⊢ ∃ (s : Finset σ) (q : MvPolynomial.{u_1, u_4} (↥s) R),
    p = (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q
have add : ∀ (p q : MvPolynomial σ R),
  (∃ (s : Finset σ) (q : MvPolynomial.{u_1, u_4} (↥s) R),
      p = (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q) →
    (∃ (s : Finset σ) (q_1 : MvPolynomial.{u_1, u_4} (↥s) R),
        q = (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q_1) →
      ∃ (s : Finset σ) (q_1 : MvPolynomial.{u_1, u_4} (↥s) R),
        p + q = (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q_1
Tactic: apply induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
C :
  ∀ (a : R),
    ∃ (s : Finset σ) (q : MvPolynomial.{u_1, u_4} (↥s) R),
      Eq (α := MvPolynomial σ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q :
          MvPolynomial σ R)
add :
  ∀ (p q : MvPolynomial σ R),
    (∃ (s : Finset σ) (q : MvPolynomial.{u_1, u_4} (↥s) R),
        p = (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q) →
      (∃ (s : Finset σ) (q_1 : MvPolynomial.{u_1, u_4} (↥s) R),
          q = (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q_1) →
        ∃ (s : Finset σ) (q_1 : MvPolynomial.{u_1, u_4} (↥s) R),
          p + q = (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q_1
⊢ ∃ (s : Finset σ) (q : MvPolynomial.{u_1, u_4} (↥s) R),
    p = (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q
have mul_X : ∀ (p : MvPolynomial σ R) (n : σ),
  (∃ (s : Finset σ) (q : MvPolynomial.{u_1, u_4} (↥s) R),
      p = (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q) →
    ∃ (s : Finset σ) (q : MvPolynomial.{u_1, u_4} (↥s) R),
      p * X n = (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q
Tactic: apply induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
r : R
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ Membership.mem (γ := Finset σ) ∅ x)) :
          (a : MvPolynomial (↥∅) R) → MvPolynomial σ R)
        ((C : (a : R) → MvPolynomial (↥∅) R) r) :
      MvPolynomial σ R)
have rw : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
  ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
Tactic: rw [rename_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p_1 : MvPolynomial σ R
s : Finset σ
p : MvPolynomial.{u_1, u_4} (↥s) R
t : Finset σ
q : MvPolynomial.{u_1, u_4} (↥t) R
⊢ ∃ (s_1 : Finset σ) (q_1 : MvPolynomial.{u_1, u_4} (↥s_1) R),
    HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) p :
          MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ t)) : (a : MvPolynomial (↥t) R) → MvPolynomial σ R) q :
          MvPolynomial σ R) =
      (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s_1)) : (a : MvPolynomial (↥s_1) R) → MvPolynomial σ R) q_1
have add : MvPolynomial.{u_1, u_4} (↥(s ∪ t)) R
Tactic: refine ⟨s ∪ t, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p_1 : MvPolynomial σ R
s : Finset σ
p : MvPolynomial.{u_1, u_4} (↥s) R
t : Finset σ
q : MvPolynomial.{u_1, u_4} (↥t) R
add : MvPolynomial.{u_1, u_4} (↥(s ∪ t)) R
⊢ ∃ (s_1 : Finset σ) (q_1 : MvPolynomial.{u_1, u_4} (↥s_1) R),
    HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) p :
          MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ t)) : (a : MvPolynomial (↥t) R) → MvPolynomial σ R) q :
          MvPolynomial σ R) =
      (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s_1)) : (a : MvPolynomial (↥s_1) R) → MvPolynomial σ R) q_1
have add₁ : HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) p :
      MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ t)) : (a : MvPolynomial (↥t) R) → MvPolynomial σ R) q :
      MvPolynomial σ R) =
  (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s ∪ t)) : (a : MvPolynomial (↥(s ∪ t)) R) → MvPolynomial σ R)
    (HAdd.hAdd (α := MvPolynomial.{u_1, u_4} (↥(s ∪ t)) R) (β := MvPolynomial.{u_1, u_4} (↥(s ∪ t)) R)
      ((rename (Subtype.map (p := fun (x : σ) ↦ x ∈ s) (q := fun (x : σ) ↦ x ∈ s ∪ t) id sorry) :
            (a : MvPolynomial (↥s) R) → MvPolynomial (↥(s ∪ t)) R)
          p :
        MvPolynomial.{u_1, u_4} (↥(s ∪ t)) R)
      ((rename (Subtype.map (p := fun (x : σ) ↦ x ∈ t) (q := fun (x : σ) ↦ x ∈ s ∪ t) id sorry) :
            (a : MvPolynomial (↥t) R) → MvPolynomial (↥(s ∪ t)) R)
          q :
        MvPolynomial.{u_1, u_4} (↥(s ∪ t)) R))
Tactic: refine ⟨s ∪ t, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p_1 : MvPolynomial σ R
s : Finset σ
p : MvPolynomial.{u_1, u_4} (↥s) R
t : Finset σ
q : MvPolynomial.{u_1, u_4} (↥t) R
⊢ MvPolynomial.{u_1, u_4} (↥(s ∪ t)) R
have add : ∀ a ∈ s, id a ∈ s ∪ t
Tactic: refine rename (Subtype.map id ?_) p + rename (Subtype.map id ?_) q
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p_1 : MvPolynomial σ R
s : Finset σ
p : MvPolynomial.{u_1, u_4} (↥s) R
t : Finset σ
q : MvPolynomial.{u_1, u_4} (↥t) R
add : ∀ a ∈ s, id a ∈ s ∪ t
⊢ MvPolynomial.{u_1, u_4} (↥(s ∪ t)) R
have add₁ : ∀ a ∈ t, id a ∈ s ∪ t
Tactic: refine rename (Subtype.map id ?_) p + rename (Subtype.map id ?_) q
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p_1 : MvPolynomial σ R
s : Finset σ
p : MvPolynomial.{u_1, u_4} (↥s) R
t : Finset σ
q : MvPolynomial.{u_1, u_4} (↥t) R
⊢ HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) p :
        MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ t)) : (a : MvPolynomial (↥t) R) → MvPolynomial σ R) q :
        MvPolynomial σ R) =
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s ∪ t)) : (a : MvPolynomial (↥(s ∪ t)) R) → MvPolynomial σ R)
      (HAdd.hAdd (α := MvPolynomial.{u_1, u_4} (↥(s ∪ t)) R) (β := MvPolynomial.{u_1, u_4} (↥(s ∪ t)) R)
        ((rename (Subtype.map (p := fun (x : σ) ↦ x ∈ s) (q := fun (x : σ) ↦ x ∈ s ∪ t) id ⋯) :
              (a : MvPolynomial (↥s) R) → MvPolynomial (↥(s ∪ t)) R)
            p :
          MvPolynomial.{u_1, u_4} (↥(s ∪ t)) R)
        ((rename (Subtype.map (p := fun (x : σ) ↦ x ∈ t) (q := fun (x : σ) ↦ x ∈ s ∪ t) id ⋯) :
              (a : MvPolynomial (↥t) R) → MvPolynomial (↥(s ∪ t)) R)
            q :
          MvPolynomial.{u_1, u_4} (↥(s ∪ t)) R))
have add : HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) p :
      MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ t)) : (a : MvPolynomial (↥t) R) → MvPolynomial σ R) q :
      MvPolynomial σ R) =
  HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((rename
            (comp (β := ↥(s ∪ t)) (Subtype.val (p := fun (x : σ) ↦ x ∈ s ∪ t))
              (Subtype.map (p := fun (x : σ) ↦ x ∈ s) (q := fun (x : σ) ↦ x ∈ s ∪ t) id sorry)) :
          (a : MvPolynomial (↥s) R) → MvPolynomial σ R)
        p :
      MvPolynomial σ R)
    ((rename
            (comp (β := ↥(s ∪ t)) (Subtype.val (p := fun (x : σ) ↦ x ∈ s ∪ t))
              (Subtype.map (p := fun (x : σ) ↦ x ∈ t) (q := fun (x : σ) ↦ x ∈ s ∪ t) id sorry)) :
          (a : MvPolynomial (↥t) R) → MvPolynomial σ R)
        q :
      MvPolynomial σ R)
Tactic: simp only [rename_rename, map_add]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p_1 : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial.{u_1, u_4} (↥s) R
⊢ ∃ (s_1 : Finset σ) (q : MvPolynomial.{u_1, u_4} (↥s_1) R),
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) p :
          MvPolynomial σ R)
        (X n) =
      (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s_1)) : (a : MvPolynomial (↥s_1) R) → MvPolynomial σ R) q
have mul_X : MvPolynomial.{u_1, u_4} (↥(insert n s)) R
Tactic: refine ⟨insert n s, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p_1 : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial.{u_1, u_4} (↥s) R
mul_X : MvPolynomial.{u_1, u_4} (↥(insert n s)) R
⊢ ∃ (s_1 : Finset σ) (q : MvPolynomial.{u_1, u_4} (↥s_1) R),
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) p :
          MvPolynomial σ R)
        (X n) =
      (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s_1)) : (a : MvPolynomial (↥s_1) R) → MvPolynomial σ R) q
have mul_X₁ : HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) p :
      MvPolynomial σ R)
    (X n) =
  (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ insert n s)) : (a : MvPolynomial (↥(insert n s)) R) → MvPolynomial σ R)
    (HMul.hMul (α := MvPolynomial.{u_1, u_4} (↥(insert n s)) R) (β := MvPolynomial.{u_1, u_4} (↥(insert n s)) R)
      ((rename (Subtype.map (p := fun (x : σ) ↦ x ∈ s) (q := fun (x : σ) ↦ x ∈ insert n s) id sorry) :
            (a : MvPolynomial (↥s) R) → MvPolynomial (↥(insert n s)) R)
          p :
        MvPolynomial.{u_1, u_4} (↥(insert n s)) R)
      (X (Subtype.mk (p := fun (x : σ) ↦ x ∈ insert n s) n sorry)))
Tactic: refine ⟨insert n s, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p_1 : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial.{u_1, u_4} (↥s) R
⊢ MvPolynomial.{u_1, u_4} (↥(insert n s)) R
have mul_X : ∀ a ∈ s, id a ∈ insert n s
Tactic: refine rename (Subtype.map id ?_) p * X ⟨n, s.mem_insert_self n⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p_1 : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial.{u_1, u_4} (↥s) R
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) p :
        MvPolynomial σ R)
      (X n) =
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ insert n s)) : (a : MvPolynomial (↥(insert n s)) R) → MvPolynomial σ R)
      (HMul.hMul (α := MvPolynomial.{u_1, u_4} (↥(insert n s)) R) (β := MvPolynomial.{u_1, u_4} (↥(insert n s)) R)
        ((rename (Subtype.map (p := fun (x : σ) ↦ x ∈ s) (q := fun (x : σ) ↦ x ∈ insert n s) id ⋯) :
              (a : MvPolynomial (↥s) R) → MvPolynomial (↥(insert n s)) R)
            p :
          MvPolynomial.{u_1, u_4} (↥(insert n s)) R)
        (X (Subtype.mk (p := fun (x : σ) ↦ x ∈ insert n s) n ⋯)))
have mul_X : HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) p :
      MvPolynomial σ R)
    (X n) =
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((rename
            (comp (β := ↥(insert n s)) (Subtype.val (p := fun (x : σ) ↦ x ∈ insert n s))
              (Subtype.map (p := fun (x : σ) ↦ x ∈ s) (q := fun (x : σ) ↦ x ∈ insert n s) id sorry)) :
          (a : MvPolynomial (↥s) R) → MvPolynomial σ R)
        p :
      MvPolynomial σ R)
    (X n)
Tactic: simp only [rename_rename, rename_X, map_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
⊢ ∃ (s : Finset σ) (q : MvPolynomial.{u_1, u_4} (↥s) R),
    p = (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q
have C : ∀ (a : R),
  ∃ (s : Finset σ) (q : MvPolynomial.{u_1, u_4} (↥s) R),
    Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q :
        MvPolynomial σ R)
Tactic: classical
  apply induction_on p
  · intro r
    exact ⟨∅, C r, by rw [rename_C]⟩
  · rintro p q ⟨s, p, rfl⟩ ⟨t, q, rfl⟩
    refine ⟨s ∪ t, ⟨?_, ?_⟩⟩
    · refine rename (Subtype.map id ?_) p + rename (Subtype.map id ?_) q <;>
        simp +contextual only [id, true_or, or_true,
          Finset.mem_union, forall_true_iff]
    · simp only [rename_rename, map_add]
      rfl
  · rintro p n ⟨s, p, rfl⟩
    refine ⟨insert n s, ⟨?_, ?_⟩⟩
    · refine rename (Subtype.map id ?_) p * X ⟨n, s.mem_insert_self n⟩
      simp +contextual only [id, or_true, Finset.mem_insert, forall_true_iff]
    · simp only [rename_rename, rename_X, map_mul]
      rfl