case intro.intro
σ : Type u_1
τ : Type ?u.859965
α : Type ?u.859968
R : Type u_2
S : Type ?u.859974
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
⊢ ∃ n f _hf q_1, ↑(rename Subtype.val) q = ↑(rename f) q_1
σ : Type u_1
τ : Type ?u.859965
α : Type ?u.859968
R : Type u_2
S : Type ?u.859974
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∃ n f _hf q, p = ↑(rename f) q
obtain ⟨s, q, rfl⟩ := exists_finset_rename p
case intro.intro
σ : Type u_1
τ : Type ?u.859965
α : Type ?u.859968
R : Type u_2
S : Type ?u.859974
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
⊢ ∃ n f _hf q_1, ↑(rename Subtype.val) q = ↑(rename f) q_1
case intro.intro
σ : Type u_1
τ : Type ?u.859965
α : Type ?u.859968
R : Type u_2
S : Type ?u.859974
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
⊢ ∃ n f _hf q_1, ↑(rename Subtype.val) q = ↑(rename f) q_1
let n := Fintype.card { x // x ∈ s }
case intro.intro
σ : Type u_1
τ : Type ?u.859965
α : Type ?u.859968
R : Type u_2
S : Type ?u.859974
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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 _hf q_1, ↑(rename Subtype.val) q = ↑(rename f) q_1
case intro.intro
σ : Type u_1
τ : Type ?u.859965
α : Type ?u.859968
R : Type u_2
S : Type ?u.859974
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
⊢ ∃ n f _hf q_1, ↑(rename Subtype.val) q = ↑(rename f) q_1
let e := Fintype.equivFin { x // x ∈ s }
case intro.intro
σ : Type u_1
τ : Type ?u.859965
α : Type ?u.859968
R : Type u_2
S : Type ?u.859974
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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)
case intro.intro
σ : Type u_1
τ : Type ?u.859965
α : Type ?u.859968
R : Type u_2
S : Type ?u.859974
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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 _hf q_1, ↑(rename Subtype.val) q = ↑(rename f) q_1
refine' ⟨n, (↑) ∘ e.symm, Subtype.val_injective.comp e.symm.injective, rename e q, _⟩
case intro.intro
σ : Type u_1
τ : Type ?u.859965
α : Type ?u.859968
R : Type u_2
S : Type ?u.859974
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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)
case intro.intro
σ : Type u_1
τ : Type ?u.859965
α : Type ?u.859968
R : Type u_2
S : Type ?u.859974
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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)
rw [← rename_rename, rename_rename e]
no goals
case intro.intro
σ : Type u_1
τ : Type ?u.859965
α : Type ?u.859968
R : Type u_2
S : Type ?u.859974
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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)
simp only [Function.comp, Equiv.symm_apply_apply, rename_rename]