case intro.intro
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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₂
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p₁ p₂ : MvPolynomial σ R
⊢ ∃ s q₁ q₂, p₁ = ↑(rename Subtype.val) q₁ ∧ p₂ = ↑(rename Subtype.val) q₂
obtain ⟨s₁, q₁, rfl⟩ := exists_finset_rename p₁
case intro.intro.intro.intro
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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
case intro.intro
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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₂
obtain ⟨s₂, q₂, rfl⟩ := exists_finset_rename p₂
case intro.intro.intro.intro
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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
case intro.intro.intro.intro
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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
use s₁ ∪ s₂
case intro.intro.intro.intro
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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 (_ : s₁ ⊆ s₁ ∪ s₂))) q₁) ∧
      ↑(rename Subtype.val) q₂ = ↑(rename Subtype.val) q₂_1
case intro.intro.intro.intro
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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
use rename (Set.inclusion <| s₁.subset_union_left s₂) q₁
case intro.intro.intro.intro
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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 (_ : s₁ ⊆ s₁ ∪ s₂))) q₁) ∧
    ↑(rename Subtype.val) q₂ = ↑(rename Subtype.val) (↑(rename (inclusion (_ : s₂ ⊆ s₁ ∪ s₂))) q₂)
case intro.intro.intro.intro
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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 (_ : s₁ ⊆ s₁ ∪ s₂))) q₁) ∧
      ↑(rename Subtype.val) q₂ = ↑(rename Subtype.val) q₂_1
use rename (Set.inclusion <| s₁.subset_union_right s₂) q₂
case intro.intro.intro.intro.left
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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 (_ : s₁ ⊆ s₁ ∪ s₂))) q₁)

case intro.intro.intro.intro.right
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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 (_ : s₂ ⊆ s₁ ∪ s₂))) q₂)
case intro.intro.intro.intro
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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 (_ : s₁ ⊆ s₁ ∪ s₂))) q₁) ∧
    ↑(rename Subtype.val) q₂ = ↑(rename Subtype.val) (↑(rename (inclusion (_ : s₂ ⊆ s₁ ∪ s₂))) q₂)
constructor
case intro.intro.intro.intro.left
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ↑(rename Subtype.val) q₁ = ↑(rename (Subtype.val ∘ inclusion (_ : s₁ ⊆ s₁ ∪ s₂))) q₁
case intro.intro.intro.intro.left
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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 (_ : s₁ ⊆ s₁ ∪ s₂))) q₁)
rw [rename_rename (Set.inclusion <| s₁.subset_union_left s₂)]
no goals
case intro.intro.intro.intro.left
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ↑(rename Subtype.val) q₁ = ↑(rename (Subtype.val ∘ inclusion (_ : s₁ ⊆ s₁ ∪ s₂))) q₁
rfl
case intro.intro.intro.intro.right
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ↑(rename Subtype.val) q₂ = ↑(rename (Subtype.val ∘ inclusion (_ : s₂ ⊆ s₁ ∪ s₂))) q₂
case intro.intro.intro.intro.right
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
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 (_ : s₂ ⊆ s₁ ∪ s₂))) q₂)
rw [rename_rename (Set.inclusion <| s₁.subset_union_right s₂)]
no goals
case intro.intro.intro.intro.right
σ : Type u_1
τ : Type ?u.798711
α : Type ?u.798714
R : Type u_2
S : Type ?u.798720
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ↑(rename Subtype.val) q₂ = ↑(rename (Subtype.val ∘ inclusion (_ : s₂ ⊆ s₁ ∪ s₂))) q₂
rfl