-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial.{u_1, u_4} (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial.{u_1, u_4} (↥s₂) R
w : Finset σ
h h₁ :
  ∃ (q₁_1 : MvPolynomial.{u_1, u_4} (↥(s₁ ∪ s₂)) R) (q₂_1 : MvPolynomial.{u_1, u_4} (↥(s₁ ∪ 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₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ 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₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
            q₂_1 :
          MvPolynomial σ R)
h₂ :
  ∃ (q₂_1 : MvPolynomial.{u_1, u_4} (↥(s₁ ∪ 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₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
            ((rename fun (x : ↥s₁) ↦ Subtype.mk (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂) (↑x : σ) ⋯ :
                (a : MvPolynomial (↥s₁) R) → MvPolynomial (↥(s₁ ∪ s₂)) R)
              q₁) :
          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₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
            q₂_1 :
          MvPolynomial σ R)
h₃ :
  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₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
          ((rename fun (x : ↥s₁) ↦ Subtype.mk (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂) (↑x : σ) ⋯ :
              (a : MvPolynomial (↥s₁) R) → MvPolynomial (↥(s₁ ∪ s₂)) R)
            q₁) :
        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₁ ∪ s₂)) : (a : MvPolynomial (↥(s₁ ∪ s₂)) R) → MvPolynomial σ R)
          ((rename fun (x : ↥s₂) ↦ Subtype.mk (p := fun (x : σ) ↦ x ∈ s₁ ∪ s₂) (↑x : σ) ⋯ :
              (a : MvPolynomial (↥s₂) R) → MvPolynomial (↥(s₁ ∪ s₂)) R)
            q₂) :
        MvPolynomial σ 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)

Tactic:
classical
    use s₁ ∪ s₂
    use rename (fun x ↦ ⟨x, Finset.subset_union_left x.2⟩) q₁
    use rename (fun x ↦ ⟨x, Finset.subset_union_right x.2⟩) q₂
    constructor <;> simp [Function.comp_def]

Premises used: Function.comp_def, MvPolynomial.rename, DFunLike.coe