-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem exists_finset_rename₂ (p₁ p₂ : MvPolynomial σ R) :
    ∃ (s : Finset σ) (q₁ q₂ : MvPolynomial s R), p₁ = rename (↑) q₁ ∧ p₂ = rename (↑) q₂

Proof state:
case intro.intro.intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ∃ s q₁_1 q₂_1,
    (rename Subtype.val) q₁ = (rename Subtype.val) q₁_1 ∧ (rename Subtype.val) q₂ = (rename Subtype.val) q₂_1

Tactic:
use s₁ ∪ s₂

Result:
case h
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ∃ q₁_1 q₂_1, (rename Subtype.val) q₁ = (rename Subtype.val) q₁_1 ∧ (rename Subtype.val) q₂ = (rename Subtype.val) q₂_1

Proof state:
case h.right
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ (rename Subtype.val) q₂ = (rename Subtype.val) ((rename (inclusion ⋯)) q₂)

Tactic:
erw [rename_rename (Set.inclusion s₁.subset_union_right)]

Result:
case h.right
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ (rename Subtype.val) q₂ = (rename (Subtype.val ∘ inclusion ⋯)) q₂

Proof state:
case intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p₂ : MvPolynomial σ R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
⊢ ∃ s q₁_1 q₂, (rename Subtype.val) q₁ = (rename Subtype.val) q₁_1 ∧ p₂ = (rename Subtype.val) q₂

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

Result:
case intro.intro.intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ∃ s q₁_1 q₂_1,
    (rename Subtype.val) q₁ = (rename Subtype.val) q₁_1 ∧ (rename Subtype.val) q₂ = (rename Subtype.val) q₂_1

Proof state:
case h
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ∃ q₁_1 q₂_1, (rename Subtype.val) q₁ = (rename Subtype.val) q₁_1 ∧ (rename Subtype.val) q₂ = (rename Subtype.val) q₂_1

Tactic:
use rename (Set.inclusion s₁.subset_union_left) q₁

Result:
case h
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ∃ q₂_1,
    (rename Subtype.val) q₁ = (rename Subtype.val) ((rename (inclusion ⋯)) q₁) ∧
      (rename Subtype.val) q₂ = (rename Subtype.val) q₂_1

Proof state:
case h
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ (rename Subtype.val) q₁ = (rename Subtype.val) ((rename (inclusion ⋯)) q₁) ∧
    (rename Subtype.val) q₂ = (rename Subtype.val) ((rename (inclusion ⋯)) q₂)

Tactic:
constructor

Result:
case h.left
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ (rename Subtype.val) q₁ = (rename Subtype.val) ((rename (inclusion ⋯)) q₁)

case h.right
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ (rename Subtype.val) q₂ = (rename Subtype.val) ((rename (inclusion ⋯)) q₂)

Proof state:
case h
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ∃ q₂_1,
    (rename Subtype.val) q₁ = (rename Subtype.val) ((rename (inclusion ⋯)) q₁) ∧
      (rename Subtype.val) q₂ = (rename Subtype.val) q₂_1

Tactic:
use rename (Set.inclusion s₁.subset_union_right) q₂

Result:
case h
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ (rename Subtype.val) q₁ = (rename Subtype.val) ((rename (inclusion ⋯)) q₁) ∧
    (rename Subtype.val) q₂ = (rename Subtype.val) ((rename (inclusion ⋯)) q₂)

Proof state:
case h.right
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ (rename Subtype.val) q₂ = (rename (Subtype.val ∘ inclusion ⋯)) q₂

Tactic:
rfl

Result:
no goals

Proof state:
case h.left
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ (rename Subtype.val) q₁ = (rename (Subtype.val ∘ inclusion ⋯)) q₁

Tactic:
rfl

Result:
no goals

Proof state:
case h.left
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ (rename Subtype.val) q₁ = (rename Subtype.val) ((rename (inclusion ⋯)) q₁)

Tactic:
erw [rename_rename (Set.inclusion s₁.subset_union_left)]

Result:
case h.left
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ (rename Subtype.val) q₁ = (rename (Subtype.val ∘ inclusion ⋯)) q₁

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

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

Result:
case intro.intro
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p₂ : MvPolynomial σ R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
⊢ ∃ s q₁_1 q₂, (rename Subtype.val) q₁ = (rename Subtype.val) q₁_1 ∧ p₂ = (rename Subtype.val) q₂