awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
𝒜 : Finset (Finset α)
⊢ HAdd.hAdd (α := ℚ)
      (∑ x : Finset α,
        (↑(#(𝒜ᶜˢ.truncatedInf (({ toFun := compl, inj' := ⋯ : Finset α ↪ Finset α } : (a : Finset α) → Finset α) x))) :
            ℚ) /
          HMul.hMul (α := ℚ)
            (↑(Finset.card.{u_1} (α := α)
                  (({ toFun := compl, inj' := ⋯ : Finset α ↪ Finset α } : (a : Finset α) → Finset α) x)) :
              ℚ)
            (↑((card α).choose
                  (Finset.card.{u_1} (α := α)
                    (({ toFun := compl, inj' := ⋯ : Finset α ↪ Finset α } : (a : Finset α) → Finset α) x))) :
              ℚ))
      (∑ s ∈ map { toFun := compl, inj' := ⋯ : Finset α ↪ Finset α } univ,
        (↑(#(𝒜.truncatedSup s)) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ))) =
    HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹) + 1

Tactic:
simp only [Function.Embedding.coeFn_mk, univ_map_embedding, ← compl_truncatedSup,
    ← sum_add_distrib, card_compl, cast_sub (card_le_univ _), choose_symm (card_le_univ _),
    ← add_div, sub_add_cancel, Fintype.sum_div_mul_card_choose_card]

Premises used: Nat.cast_sub, Finset.sum_add_distrib, Finset.card_compl, Nat.choose_symm, Finset.card_le_univ, Function.Embedding.coeFn_mk, Finset.univ_map_embedding, _private.0.Fintype.sum_div_mul_card_choose_card, sub_add_cancel, Finset.compl_truncatedSup, add_div
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
inst_2 : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
⊢ let m := #𝒜;
  m = #𝒜

Tactic:
set m := 𝒜.card with hm

Premises used: Finset.card
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
inst_2 : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
m : ℕ := #𝒜
hm : m = #𝒜
clear_value : ∀ (m : ℕ) (hm : m = #𝒜), supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
⊢ supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)

Tactic:
clear_value m
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
m : ℕ
ih :
  ∀ m_1 < m,
    ∀ {𝒜 : Finset (Finset α)} (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜) (hm : m_1 = #𝒜),
      supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
hm : m = #𝒜
⊢ supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)

Tactic:
_
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
inst_2 : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
m : ℕ
hm : m = #𝒜
ind :
  ∀ (m : ℕ)
    (ih :
      ∀ m_1 < m,
        ∀ {𝒜 : Finset (Finset α)} (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜) (hm : m_1 = #𝒜),
          supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹))
    {𝒜 : Finset (Finset α)} (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜) (hm : m = #𝒜),
    supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
⊢ supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)

Tactic:
induction m using Nat.strongRecOn generalizing 𝒜 with | ind m ih => _
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
m : ℕ
ih :
  ∀ m_1 < m,
    ∀ {𝒜 : Finset (Finset α)} (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜) (hm : m_1 = #𝒜),
      supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
hm : m = #𝒜
⊢ ∀ (𝒜 : Finset (Finset α)) (h𝒜 : #𝒜 < m) (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜),
    supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)

Tactic:
replace ih := fun 𝒜 h𝒜 h𝒜₁ h𝒜₂ ↦ @ih _ h𝒜 𝒜 h𝒜₁ h𝒜₂ rfl
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
m : ℕ
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
hm : m = #𝒜
ih :
  ∀ (𝒜 : Finset (Finset α)) (h𝒜 : #𝒜 < m) (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜),
    supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
ind :
  ∀ (a : Finset α) (h𝒜₁ : Finset.Nonempty (α := Finset α) {a}) (h𝒜₂ : univ ∉ {a})
    (hm : m = Finset.card (α := Finset α) {a}),
    supSum (α := α) {a} = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
ind₁ : ∀ (h𝒜₃ : 𝒜.Nontrivial), supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
⊢ supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)

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

Premises used: Finset.Nonempty.exists_eq_singleton_or_nontrivial, rfl
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
m : ℕ
ih :
  ∀ (𝒜 : Finset (Finset α)) (h𝒜 : #𝒜 < m) (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜),
    supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
a : Finset α
h𝒜₁ : Finset.Nonempty (α := Finset α) {a}
h𝒜₂ : univ ∉ {a}
hm : m = Finset.card (α := Finset α) {a}
⊢ supSum (α := α) {a} = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)

Tactic:
supSum_singleton ?_

Premises used: AhlswedeZhang.supSum_singleton
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
m : ℕ
ih :
  ∀ (𝒜 : Finset (Finset α)) (h𝒜 : #𝒜 < m) (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜),
    supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
a : Finset α
h𝒜₁ : Finset.Nonempty (α := Finset α) {a}
h𝒜₂ : univ ∉ {a}
hm : m = Finset.card (α := Finset α) {a}
ind : a ≠ univ
⊢ supSum (α := α) {a} = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)

Tactic:
refine supSum_singleton ?_

Premises used: AhlswedeZhang.supSum_singleton
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
m : ℕ
ih :
  ∀ (𝒜 : Finset (Finset α)) (h𝒜 : #𝒜 < m) (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜),
    supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
a : Finset α
h𝒜₁ : Finset.Nonempty (α := Finset α) {a}
h𝒜₂ : univ ∉ {a}
hm : m = Finset.card (α := Finset α) {a}
⊢ a ≠ univ

Tactic:
simpa [eq_comm] using h𝒜₂

Premises used: eq_comm
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
m : ℕ
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
hm : m = #𝒜
ih :
  ∀ (𝒜 : Finset (Finset α)) (h𝒜 : #𝒜 < m) (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜),
    supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
h𝒜₃ : 𝒜.Nontrivial
ind :
  ∀ (hm : 0 = #𝒜)
    (ih :
      ∀ (𝒜 : Finset (Finset α)) (h𝒜 : #𝒜 < 0) (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜),
        supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)),
    supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
ind₁ :
  ∀ (n : ℕ) (hm : n + 1 = #𝒜)
    (ih :
      ∀ (𝒜 : Finset (Finset α)) (h𝒜 : #𝒜 < n + 1) (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜),
        supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)),
    supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
⊢ supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)

Tactic:
cases m
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
h𝒜₃ : 𝒜.Nontrivial
hm : 0 = #𝒜
ih :
  ∀ (𝒜 : Finset (Finset α)) (h𝒜 : #𝒜 < 0) (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜),
    supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
⊢ supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)

Tactic:
cases h𝒜₁.card_pos.ne hm

Premises used: Finset.Nonempty.card_pos, LT.lt.ne
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
h𝒜₃ : 𝒜.Nontrivial
n : ℕ
hm : n + 1 = #𝒜
ih :
  ∀ (𝒜 : Finset (Finset α)) (h𝒜 : #𝒜 < n + 1) (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜),
    supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
ind :
  ∀ (s : Finset α) (𝒜 : Finset (Finset α)) (hs : s ∉ 𝒜) (h𝒜₁ : (insert s 𝒜).Nonempty) (h𝒜₂ : univ ∉ insert s 𝒜)
    (h𝒜₃ : (insert s 𝒜).Nontrivial)
    (ih :
      ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
        supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹))
    (hm : #𝒜 + 1 = #(insert s 𝒜)),
    supSum (insert s 𝒜) = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
⊢ supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)

Tactic:
obtain ⟨s, 𝒜, hs, rfl, rfl⟩ := card_eq_succ.1 hm.symm

Premises used: Finset.card_eq_succ, Iff.mp, Eq.symm, rfl
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
by_contra! :
  ∀ (hs : s ∉ ∅) (h𝒜₁ : Finset.Nonempty (α := Finset α) (insert s ∅)) (h𝒜₂ : univ ∉ insert s ∅)
    (h𝒜₃ : Finset.Nontrivial (α := Finset α) (insert s ∅))
    (ih :
      ∀ (𝒜 : Finset (Finset α)) (h𝒜 : #𝒜 < Finset.card.{u_1} (α := Finset α) ∅ + 1) (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜),
        supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹))
    (hm : Finset.card.{u_1} (α := Finset α) ∅ + 1 = Finset.card (α := Finset α) (insert s ∅)), False
⊢ 𝒜.Nonempty

Tactic:
by_contra! rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
hs : s ∉ ∅
h𝒜₁ : Finset.Nonempty (α := Finset α) (insert s ∅)
h𝒜₂ : univ ∉ insert s ∅
h𝒜₃ : Finset.Nontrivial (α := Finset α) (insert s ∅)
ih :
  ∀ (𝒜 : Finset (Finset α)) (h𝒜 : #𝒜 < Finset.card.{u_1} (α := Finset α) ∅ + 1) (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜),
    supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : Finset.card.{u_1} (α := Finset α) ∅ + 1 = Finset.card (α := Finset α) (insert s ∅)
⊢ False

Tactic:
simp at h𝒜₃
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
⊢ 𝒜.Nonempty

Tactic:
have h𝒜 : 𝒜.Nonempty := by by_contra! rfl; simp at h𝒜₃
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
ind : Finset.card (α := Finset α) (image (fun (x : Finset α) ↦ s ⊓ x) 𝒜) < #𝒜 + 1
ind₁ : Finset.Nonempty (α := Finset α) (image (fun (x : Finset α) ↦ s ⊓ x) 𝒜)
ind₂ : univ ∉ image (fun (x : Finset α) ↦ s ⊓ x) 𝒜
ind₃ : #𝒜 < #𝒜 + 1
ind₄ : 𝒜.Nonempty
ind₅ : univ ∉ 𝒜
⊢ supSum (insert s 𝒜) = HMul.hMul (α := ℚ) (↑(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]

Premises used: Finset.insert_eq, Finset.mem_insert_self, eq_sub_of_add_eq, AhlswedeZhang.supSum_union_add_supSum_infs, Finset.singleton_infs, ne_of_mem_of_not_mem, AhlswedeZhang.supSum_singleton, add_sub_cancel_right
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ Finset.card (α := Finset α) (image (fun (x : Finset α) ↦ s ⊓ x) 𝒜) < #𝒜 + 1

Tactic:
card_image_le.trans_lt (lt_add_one _)

Premises used: lt_add_one, Finset.card_image_le, LE.le.trans_lt
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ Finset.card (α := Finset α) (image (fun (x : Finset α) ↦ s ⊓ x) 𝒜) < #𝒜 + 1

Tactic:
exact card_image_le.trans_lt (lt_add_one _)

Premises used: lt_add_one, Finset.card_image_le, LE.le.trans_lt
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ Finset.Nonempty (α := Finset α) (image (fun (x : Finset α) ↦ s ⊓ x) 𝒜)

Tactic:
h𝒜.image _

Premises used: Finset.Nonempty.image
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ Finset.Nonempty (α := Finset α) (image (fun (x : Finset α) ↦ s ⊓ x) 𝒜)

Tactic:
exact h𝒜.image _

Premises used: Finset.Nonempty.image
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ univ ∉ image (fun (x : Finset α) ↦ s ⊓ x) 𝒜

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

Premises used: Finset.mem_insert_self, ne_of_mem_of_not_mem
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ #𝒜 < #𝒜 + 1

Tactic:
lt_add_one _

Premises used: lt_add_one
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ #𝒜 < #𝒜 + 1

Tactic:
exact lt_add_one _

Premises used: lt_add_one
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ 𝒜.Nonempty

Tactic:
h𝒜
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ 𝒜.Nonempty

Tactic:
exact h𝒜
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ univ ∉ 𝒜

Tactic:
fun h ↦ h𝒜₂ (mem_insert_of_mem h)

Premises used: Finset.mem_insert_of_mem, Not
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)) (h𝒜 : #𝒜_1 < #𝒜 + 1) (h𝒜₁ : 𝒜_1.Nonempty) (h𝒜₂ : univ ∉ 𝒜_1),
    supSum 𝒜_1 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ univ ∉ 𝒜

Tactic:
exact fun h ↦ h𝒜₂ (mem_insert_of_mem h)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
inst_2 : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₀ : ∅ ∉ 𝒜
rw : univ ∉ 𝒜ᶜˢ
⊢ infSum 𝒜 = 1

Tactic:
rw [← compls_compls 𝒜, eq_sub_of_add_eq (infSum_compls_add_supSum _),
    supSum_of_univ_notMem h𝒜₁.compls, add_sub_cancel_left]

Premises used: add_sub_cancel_left, eq_sub_of_add_eq, Finset.compls_compls, AhlswedeZhang.infSum_compls_add_supSum, AhlswedeZhang.supSum_of_univ_notMem, Finset.Nonempty.compls
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
inst_2 : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₀ : ∅ ∉ 𝒜
⊢ univ ∉ 𝒜ᶜˢ

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ nonMemberSubfamily a 𝒜 ↔ s ∈ 𝒜 ∧ a ∉ s

Tactic:
simp [nonMemberSubfamily]

Premises used: Finset.nonMemberSubfamily
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
simp_rw : (∃ (a_1 : Finset α), (a_1 ∈ 𝒜 ∧ a ∈ a_1) ∧ a_1.erase a = s) ↔ insert a s ∈ 𝒜 ∧ a ∉ s
⊢ s ∈ memberSubfamily a 𝒜 ↔ insert a s ∈ 𝒜 ∧ a ∉ s

Tactic:
simp_rw [memberSubfamily, mem_image, mem_filter]

Premises used: Finset.mem_image, Finset.memberSubfamily, Finset.mem_filter
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝒜 ∧ a ∉ s
⊢ a ∈ insert a s

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
refine : (∃ (a_1 : Finset α), (a_1 ∈ 𝒜 ∧ a ∈ a_1) ∧ a_1.erase a = s) → insert a s ∈ 𝒜 ∧ a ∉ s
⊢ (∃ (a_1 : Finset α), (a_1 ∈ 𝒜 ∧ a ∈ a_1) ∧ a_1.erase a = s) ↔ insert a s ∈ 𝒜 ∧ a ∉ s

Tactic:
refine ⟨?_, fun h => ⟨insert a s, ⟨h.1, by simp⟩, erase_insert h.2⟩⟩
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
hs1 : s ∈ 𝒜
hs2 : a ∈ s
rw : s ∈ 𝒜 ∧ a ∉ s.erase a
⊢ insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a

Tactic:
rw [insert_erase hs2]

Premises used: Finset.insert_erase
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
hs1 : s ∈ 𝒜
hs2 : a ∈ s
⊢ s ∈ 𝒜 ∧ a ∉ s.erase a

Tactic:
⟨hs1, notMem_erase _ _⟩

Premises used: And.intro, Finset.notMem_erase
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
hs1 : s ∈ 𝒜
hs2 : a ∈ s
⊢ s ∈ 𝒜 ∧ a ∉ s.erase a

Tactic:
exact ⟨hs1, notMem_erase _ _⟩
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ nonMemberSubfamily a (𝒜 ∩ ℬ) = nonMemberSubfamily a 𝒜 ∩ nonMemberSubfamily a ℬ

Tactic:
filter_inter_distrib _ _ _

Premises used: Finset.nonMemberSubfamily, Finset.filter_inter_distrib
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
rw : (↑({s ∈ 𝒜 | a ∈ s}) : Set (Finset α)) ∪ (↑({s ∈ ℬ | a ∈ s}) : Set (Finset α)) ⊆ {s : Finset α | a ∈ s}
⊢ Eq (α := Finset (Finset α)) (image (fun (s : Finset α) ↦ s.erase a) ({s ∈ 𝒜 ∩ ℬ | a ∈ s}))
    (image (fun (s : Finset α) ↦ s.erase a) ({s ∈ 𝒜 | a ∈ s}) ∩
      image (fun (s : Finset α) ↦ s.erase a) ({s ∈ ℬ | a ∈ s}))

Tactic:
rw [filter_inter_distrib, image_inter_of_injOn _ _ ((erase_injOn' _).mono _)]

Premises used: Finset.image_inter_of_injOn, Finset.erase_injOn', Set.InjOn.mono, Finset.filter_inter_distrib
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ (↑({s ∈ 𝒜 | a ∈ s}) : Set (Finset α)) ∪ (↑({s ∈ ℬ | a ∈ s}) : Set (Finset α)) ⊆ {s : Finset α | a ∈ s}

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.Compression.Down
Goal:
α : Type u_1
inst : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ nonMemberSubfamily a (𝒜 ∪ ℬ) = nonMemberSubfamily a 𝒜 ∪ nonMemberSubfamily a ℬ

Tactic:
filter_union _ _ _

Premises used: Finset.nonMemberSubfamily, Finset.filter_union