awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
p_1 q : MvPolynomial σ R
h :
  Eq (α := MvPolynomial (τ × σ) R)
    ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ C g p_1) : MvPolynomial (τ × σ) R)
    (eval₂ C (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x)) p_1 :
      MvPolynomial (τ × σ) R)
h_1 :
  Eq (α := MvPolynomial (τ × σ) R)
    ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ C g q) : MvPolynomial (τ × σ) R)
    (eval₂ 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₂ C g (p_1 + q)) :
      MvPolynomial (τ × σ) R)
    (eval₂ C (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x)) (p_1 + q) :
      MvPolynomial (τ × σ) R)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
p_1 : MvPolynomial σ R
n : σ
h :
  Eq (α := MvPolynomial (τ × σ) R)
    ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ C g p_1) : MvPolynomial (τ × σ) R)
    (eval₂ C (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x)) p_1 :
      MvPolynomial (τ × σ) R)
⊢ Eq (α := MvPolynomial (τ × σ) R)
    ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ C g (p_1 * X n)) :
      MvPolynomial (τ × σ) R)
    (eval₂ C (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x)) (p_1 * X n) :
      MvPolynomial (τ × σ) R)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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)
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)
⊢ eval₂ f g ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R) p) =
    eval₂ f (fun (j : τ) ↦ g (i, j)) p

Tactic:
apply MvPolynomial.induction_on p

Premises used: MvPolynomial.induction_on
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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
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:
simp [*]
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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 p_1 q : MvPolynomial τ R
h :
  eval₂ f g ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R) p_1) =
    eval₂ f (fun (j : τ) ↦ g (i, j)) p_1
h_1 :
  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_1 + q)) =
    eval₂ f (fun (j : τ) ↦ g (i, j)) (p_1 + q)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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 p_1 : MvPolynomial τ R
n : τ
h :
  eval₂ f g ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R) p_1) =
    eval₂ f (fun (j : τ) ↦ g (i, j)) p_1
⊢ eval₂ f g ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R) (p_1 * X n)) =
    eval₂ f (fun (j : τ) ↦ g (i, j)) (p_1 * X n)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
g : σ × τ → R
i : σ
p : MvPolynomial τ R
⊢ Eq.{u_4 + 1} (α := R)
    ((eval g : (a : MvPolynomial (σ × τ) R) → R)
        ((rename (Prod.mk i) : (a : MvPolynomial τ R) → MvPolynomial (σ × τ) R) p : MvPolynomial (σ × τ) R) :
      R)
    ((eval fun (j : τ) ↦ g (i, j) : (a : MvPolynomial τ R) → R) p : R)

Tactic:
eval₂_rename_prod_mk (RingHom.id _) _ _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.eval₂_rename_prod_mk, RingHom.id, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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
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
⊢ ∃ (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

Tactic:
apply induction_on p

Premises used: MvPolynomial.induction_on
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
r : R
rw rw₁ :
  Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ 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)

Tactic:
rw [rename_C]

Premises used: MvPolynomial.rename_C
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
r : R
⊢ ∃ (s : Finset σ) (q : MvPolynomial.{u_1, u_4} (↥s) R),
    Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q :
        MvPolynomial σ R)

Tactic:
exact ⟨∅, C r, by rw [rename_C]⟩
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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

Tactic:
⟨s ∪ t, ⟨?_, ?_⟩⟩

Premises used: Exists.intro, Union.union
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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
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 ⋯) :
              (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))
⊢ ∃ (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

Tactic:
refine ⟨s ∪ t, ⟨?_, ?_⟩⟩
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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
add₁ : ∀ a ∈ t, id a ∈ s ∪ t
⊢ MvPolynomial.{u_1, u_4} (↥(s ∪ t)) R

Tactic:
refine rename (Subtype.map id ?_) p + rename (Subtype.map id ?_) q

Premises used: Subtype.map, id, MvPolynomial.rename, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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
⊢ ∀ a ∈ s, id a ∈ s ∪ t

Tactic:
simp +contextual only [id, true_or, or_true,
          Finset.mem_union, forall_true_iff]

Premises used: true_or, id, Finset.mem_union, forall_true_iff, or_true
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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
⊢ ∀ a ∈ t, id a ∈ s ∪ t

Tactic:
simp +contextual only [id, true_or, or_true,
          Finset.mem_union, forall_true_iff]

Premises used: true_or, id, Finset.mem_union, forall_true_iff, or_true
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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 :
  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 ⋯)) :
            (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 ⋯)) :
            (a : MvPolynomial (↥t) R) → MvPolynomial σ R)
          q :
        MvPolynomial σ 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))

Tactic:
simp only [rename_rename, map_add]

Premises used: MvPolynomial.rename_rename, map_add
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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) =
    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 ⋯)) :
            (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 ⋯)) :
            (a : MvPolynomial (↥t) R) → MvPolynomial σ R)
          q :
        MvPolynomial σ R)

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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

Tactic:
⟨insert n s, ⟨?_, ?_⟩⟩

Premises used: Insert.insert, Exists.intro
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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
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 ⋯) :
              (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 ⋯)))
⊢ ∃ (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

Tactic:
refine ⟨insert n s, ⟨?_, ?_⟩⟩
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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 : ∀ a ∈ s, id a ∈ insert n s
⊢ MvPolynomial.{u_1, u_4} (↥(insert n s)) R

Tactic:
refine rename (Subtype.map id ?_) p * X ⟨n, s.mem_insert_self n⟩

Premises used: Subtype.map, MvPolynomial.X, id, MvPolynomial.rename, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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
⊢ ∀ a ∈ s, id a ∈ insert n s

Tactic:
simp +contextual only [id, or_true, Finset.mem_insert, forall_true_iff]

Premises used: id, Finset.mem_insert, forall_true_iff, or_true
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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 :
  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 ⋯)) :
            (a : MvPolynomial (↥s) R) → MvPolynomial σ R)
          p :
        MvPolynomial σ R)
      (X n)
⊢ 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 ⋯)))

Tactic:
simp only [rename_rename, rename_X, map_mul]

Premises used: MvPolynomial.rename_rename, map_mul, MvPolynomial.rename_X
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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) =
    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 ⋯)) :
            (a : MvPolynomial (↥s) R) → MvPolynomial σ R)
          p :
        MvPolynomial σ R)
      (X n)

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p₁ p₂ : MvPolynomial σ R
obtain :
  ∀ (s₁ : Finset σ) (q₁ : MvPolynomial.{u_1, u_4} (↥s₁) R),
    ∃ (s : Finset σ) (q₁_1 : MvPolynomial.{u_1, u_4} (↥s) R) (q₂ : MvPolynomial.{u_1, u_4} (↥s) R),
      Eq (α := MvPolynomial σ R)
          ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁)) : (a : MvPolynomial (↥s₁) R) → MvPolynomial σ R) q₁ :
            MvPolynomial σ R)
          ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q₁_1 :
            MvPolynomial σ 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) (q₂ : MvPolynomial.{u_1, u_4} (↥s) R),
    p₁ = (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q₁ ∧
      p₂ = (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q₂

Tactic:
obtain ⟨s₁, q₁, rfl⟩ := exists_finset_rename p₁

Premises used: MvPolynomial.exists_finset_rename, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p₂ : MvPolynomial σ R
s₁ : Finset σ
q₁ : MvPolynomial.{u_1, u_4} (↥s₁) R
obtain :
  ∀ (s₂ : Finset σ) (q₂ : MvPolynomial.{u_1, u_4} (↥s₂) R),
    ∃ (s : Finset σ) (q₁_1 : MvPolynomial.{u_1, u_4} (↥s) R) (q₂_1 : MvPolynomial.{u_1, u_4} (↥s) R),
      Eq (α := MvPolynomial σ R)
          ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁)) : (a : MvPolynomial (↥s₁) R) → MvPolynomial σ R) q₁ :
            MvPolynomial σ R)
          ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q₁_1 :
            MvPolynomial σ R) ∧
        Eq (α := MvPolynomial σ R)
          ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₂)) : (a : MvPolynomial (↥s₂) R) → MvPolynomial σ R) q₂ :
            MvPolynomial σ R)
          ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q₂_1 :
            MvPolynomial σ R)
⊢ ∃ (s : Finset σ) (q₁_1 : MvPolynomial.{u_1, u_4} (↥s) R) (q₂ : MvPolynomial.{u_1, u_4} (↥s) R),
    Eq (α := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s₁)) : (a : MvPolynomial (↥s₁) R) → MvPolynomial σ R) q₁ :
          MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q₁_1 :
          MvPolynomial σ R) ∧
      p₂ = (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q₂

Tactic:
obtain ⟨s₂, q₂, rfl⟩ := exists_finset_rename p₂

Premises used: MvPolynomial.exists_finset_rename, rfl