-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem exists_fin_rename (p : MvPolynomial σ R) :
    ∃ (n : ℕ) (f : Fin n → σ) (_hf : Injective f) (q : MvPolynomial (Fin n) R), p = rename f q

Proof state:
case intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
⊢ ∃ n f, ∃ (_ : Injective f), ∃ q_1, (rename Subtype.val) q = (rename f) q_1

Tactic:
let e := Fintype.equivFin { x // x ∈ s }

Result:
case intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
e : { x // x ∈ s } ≃ Fin (Fintype.card { x // x ∈ s }) := Fintype.equivFin { x // x ∈ s }
⊢ ∃ n f, ∃ (_ : Injective f), ∃ q_1, (rename Subtype.val) q = (rename f) q_1

Proof state:
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∃ n f, ∃ (_ : Injective f), ∃ q, p = (rename f) q

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

Result:
case intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
⊢ ∃ n f, ∃ (_ : Injective f), ∃ q_1, (rename Subtype.val) q = (rename f) q_1

Proof state:
case intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
⊢ ∃ n f, ∃ (_ : Injective f), ∃ q_1, (rename Subtype.val) q = (rename f) q_1

Tactic:
let n := Fintype.card { x // x ∈ s }

Result:
case intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
⊢ ∃ n f, ∃ (_ : Injective f), ∃ q_1, (rename Subtype.val) q = (rename f) q_1

Proof state:
case intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
e : { x // x ∈ s } ≃ Fin (Fintype.card { x // x ∈ s }) := Fintype.equivFin { x // x ∈ s }
⊢ (rename Subtype.val) q = (rename Subtype.val) ((rename (⇑e.symm ∘ ⇑e)) q)

Tactic:
simp only [Function.comp_def, Equiv.symm_apply_apply, rename_rename]

Result:
no goals

Proof state:
case intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
e : { x // x ∈ s } ≃ Fin (Fintype.card { x // x ∈ s }) := Fintype.equivFin { x // x ∈ s }
⊢ ∃ n f, ∃ (_ : Injective f), ∃ q_1, (rename Subtype.val) q = (rename f) q_1

Tactic:
refine ⟨n, (↑) ∘ e.symm, Subtype.val_injective.comp e.symm.injective, rename e q, ?_⟩

Result:
case intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
e : { x // x ∈ s } ≃ Fin (Fintype.card { x // x ∈ s }) := Fintype.equivFin { x // x ∈ s }
⊢ (rename Subtype.val) q = (rename (Subtype.val ∘ ⇑e.symm)) ((rename ⇑e) q)

Proof state:
case intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
e : { x // x ∈ s } ≃ Fin (Fintype.card { x // x ∈ s }) := Fintype.equivFin { x // x ∈ s }
⊢ (rename Subtype.val) q = (rename (Subtype.val ∘ ⇑e.symm)) ((rename ⇑e) q)

Tactic:
rw [← rename_rename, rename_rename e]

Result:
case intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
e : { x // x ∈ s } ≃ Fin (Fintype.card { x // x ∈ s }) := Fintype.equivFin { x // x ∈ s }
⊢ (rename Subtype.val) q = (rename Subtype.val) ((rename (⇑e.symm ∘ ⇑e)) q)