awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ upperClosure (↑𝒜 : Set (Finset α))
hℬ : s ∉ upperClosure (↑ℬ : Set (Finset α))
neg : #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = card.{u_1} (α := α) ⊥ + #(ℬ.truncatedInf s)
neg₁ : #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = card.{u_1} (α := α) ⊥ + card.{u_1} (α := α) ⊥
neg₂ : card.{u_1} (α := α) ⊥ + #((𝒜 ⊻ ℬ).truncatedInf s) = card.{u_1} (α := α) ⊥ + card.{u_1} (α := α) ⊥
neg₃ neg₄ : card.{u_1} (α := α) ⊥ + card.{u_1} (α := α) ⊥ = card.{u_1} (α := α) ⊥ + card.{u_1} (α := α) ⊥
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)

Tactic:
rw [truncatedInf_of_notMem h𝒜, truncatedInf_of_notMem hℬ,
      truncatedInf_union_of_notMem h𝒜 hℬ, truncatedInf_sups_of_notMem fun h ↦ h𝒜 h.1]

Premises used: Finset.truncatedInf_union_of_notMem, Finset.truncatedInf_sups_of_notMem, And.left, Finset.truncatedInf_of_notMem
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 ℬ : Finset (Finset α)
rw :
  ∀ (s : Finset α),
    Membership.mem (γ := Finset (Finset α)) univ s →
      (↑(#((𝒜 ∪ ℬ).truncatedSup s)) : ℚ) /
            (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) +
          (↑(#((𝒜 ⊼ ℬ).truncatedSup s)) : ℚ) /
            (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) =
        (↑(#(𝒜.truncatedSup s)) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) +
          (↑(#(ℬ.truncatedSup s)) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ))
⊢ HAdd.hAdd (α := ℚ)
      (∑ s : Finset α,
        (↑(#((𝒜 ∪ ℬ).truncatedSup s)) : ℚ) /
          (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)))
      (∑ s : Finset α,
        (↑(#((𝒜 ⊼ ℬ).truncatedSup s)) : ℚ) /
          (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ))) =
    HAdd.hAdd (α := ℚ)
      (∑ s : Finset α,
        (↑(#(𝒜.truncatedSup s)) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)))
      (∑ s : Finset α,
        (↑(#(ℬ.truncatedSup s)) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)))

Tactic:
rw [← sum_add_distrib, ← sum_add_distrib, Finset.sum_congr rfl fun s _ ↦ _]

Premises used: Finset.sum_add_distrib, Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 ℬ : Finset (Finset α)
simp_rw : ∀ (s : Finset α), Membership.mem (γ := Finset (Finset α)) univ s → True
⊢ ∀ (s : Finset α),
    Membership.mem (γ := Finset (Finset α)) univ s →
      (↑(#((𝒜 ∪ ℬ).truncatedSup s)) : ℚ) /
            (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) +
          (↑(#((𝒜 ⊼ ℬ).truncatedSup s)) : ℚ) /
            (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) =
        (↑(#(𝒜.truncatedSup s)) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) +
          (↑(#(ℬ.truncatedSup s)) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ))

Tactic:
simp_rw [← add_div, ← Nat.cast_add, card_truncatedSup_union_add_card_truncatedSup_infs]

Premises used: Nat.cast_add, Finset.card_truncatedSup_union_add_card_truncatedSup_infs, add_div
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ (s : Finset α), Membership.mem (γ := Finset (Finset α)) univ s → True

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 ℬ : Finset (Finset α)
rw :
  ∀ (s : Finset α),
    Membership.mem (γ := Finset (Finset α)) univ s →
      (↑(#((𝒜 ∪ ℬ).truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ) +
          (↑(#((𝒜 ⊻ ℬ).truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ) =
        (↑(#(𝒜.truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ) +
          (↑(#(ℬ.truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ)
⊢ HAdd.hAdd (α := ℚ)
      (∑ s : Finset α, (↑(#((𝒜 ∪ ℬ).truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ))
      (∑ s : Finset α,
        (↑(#((𝒜 ⊻ ℬ).truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ)) =
    HAdd.hAdd (α := ℚ)
      (∑ s : Finset α, (↑(#(𝒜.truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ))
      (∑ s : Finset α, (↑(#(ℬ.truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ))

Tactic:
rw [← sum_add_distrib, ← sum_add_distrib, Finset.sum_congr rfl fun s _ ↦ _]

Premises used: Finset.sum_add_distrib, Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 ℬ : Finset (Finset α)
simp_rw : ∀ (s : Finset α), Membership.mem (γ := Finset (Finset α)) univ s → True
⊢ ∀ (s : Finset α),
    Membership.mem (γ := Finset (Finset α)) univ s →
      (↑(#((𝒜 ∪ ℬ).truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ) +
          (↑(#((𝒜 ⊻ ℬ).truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ) =
        (↑(#(𝒜.truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ) +
          (↑(#(ℬ.truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ)

Tactic:
simp_rw [← add_div, ← Nat.cast_add, card_truncatedInf_union_add_card_truncatedInf_sups]

Premises used: Finset.card_truncatedInf_union_add_card_truncatedInf_sups, Nat.cast_add, add_div
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
h𝒜₀ : ∅ ∉ 𝒜
⊢ Eq (α := ℚ) (∑ s ∈ 𝒜, (↑((card α).choose #s) : ℚ)⁻¹)
    (∑ s ∈ 𝒜, (↑(#(𝒜.truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ))

Tactic:
?_
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
h𝒜₀ : ∅ ∉ 𝒜
s : Finset α
⊢ 0 ≤ (↑(#(𝒜.truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
h𝒜₀ : ∅ ∉ 𝒜
_ :
  Eq (α := ℚ) (∑ s ∈ 𝒜, (↑((card α).choose #s) : ℚ)⁻¹)
    (∑ s ∈ 𝒜, (↑(#(𝒜.truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ))
⊢ ∑ s ∈ 𝒜, (↑((card α).choose #s) : ℚ)⁻¹ ≤ infSum 𝒜

Tactic:
calc
    _ = ∑ s ∈ 𝒜, #(truncatedInf 𝒜 s) / (#s * (card α).choose #s : ℚ) := ?_
    _ ≤ _ := sum_le_univ_sum_of_nonneg fun s ↦ by positivity

Premises used: Finset.sum_le_univ_sum_of_nonneg
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
h𝒜₀ : ∅ ∉ 𝒜
⊢ Eq (α := ℚ) (∑ s ∈ 𝒜, (↑((card α).choose #s) : ℚ)⁻¹)
    (∑ s ∈ 𝒜, (↑(#(𝒜.truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ))

Tactic:
sum_congr rfl fun s hs ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
h𝒜₀ : ∅ ∉ 𝒜
refine :
  ∀ (s : Finset α) (hs : s ∈ 𝒜),
    (↑((card α).choose #s) : ℚ)⁻¹ =
      (↑(#(𝒜.truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ)
⊢ Eq (α := ℚ) (∑ s ∈ 𝒜, (↑((card α).choose #s) : ℚ)⁻¹)
    (∑ s ∈ 𝒜, (↑(#(𝒜.truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ))

Tactic:
refine sum_congr rfl fun s hs ↦ ?_
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
h𝒜₀ : ∅ ∉ 𝒜
s : Finset α
hs : s ∈ 𝒜
ha : Ne (α := ℚ) (↑(#s) : ℚ) 0
⊢ (↑((card α).choose #s) : ℚ)⁻¹ =
    (↑(#(𝒜.truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ)

Tactic:
rw [truncatedInf_of_isAntichain h𝒜 hs, div_mul_cancel_left₀]

Premises used: div_mul_cancel_left₀, Finset.truncatedInf_of_isAntichain
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
h𝒜₀ : ∅ ∉ 𝒜
s : Finset α
hs : s ∈ 𝒜
⊢ 0 < #s

Tactic:
have := (nonempty_iff_ne_empty.2 <| ne_of_mem_of_not_mem hs h𝒜₀).card_pos
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
h𝒜₀ : ∅ ∉ 𝒜
s : Finset α
hs : s ∈ 𝒜
this : 0 < #s
⊢ Ne (α := ℚ) (↑(#s) : ℚ) 0

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
inst_2 : Nonempty α
hs : s ≠ univ
t : Finset α
simp_rw :
  HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#(if t ⊆ s then s else ⊤)) : ℚ) /
      (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
    if t ⊆ s then
      HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ))
    else 0
⊢ HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#(truncatedSup {s} t)) : ℚ) /
      (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
    if t ⊆ s then
      HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ))
    else 0

Tactic:
simp_rw [truncatedSup_singleton, le_iff_subset]

Premises used: Finset.truncatedSup_singleton, Finset.le_iff_subset
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
inst_2 : Nonempty α
hs : s ≠ univ
t : Finset α
pos :
  t ⊆ s →
    HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
      HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ))
neg :
  ¬t ⊆ s →
    HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(Finset.card.{u_1} (α := α) ⊤) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
      0
⊢ HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#(if t ⊆ s then s else ⊤)) : ℚ) /
      (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
    if t ⊆ s then
      HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ))
    else 0

Tactic:
split_ifs
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
inst_2 : Nonempty α
hs : s ≠ univ
t : Finset α
h : t ⊆ s
⊢ HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
      (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
    HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
      (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ))

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
inst_2 : Nonempty α
hs : s ≠ univ
t : Finset α
h : ¬t ⊆ s
⊢ HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(Finset.card.{u_1} (α := α) ⊤) : ℚ) /
      (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
    0

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
inst_2 : Nonempty α
hs : s ≠ univ
⊢ ∀ (t : Finset α),
    HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#(truncatedSup {s} t)) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
      if t ⊆ s then
        HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
          (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ))
      else 0

Tactic:
have : ∀ t : Finset α,
    (card α - #(truncatedSup {s} t) : ℚ) / ((card α - #t) * (card α).choose #t) =
    if t ⊆ s then (card α - #s : ℚ) / ((card α - #t) * (card α).choose #t) else 0 := by
    rintro t
    simp_rw [truncatedSup_singleton, le_iff_subset]
    split_ifs <;> simp
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
inst_2 : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#(truncatedSup {s} t)) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
      if t ⊆ s then
        HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
          (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ))
      else 0
simp_rw :
  Eq (α := ℚ) 1
    (∑ x : Finset α,
      HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#(truncatedSup {s} x)) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#x) : ℚ) * (↑((card α).choose #x) : ℚ)))
⊢ supSum (α := α) {s} = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)

Tactic:
simp_rw [← sub_eq_of_eq_add (Fintype.sum_div_mul_card_choose_card α), eq_sub_iff_add_eq,
    ← eq_sub_iff_add_eq', supSum, ← sum_sub_distrib, ← sub_div]

Premises used: eq_sub_iff_add_eq', eq_sub_iff_add_eq, sub_div, Finset.sum_sub_distrib, AhlswedeZhang.supSum, sub_eq_of_eq_add, _private.0.Fintype.sum_div_mul_card_choose_card
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
inst_2 : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#(truncatedSup {s} t)) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
      if t ⊆ s then
        HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
          (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ))
      else 0
rw :
  Eq (α := ℚ)
    (∑ j ∈ range (#s + 1),
      ∑ t ∈ powersetCard j s,
        HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
          (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)))
    (∑ i ∈ range (#s + 1),
      (↑((#s).choose i) : ℚ) * HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑i : ℚ) * (↑((card α).choose i) : ℚ)))
⊢ Eq (α := ℚ) 1
    (∑ x : Finset α,
      HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#(truncatedSup {s} x)) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#x) : ℚ) * (↑((card α).choose #x) : ℚ)))

Tactic:
rw [sum_congr rfl fun t _ ↦ this t, sum_ite, sum_const_zero, add_zero, filter_subset_univ,
    sum_powerset, ← binomial_sum_eq ((card_lt_iff_ne_univ _).2 hs), eq_comm]

Premises used: Iff.mpr, Finset.card_lt_iff_ne_univ, eq_comm, Finset.sum_const_zero, Finset.sum_powerset, Finset.filter_subset_univ, _private.0.binomial_sum_eq, add_zero, Finset.sum_congr, Finset.sum_ite, rfl
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
inst_2 : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#(truncatedSup {s} t)) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
      if t ⊆ s then
        HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
          (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ))
      else 0
⊢ Eq (α := ℚ)
    (∑ j ∈ range (#s + 1),
      ∑ t ∈ powersetCard j s,
        HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
          (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)))
    (∑ i ∈ range (#s + 1),
      (↑((#s).choose i) : ℚ) * HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑i : ℚ) * (↑((card α).choose i) : ℚ)))

Tactic:
sum_congr rfl fun n _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
inst_2 : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#(truncatedSup {s} t)) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
      if t ⊆ s then
        HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
          (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ))
      else 0
refine :
  ∀ n ∈ range (#s + 1),
    ∑ t ∈ powersetCard n s,
        HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
          (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
      (↑((#s).choose n) : ℚ) * HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ) * (↑((card α).choose n) : ℚ))
⊢ Eq (α := ℚ)
    (∑ j ∈ range (#s + 1),
      ∑ t ∈ powersetCard j s,
        HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
          (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)))
    (∑ i ∈ range (#s + 1),
      (↑((#s).choose i) : ℚ) * HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑i : ℚ) * (↑((card α).choose i) : ℚ)))

Tactic:
refine sum_congr rfl fun n _ ↦ ?_
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
inst_2 : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#(truncatedSup {s} t)) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
      if t ⊆ s then
        HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
          (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ))
      else 0
n : ℕ
h : n ∈ range (#s + 1)
rw :
  ∑ t ∈ powersetCard n s,
      HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
    (#s).choose n •
      (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ) * (↑((card α).choose n) : ℚ)))
⊢ ∑ t ∈ powersetCard n s,
      HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
    (↑((#s).choose n) : ℚ) * HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
      (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ) * (↑((card α).choose n) : ℚ))

Tactic:
rw [mul_div_assoc, ← nsmul_eq_mul]

Premises used: mul_div_assoc, nsmul_eq_mul
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
inst_2 : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#(truncatedSup {s} t)) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
      if t ⊆ s then
        HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
          (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ))
      else 0
n : ℕ
h : n ∈ range (#s + 1)
⊢ ∑ t ∈ powersetCard n s,
      HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
    (#s).choose n •
      (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ) * (↑((card α).choose n) : ℚ)))

Tactic:
sum_powersetCard n s fun m ↦ (card α - #s : ℚ) / ((card α - m) * (card α).choose m)

Premises used: Nat.choose, HMul.hMul, HSub.hSub, Fintype.card, HDiv.hDiv, Nat.cast, Finset.card, Finset.sum_powersetCard
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
inst_2 : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#(truncatedSup {s} t)) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
      if t ⊆ s then
        HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
          (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ))
      else 0
n : ℕ
h : n ∈ range (#s + 1)
⊢ ∑ t ∈ powersetCard n s,
      HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
    (#s).choose n •
      (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ) * (↑((card α).choose n) : ℚ)))

Tactic:
exact sum_powersetCard n s fun m ↦ (card α - #s : ℚ) / ((card α - m) * (card α).choose m)

Premises used: Nat.choose, HMul.hMul, HSub.hSub, Fintype.card, HDiv.hDiv, Nat.cast, Finset.card, Finset.sum_powersetCard
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
𝒜 : Finset (Finset α)
rw :
  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
⊢ HAdd.hAdd (α := ℚ)
      (∑ s : Finset α, (↑(#(𝒜ᶜˢ.truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ))
      (∑ s : Finset α,
        (↑(#(𝒜.truncatedSup s)) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ))) =
    HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹) + 1

Tactic:
rw [← @map_univ_of_surjective (Finset α) _ _ _ ⟨compl, compl_injective⟩ compl_surjective, sum_map]

Premises used: Finset.sum_map, compl_surjective, Finset.map_univ_of_surjective