no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => vars (φ i))
⊢ vars (∑ i in t, φ i) = Finset.biUnion t fun i => vars (φ i)
classical
induction t using Finset.induction_on with
| empty => simp
| insert has hsum =>
  rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
  unfold Pairwise onFun at h
  rw [hsum]
  simp only [Finset.disjoint_iff_ne] at h⊢
  intro v hv v2 hv2
  rw [Finset.mem_biUnion] at hv2
  rcases hv2 with ⟨i, his, hi⟩
  refine' h _ _ hv _ hi
  rintro rfl
  contradiction
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => vars (φ i))
⊢ vars (∑ i in t, φ i) = Finset.biUnion t fun i => vars (φ i)
induction t using Finset.induction_on with
| empty => simp
| insert has hsum =>
  rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
  unfold Pairwise onFun at h
  rw [hsum]
  simp only [Finset.disjoint_iff_ne] at h⊢
  intro v hv v2 hv2
  rw [Finset.mem_biUnion] at hv2
  rcases hv2 with ⟨i, his, hi⟩
  refine' h _ _ hv _ hi
  rintro rfl
  contradiction
no goals
case empty
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => vars (φ i))
⊢ vars (∑ i in ∅, φ i) = Finset.biUnion ∅ fun i => vars (φ i)
simp
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => vars (φ i))
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
⊢ Disjoint (vars (φ a✝)) (vars (∑ x in s✝, φ x))
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => vars (φ i))
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
⊢ vars (∑ i in insert a✝ s✝, φ i) = Finset.biUnion (insert a✝ s✝) fun i => vars (φ i)
rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ((fun i => vars (φ i)) i) ((fun i => vars (φ i)) j)
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
⊢ Disjoint (vars (φ a✝)) (vars (∑ x in s✝, φ x))
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => vars (φ i))
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
⊢ Disjoint (vars (φ a✝)) (vars (∑ x in s✝, φ x))
unfold Pairwise onFun at h
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ((fun i => vars (φ i)) i) ((fun i => vars (φ i)) j)
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
⊢ Disjoint (vars (φ a✝)) (Finset.biUnion s✝ fun i => vars (φ i))
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ((fun i => vars (φ i)) i) ((fun i => vars (φ i)) j)
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
⊢ Disjoint (vars (φ a✝)) (vars (∑ x in s✝, φ x))
rw [hsum]
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
⊢ ∀ (a : σ), a ∈ vars (φ a✝) → ∀ (b : σ), (b ∈ Finset.biUnion s✝ fun i => vars (φ i)) → a ≠ b
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ((fun i => vars (φ i)) i) ((fun i => vars (φ i)) j)
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
⊢ Disjoint (vars (φ a✝)) (Finset.biUnion s✝ fun i => vars (φ i))
simp only [Finset.disjoint_iff_ne] at h⊢
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
v : σ
hv : v ∈ vars (φ a✝)
v2 : σ
hv2 : v2 ∈ Finset.biUnion s✝ fun i => vars (φ i)
⊢ v ≠ v2
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
⊢ ∀ (a : σ), a ∈ vars (φ a✝) → ∀ (b : σ), (b ∈ Finset.biUnion s✝ fun i => vars (φ i)) → a ≠ b
intro v hv v2 hv2
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
v : σ
hv : v ∈ vars (φ a✝)
v2 : σ
hv2 : ∃ a, a ∈ s✝ ∧ v2 ∈ vars (φ a)
⊢ v ≠ v2
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
v : σ
hv : v ∈ vars (φ a✝)
v2 : σ
hv2 : v2 ∈ Finset.biUnion s✝ fun i => vars (φ i)
⊢ v ≠ v2
rw [Finset.mem_biUnion] at hv2
case insert.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
v : σ
hv : v ∈ vars (φ a✝)
v2 : σ
i : ι
his : i ∈ s✝
hi : v2 ∈ vars (φ i)
⊢ v ≠ v2
case insert
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
v : σ
hv : v ∈ vars (φ a✝)
v2 : σ
hv2 : ∃ a, a ∈ s✝ ∧ v2 ∈ vars (φ a)
⊢ v ≠ v2
rcases hv2 with ⟨i, his, hi⟩
case insert.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
v : σ
hv : v ∈ vars (φ a✝)
v2 : σ
i : ι
his : i ∈ s✝
hi : v2 ∈ vars (φ i)
⊢ a✝ ≠ i
case insert.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
v : σ
hv : v ∈ vars (φ a✝)
v2 : σ
i : ι
his : i ∈ s✝
hi : v2 ∈ vars (φ i)
⊢ v ≠ v2
refine' h _ _ hv _ hi
case insert.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
v : σ
hv : v ∈ vars (φ a✝)
v2 : σ
his : a✝ ∈ s✝
hi : v2 ∈ vars (φ a✝)
⊢ False
case insert.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
v : σ
hv : v ∈ vars (φ a✝)
v2 : σ
i : ι
his : i ∈ s✝
hi : v2 ∈ vars (φ i)
⊢ a✝ ≠ i
rintro rfl
no goals
case insert.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.195288
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_2
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : ¬a✝ ∈ s✝
hsum : vars (∑ i in s✝, φ i) = Finset.biUnion s✝ fun i => vars (φ i)
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ (a : σ), a ∈ vars (φ i) → ∀ (b : σ), b ∈ vars (φ j) → a ≠ b
v : σ
hv : v ∈ vars (φ a✝)
v2 : σ
his : a✝ ∈ s✝
hi : v2 ∈ vars (φ a✝)
⊢ False
contradiction