awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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: 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
-- 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: 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
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p₁ p₂ : MvPolynomial σ R
⊢ ∃ (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₂
have 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₂
Tactic: obtain ⟨s₁, q₁, rfl⟩ := exists_finset_rename p₁
Cleared hypotheses: 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
⊢ ∃ (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₂
have 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)
Tactic: obtain ⟨s₂, q₂, rfl⟩ := exists_finset_rename p₂
Cleared hypotheses: p₂
-- 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
⊢ ∃ (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 : ∃ (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)
Tactic: use s₁ ∪ s₂
-- 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
⊢ ∃ (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)
have 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 : σ) 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)
          q₂_1 :
        MvPolynomial σ R)
Tactic: use rename (fun x ↦ ⟨x, Finset.subset_union_left x.2⟩) q₁
-- 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
⊢ ∃ (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)
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: use rename (fun x ↦ ⟨x, Finset.subset_union_right x.2⟩) q₂
-- 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
⊢ 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)
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)
Tactic: constructor
-- 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
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) ∧
    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)
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)
Tactic: constructor
-- 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 σ
⊢ ∃ (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 : ∃ (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)
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]
-- 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)
⊢ ∃ (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₂ : ∃ (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 : σ) 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)
          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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
⊢ ∃ (n : ℕ) (f : Fin n → σ) (_ : Injective f) (q : MvPolynomial (Fin n) R),
    p = (rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) q
have obtain : ∀ (s : Finset σ) (q : MvPolynomial.{u_1, u_4} (↥s) R),
  ∃ (n : ℕ) (f : Fin n → σ) (_ : Injective f) (q_1 : MvPolynomial (Fin n) R),
    Eq (α := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q :
        MvPolynomial σ R)
      ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) q_1 : MvPolynomial σ R)
Tactic: obtain ⟨s, q, rfl⟩ := exists_finset_rename p
Cleared hypotheses: p
-- 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
n : ℕ := Fintype.card.{u_1} ↥s
e : ↥s ≃ Fin (Fintype.card.{u_1} ↥s) := Fintype.equivFin ↥s
⊢ ∃ (n : ℕ) (f : Fin n → σ) (_ : Injective f) (q_1 : MvPolynomial (Fin n) R),
    Eq (α := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q :
        MvPolynomial σ R)
      ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) q_1 : MvPolynomial σ R)
have refine : Eq (α := MvPolynomial σ R)
  ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) q :
    MvPolynomial σ R)
  ((rename (comp (β := ↥s) (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) (⇑e.symm : (a : Fin (Fintype.card ↥s)) → ↥s)) :
        (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
      ((rename (⇑e : (a : ↥s) → Fin (Fintype.card ↥s)) :
          (a : MvPolynomial (↥s) R) → MvPolynomial (Fin (Fintype.card ↥s)) R)
        q) :
    MvPolynomial σ R)
Tactic: refine ⟨n, (↑) ∘ e.symm, Subtype.val_injective.comp e.symm.injective, rename e q, ?_⟩