-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_sum_of_disjoint [DecidableEq σ] (h : Pairwise <| (Disjoint on fun i => (φ i).vars)) :
    (∑ i ∈ t, φ i).vars = Finset.biUnion t fun i => (φ i).vars

Proof state:
case insert.intro.intro
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ a ∈ (φ i).vars, ∀ b ∈ (φ j).vars, a ≠ b
v : σ
hv : v ∈ (φ a✝).vars
v2 : σ
i : ι
his : i ∈ s✝
hi : v2 ∈ (φ i).vars
⊢ a✝ ≠ i

Tactic:
rintro rfl

Result:
case insert.intro.intro
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ a ∈ (φ i).vars, ∀ b ∈ (φ j).vars, a ≠ b
v : σ
hv : v ∈ (φ a✝).vars
v2 : σ
his : a✝ ∈ s✝
hi : v2 ∈ (φ a✝).vars
⊢ False

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => (φ i).vars)
⊢ (∑ i ∈ t, φ i).vars = t.biUnion fun i => (φ i).vars

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

Result:
no goals

Proof state:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ a ∈ (φ i).vars, ∀ b ∈ (φ j).vars, a ≠ b
v : σ
hv : v ∈ (φ a✝).vars
v2 : σ
hv2 : v2 ∈ s✝.biUnion fun i => (φ i).vars
⊢ v ≠ v2

Tactic:
rw [Finset.mem_biUnion] at hv2

Result:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ a ∈ (φ i).vars, ∀ b ∈ (φ j).vars, a ≠ b
v : σ
hv : v ∈ (φ a✝).vars
v2 : σ
hv2 : ∃ a ∈ s✝, v2 ∈ (φ a).vars
⊢ v ≠ v2

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => (φ i).vars)
⊢ (∑ i ∈ t, φ i).vars = t.biUnion fun i => (φ i).vars

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

Result:
no goals

Proof state:
case empty
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => (φ i).vars)
⊢ (∑ i ∈ ∅, φ i).vars = ∅.biUnion fun i => (φ i).vars

Tactic:
simp

Result:
no goals

Proof state:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ((fun i => (φ i).vars) i) ((fun i => (φ i).vars) j)
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
⊢ Disjoint (φ a✝).vars (∑ x ∈ s✝, φ x).vars

Tactic:
rw [hsum]

Result:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ((fun i => (φ i).vars) i) ((fun i => (φ i).vars) j)
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
⊢ Disjoint (φ a✝).vars (s✝.biUnion fun i => (φ i).vars)

Proof state:
case insert.intro.intro
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ a ∈ (φ i).vars, ∀ b ∈ (φ j).vars, a ≠ b
v : σ
hv : v ∈ (φ a✝).vars
v2 : σ
his : a✝ ∈ s✝
hi : v2 ∈ (φ a✝).vars
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
case insert.intro.intro
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ a ∈ (φ i).vars, ∀ b ∈ (φ j).vars, a ≠ b
v : σ
hv : v ∈ (φ a✝).vars
v2 : σ
i : ι
his : i ∈ s✝
hi : v2 ∈ (φ i).vars
⊢ v ≠ v2

Tactic:
refine h ?_ _ hv _ hi

Result:
case insert.intro.intro
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ a ∈ (φ i).vars, ∀ b ∈ (φ j).vars, a ≠ b
v : σ
hv : v ∈ (φ a✝).vars
v2 : σ
i : ι
his : i ∈ s✝
hi : v2 ∈ (φ i).vars
⊢ a✝ ≠ i

Proof state:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => (φ i).vars)
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
⊢ (∑ i ∈ insert a✝ s✝, φ i).vars = (insert a✝ s✝).biUnion fun i => (φ i).vars

Tactic:
rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]

Result:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => (φ i).vars)
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
⊢ Disjoint (φ a✝).vars (∑ x ∈ s✝, φ x).vars

Proof state:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ a ∈ (φ i).vars, ∀ b ∈ (φ j).vars, a ≠ b
⊢ ∀ a ∈ (φ a✝).vars, ∀ b ∈ s✝.biUnion fun i => (φ i).vars, a ≠ b

Tactic:
intro v hv v2 hv2

Result:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ a ∈ (φ i).vars, ∀ b ∈ (φ j).vars, a ≠ b
v : σ
hv : v ∈ (φ a✝).vars
v2 : σ
hv2 : v2 ∈ s✝.biUnion fun i => (φ i).vars
⊢ v ≠ v2

Proof state:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ a ∈ (φ i).vars, ∀ b ∈ (φ j).vars, a ≠ b
v : σ
hv : v ∈ (φ a✝).vars
v2 : σ
hv2 : ∃ a ∈ s✝, v2 ∈ (φ a).vars
⊢ v ≠ v2

Tactic:
rcases hv2 with ⟨i, his, hi⟩

Result:
case insert.intro.intro
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ a ∈ (φ i).vars, ∀ b ∈ (φ j).vars, a ≠ b
v : σ
hv : v ∈ (φ a✝).vars
v2 : σ
i : ι
his : i ∈ s✝
hi : v2 ∈ (φ i).vars
⊢ v ≠ v2