-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem finset_sum_eq_sup_iff_disjoint [DecidableEq α] {i : Finset β} {f : β → Multiset α} :
    i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)

Proof state:
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
i : Finset β
f : β → Multiset α
⊢ i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)

Tactic:
induction' i using Finset.cons_induction_on with z i hz hr

Result:
case h₁
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
⊢ ∅.sum f = ∅.sup f ↔ ∀ x ∈ ∅, ∀ y ∈ ∅, x ≠ y → Disjoint (f x) (f y)

case h₂
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
⊢ (Finset.cons z i hz).sum f = (Finset.cons z i hz).sup f ↔
    ∀ x ∈ Finset.cons z i hz, ∀ y ∈ Finset.cons z i hz, x ≠ y → Disjoint (f x) (f y)

Proof state:
case h₁
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
⊢ ∅.sum f = ∅.sup f ↔ ∀ x ∈ ∅, ∀ y ∈ ∅, x ≠ y → Disjoint (f x) (f y)

Tactic:
simp only [Finset.not_mem_empty, IsEmpty.forall_iff, imp_true_iff, Finset.sum_empty,
  Finset.sup_empty, bot_eq_zero, eq_self_iff_true]

Result:
no goals

Proof state:
case h₂
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
⊢ (Finset.cons z i hz).sum f = (Finset.cons z i hz).sup f ↔
    ∀ x ∈ Finset.cons z i hz, ∀ y ∈ Finset.cons z i hz, x ≠ y → Disjoint (f x) (f y)

Tactic:
simp_rw [Finset.sum_cons hz, Finset.sup_cons, Finset.mem_cons, Multiset.sup_eq_union,
  forall_eq_or_imp, Ne, not_true_eq_false, IsEmpty.forall_iff, true_and,
  imp_and, forall_and, ← hr, @eq_comm _ z]

Result:
case h₂
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (∀ a ∈ i, ¬a = z → Disjoint (f z) (f a)) ∧ (∀ x ∈ i, ¬x = z → Disjoint (f x) (f z)) ∧ i.sum f = i.sup f

Proof state:
case h₂
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
this : ∀ x ∈ i, x ≠ z
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔ Disjoint (f z) (i.sum f) ∧ i.sum f = i.sup f

Tactic:
exact add_eq_union_left_of_le (Finset.sup_le fun x hx => le_sum_of_mem (mem_map_of_mem f hx))

Result:
no goals

Proof state:
case h₂
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
this : ∀ x ∈ i, x ≠ z
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (∀ a ∈ i, Disjoint (f z) (f a)) ∧ (∀ x ∈ i, Disjoint (f x) (f z)) ∧ i.sum f = i.sup f

Tactic:
simp_rw [← disjoint_finset_sum_left, ← disjoint_finset_sum_right, disjoint_comm, ← and_assoc,
  and_self_iff]

Result:
case h₂
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
this : ∀ x ∈ i, x ≠ z
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔ Disjoint (f z) (i.sum f) ∧ i.sum f = i.sup f

Proof state:
case h₂
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
this : ∀ x ∈ i, x ≠ z
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (∀ a ∈ i, ¬a = z → Disjoint (f z) (f a)) ∧ (∀ x ∈ i, ¬x = z → Disjoint (f x) (f z)) ∧ i.sum f = i.sup f

Tactic:
simp +contextual only [this, not_false_iff, true_imp_iff]

Result:
case h₂
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
this : ∀ x ∈ i, x ≠ z
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (∀ a ∈ i, Disjoint (f z) (f a)) ∧ (∀ x ∈ i, Disjoint (f x) (f z)) ∧ i.sum f = i.sup f

Proof state:
case h₂
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (∀ a ∈ i, ¬a = z → Disjoint (f z) (f a)) ∧ (∀ x ∈ i, ¬x = z → Disjoint (f x) (f z)) ∧ i.sum f = i.sup f

Tactic:
have := fun x (H : x ∈ i) => ne_of_mem_of_not_mem H hz

Result:
case h₂
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
this : ∀ x ∈ i, x ≠ z
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (∀ a ∈ i, ¬a = z → Disjoint (f z) (f a)) ∧ (∀ x ∈ i, ¬x = z → Disjoint (f x) (f z)) ∧ i.sum f = i.sup f