-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem exists_finset_rename (p : MvPolynomial σ R) :
    ∃ (s : Finset σ) (q : MvPolynomial { x // x ∈ s } R), p = rename (↑) q

Proof state:
case h_X.intro.intro.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ (rename Subtype.val) p * X n = (rename Subtype.val) ((rename (Subtype.map id ⋯)) p * X ⟨n, ⋯⟩)

Tactic:
simp only [rename_rename, rename_X, Subtype.coe_mk, map_mul]

Result:
case h_X.intro.intro.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ (rename Subtype.val) p * X n = (rename (Subtype.val ∘ Subtype.map id ⋯)) p * X n

Proof state:
case h_X.intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ∃ s_1 q, (rename Subtype.val) p * X n = (rename Subtype.val) q

Tactic:
refine ⟨insert n s, ⟨?_, ?_⟩⟩

Result:
case h_X.intro.intro.refine_1
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ MvPolynomial { x // x ∈ insert n s } R

case h_X.intro.intro.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ (rename Subtype.val) p * X n = (rename Subtype.val) ?h_X.intro.intro.refine_1

Proof state:
case h_X.intro.intro.refine_1
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ∀ a ∈ s, id a ∈ insert n s

Tactic:
simp +contextual only [id, or_true, Finset.mem_insert, forall_true_iff]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
r : R
⊢ C r = (rename Subtype.val) (C r)

Tactic:
rw [rename_C]

Result:
no goals

Proof state:
case h_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ), (∃ s q, p = (rename Subtype.val) q) → ∃ s q, p * X n = (rename Subtype.val) q

Tactic:
rintro p n ⟨s, p, rfl⟩

Result:
case h_X.intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ∃ s_1 q, (rename Subtype.val) p * X n = (rename Subtype.val) q

Proof state:
case h_C
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (a : R), ∃ s q, C a = (rename Subtype.val) q

Tactic:
intro r

Result:
case h_C
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
r : R
⊢ ∃ s q, C r = (rename Subtype.val) q

Proof state:
case h_add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (∃ s q, p = (rename Subtype.val) q) →
      (∃ s q_1, q = (rename Subtype.val) q_1) → ∃ s q_1, p + q = (rename Subtype.val) q_1

Tactic:
rintro p q ⟨s, p, rfl⟩ ⟨t, q, rfl⟩

Result:
case h_add.intro.intro.intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ∃ s_1 q_1, (rename Subtype.val) p + (rename Subtype.val) q = (rename Subtype.val) q_1

Proof state:
case h_add.intro.intro.intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ∃ s_1 q_1, (rename Subtype.val) p + (rename Subtype.val) q = (rename Subtype.val) q_1

Tactic:
refine ⟨s ∪ t, ⟨?_, ?_⟩⟩

Result:
case h_add.intro.intro.intro.intro.refine_1
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ MvPolynomial { x // x ∈ s ∪ t } R

case h_add.intro.intro.intro.intro.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ (rename Subtype.val) p + (rename Subtype.val) q = (rename Subtype.val) ?h_add.intro.intro.intro.intro.refine_1

Proof state:
case h_C
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
r : R
⊢ ∃ s q, C r = (rename Subtype.val) q

Tactic:
exact ⟨∅, C r, by rw [rename_C]⟩

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∃ s q, p = (rename Subtype.val) q

Tactic:
apply induction_on p

Result:
case h_C
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (a : R), ∃ s q, C a = (rename Subtype.val) q

case h_add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (∃ s q, p = (rename Subtype.val) q) →
      (∃ s q_1, q = (rename Subtype.val) q_1) → ∃ s q_1, p + q = (rename Subtype.val) q_1

case h_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ), (∃ s q, p = (rename Subtype.val) q) → ∃ s q, p * X n = (rename Subtype.val) q

Proof state:
case h_add.intro.intro.intro.intro.refine_1
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ MvPolynomial { x // x ∈ s ∪ t } R

Tactic:
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]

Result:
no goals

Proof state:
case h_X.intro.intro.refine_1
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ MvPolynomial { x // x ∈ insert n s } R

Tactic:
refine rename (Subtype.map id ?_) p * X ⟨n, s.mem_insert_self n⟩

Result:
case h_X.intro.intro.refine_1
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ∀ a ∈ s, id a ∈ insert n s

Proof state:
case h_add.intro.intro.intro.intro.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ (rename Subtype.val) p + (rename Subtype.val) q =
    (rename (Subtype.val ∘ Subtype.map id ⋯)) p + (rename (Subtype.val ∘ Subtype.map id ⋯)) q

Tactic:
rfl

Result:
no goals

Proof state:
case h_X.intro.intro.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ (rename Subtype.val) p * X n = (rename (Subtype.val ∘ Subtype.map id ⋯)) p * X n

Tactic:
rfl

Result:
no goals

Proof state:
case h_add.intro.intro.intro.intro.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ (rename Subtype.val) p + (rename Subtype.val) q =
    (rename Subtype.val) ((rename (Subtype.map id ⋯)) p + (rename (Subtype.map id ⋯)) q)

Tactic:
simp only [rename_rename, map_add]

Result:
case h_add.intro.intro.intro.intro.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ (rename Subtype.val) p + (rename Subtype.val) q =
    (rename (Subtype.val ∘ Subtype.map id ⋯)) p + (rename (Subtype.val ∘ Subtype.map id ⋯)) q