-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma supSum_of_not_univ_mem (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜) :
    supSum 𝒜 = card α * ∑ k ∈ range (card α), (k : ℚ)⁻¹

Proof state:
case ind.inr.succ.intro.intro.intro.intro
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ supSum (insert s 𝒜) = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
rw [insert_eq, eq_sub_of_add_eq (supSum_union_add_supSum_infs _ _), singleton_infs,
  supSum_singleton (ne_of_mem_of_not_mem (mem_insert_self _ _) h𝒜₂), ih, ih, add_sub_cancel_right]

Result:
case ind.inr.succ.intro.intro.intro.intro.h𝒜
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ #(image (fun x => s ⊓ x) 𝒜) < #𝒜 + 1

case ind.inr.succ.intro.intro.intro.intro.h𝒜₁
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ (image (fun x => s ⊓ x) 𝒜).Nonempty

case ind.inr.succ.intro.intro.intro.intro.h𝒜₂
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ univ ∉ image (fun x => s ⊓ x) 𝒜

case ind.inr.succ.intro.intro.intro.intro.h𝒜
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ #𝒜 < #𝒜 + 1

case ind.inr.succ.intro.intro.intro.intro.h𝒜₁
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ 𝒜.Nonempty

case ind.inr.succ.intro.intro.intro.intro.h𝒜₂
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ univ ∉ 𝒜

Proof state:
case ind.inr.succ.intro.intro.intro.intro.h𝒜₂
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ univ ∉ image (fun x => s ⊓ x) 𝒜

Tactic:
simpa using fun _ ↦ ne_of_mem_of_not_mem (mem_insert_self _ _) h𝒜₂

Result:
no goals

Proof state:
case ind.inr.succ.intro.intro.intro.intro
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
⊢ supSum (insert s 𝒜) = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
have h𝒜 : 𝒜.Nonempty := nonempty_iff_ne_empty.2 (by rintro rfl; simp at h𝒜₃)

Result:
case ind.inr.succ.intro.intro.intro.intro
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ supSum (insert s 𝒜) = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Proof state:
case ind.inr.succ.intro.intro.intro.intro.h𝒜₁
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ 𝒜.Nonempty

Tactic:
exact h𝒜

Result:
no goals

Proof state:
case ind
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
m : ℕ
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
hm : m = #𝒜
ih : ∀ (𝒜 : Finset (Finset α)), #𝒜 < m → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
obtain ⟨a, rfl⟩ | h𝒜₃ := h𝒜₁.exists_eq_singleton_or_nontrivial

Result:
case ind.inl.intro
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
m : ℕ
ih : ∀ (𝒜 : Finset (Finset α)), #𝒜 < m → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
a : Finset α
h𝒜₁ : {a}.Nonempty
h𝒜₂ : univ ∉ {a}
hm : m = #{a}
⊢ supSum {a} = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

case ind.inr
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
m : ℕ
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
hm : m = #𝒜
ih : ∀ (𝒜 : Finset (Finset α)), #𝒜 < m → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
h𝒜₃ : 𝒜.Nontrivial
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Proof state:
case ind.inr
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
m : ℕ
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
hm : m = #𝒜
ih : ∀ (𝒜 : Finset (Finset α)), #𝒜 < m → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
h𝒜₃ : 𝒜.Nontrivial
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
cases m

Result:
case ind.inr.zero
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
h𝒜₃ : 𝒜.Nontrivial
hm : 0 = #𝒜
ih : ∀ (𝒜 : Finset (Finset α)), #𝒜 < 0 → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

case ind.inr.succ
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
h𝒜₃ : 𝒜.Nontrivial
n✝ : ℕ
hm : n✝ + 1 = #𝒜
ih :
  ∀ (𝒜 : Finset (Finset α)), #𝒜 < n✝ + 1 → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹