-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
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)
⊢ ∃ (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)
have 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 : σ) sorry :
            (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 : σ) sorry :
            (a : MvPolynomial (↥s₂) R) → MvPolynomial (↥(s₁ ∪ s₂)) R)
          q₂) :
      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]