-- 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
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₁ 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:
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

Premises used: Subtype.map, MvPolynomial.rename_rename, true_or, MvPolynomial.X, map_add, id, Finset.mem_insert, MvPolynomial.induction_on, map_mul, MvPolynomial.rename, Finset.mem_union, MvPolynomial.rename_X, forall_true_iff, or_true, DFunLike.coe, rfl