awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ 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) : ℚ))
have 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) : ℚ)
Tactic: rw [← sum_add_distrib, ← sum_add_distrib, Finset.sum_congr rfl fun s _ ↦ _]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ (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) : ℚ)
have simp_rw : ∀ (s : Finset α), Membership.mem (γ := Finset (Finset α)) univ s → True
Tactic: simp_rw [← add_div, ← Nat.cast_add, card_truncatedInf_union_add_card_truncatedInf_sups]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun (x1 x2 : Finset α) ↦ x1 ⊆ x2) (↑𝒜 : Set (Finset α))
h𝒜₀ : ∅ ∉ 𝒜
⊢ ∑ s ∈ 𝒜, (↑((card α).choose #s) : ℚ)⁻¹ ≤ infSum 𝒜
have _ : Eq (α := ℚ) (∑ s ∈ 𝒜, (↑((card α).choose #s) : ℚ)⁻¹)
  (∑ s ∈ 𝒜, (↑(#(𝒜.truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ))
Tactic: calc
    _ = ∑ s ∈ 𝒜, #(truncatedInf 𝒜 s) / (#s * (card α).choose #s : ℚ) := ?_
    _ ≤ _ := sum_le_univ_sum_of_nonneg fun s ↦ by positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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) : ℚ))
have refine : ∀ (s : Finset α) (hs : s ∈ 𝒜),
  (↑((card α).choose #s) : ℚ)⁻¹ =
    (↑(#(𝒜.truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ)
Tactic: refine sum_congr rfl fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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 ∈ 𝒜
⊢ (↑((card α).choose #s) : ℚ)⁻¹ =
    (↑(#(𝒜.truncatedInf s)) : ℚ) / HMul.hMul (α := ℚ) (↑(#s) : ℚ) (↑((card α).choose #s) : ℚ)
have ha : Ne (α := ℚ) (↑(#s) : ℚ) 0
Tactic: rw [truncatedInf_of_isAntichain h𝒜 hs, div_mul_cancel_left₀]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
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 ∈ 𝒜
⊢ Ne (α := ℚ) (↑(#s) : ℚ) 0
have this : 0 < #s
Tactic: have := (nonempty_iff_ne_empty.2 <| ne_of_mem_of_not_mem hs h𝒜₀).card_pos
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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
have 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
Tactic: simp_rw [truncatedSup_singleton, le_iff_subset]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
inst_2 : Nonempty α
hs : s ≠ univ
t : Finset α
⊢ 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
have 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) : ℚ))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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) : ℚ))
⊢ 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
have neg : ¬t ⊆ s →
  HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(Finset.card.{u_1} (α := α) ⊤) : ℚ) /
      (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#t) : ℚ) * (↑((card α).choose #t) : ℚ)) =
    0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
inst_2 : Nonempty α
hs : s ≠ univ
⊢ supSum (α := α) {s} = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
have 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
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
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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
⊢ supSum (α := α) {s} = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
have simp_rw : Eq (α := ℚ) 1
  (∑ x : Finset α,
    HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#(truncatedSup {s} x)) : ℚ) /
      (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#x) : ℚ) * (↑((card α).choose #x) : ℚ)))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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 (α := ℚ) 1
    (∑ x : Finset α,
      HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#(truncatedSup {s} x)) : ℚ) /
        (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#x) : ℚ) * (↑((card α).choose #x) : ℚ)))
have 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) : ℚ)))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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) : ℚ)))
have 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) : ℚ))
Tactic: refine sum_congr rfl fun n _ ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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) : ℚ))
have 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) : ℚ)))
Tactic: rw [mul_div_assoc, ← nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
𝒜 : Finset (Finset α)
⊢ 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
have rw : HAdd.hAdd (α := ℚ)
    (∑ x : Finset α,
      (↑(#(𝒜ᶜˢ.truncatedInf (({ toFun := compl, inj' := sorry : Finset α ↪ Finset α } : (a : Finset α) → Finset α) x))) :
          ℚ) /
        HMul.hMul (α := ℚ)
          (↑(Finset.card.{u_1} (α := α)
                (({ toFun := compl, inj' := sorry : Finset α ↪ Finset α } : (a : Finset α) → Finset α) x)) :
            ℚ)
          (↑((card α).choose
                (Finset.card.{u_1} (α := α)
                  (({ toFun := compl, inj' := sorry : Finset α ↪ Finset α } : (a : Finset α) → Finset α) x))) :
            ℚ))
    (∑ s ∈ map { toFun := compl, inj' := sorry : Finset α ↪ Finset α } univ,
      (↑(#(𝒜.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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
inst_2 : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
⊢ supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
have hm : let m := #𝒜;
m = #𝒜
Tactic: set m := 𝒜.card with hm
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
inst_2 : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
m : ℕ := #𝒜
hm : m = #𝒜
⊢ supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
have clear_value : ∀ (m : ℕ) (hm : m = #𝒜), supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
Tactic: clear_value m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
𝒜 : Finset (Finset α)
inst_2 : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
m : ℕ
hm : m = #𝒜
⊢ supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
have 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 : ℚ)⁻¹)
Tactic: induction m using Nat.strongRecOn generalizing 𝒜 with | ind m ih => _
Cleared hypotheses: 𝒜, h𝒜₁, h𝒜₂, m, hm
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
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 : ℚ)⁻¹)
have ih₁ : ∀ (𝒜 : 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
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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 : ℚ)⁻¹)
⊢ supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
have 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 : ℚ)⁻¹)
Tactic: obtain ⟨a, rfl⟩ | h𝒜₃ := h𝒜₁.exists_eq_singleton_or_nontrivial
Cleared hypotheses: 𝒜, h𝒜₁, h𝒜₂, hm
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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 : ℚ)⁻¹)
⊢ supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
have ind₁ : ∀ (h𝒜₃ : 𝒜.Nontrivial), supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
Tactic: obtain ⟨a, rfl⟩ | h𝒜₃ := h𝒜₁.exists_eq_singleton_or_nontrivial
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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 : ℚ)⁻¹)
have ind : a ≠ univ
Tactic: refine supSum_singleton ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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
⊢ supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
have 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 : ℚ)⁻¹)
Tactic: cases m
Cleared hypotheses: m, hm, ih
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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 : ℚ)⁻¹)
⊢ supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
have 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 : ℚ)⁻¹)
Tactic: cases m
Cleared hypotheses: m, hm, ih
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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 : ℚ)⁻¹)
⊢ supSum 𝒜 = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
have 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 : ℚ)⁻¹)
Tactic: obtain ⟨s, 𝒜, hs, rfl, rfl⟩ := card_eq_succ.1 hm.symm
Cleared hypotheses: 𝒜, h𝒜₁, h𝒜₂, h𝒜₃, n, hm, ih
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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
have 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
Tactic: by_contra! rfl
Cleared hypotheses: 𝒜, hs, h𝒜₁, h𝒜₂, h𝒜₃, ih, hm
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
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 𝒜)
⊢ supSum (insert s 𝒜) = HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹)
have h𝒜 : 𝒜.Nonempty
Tactic: have h𝒜 : 𝒜.Nonempty := by by_contra! rfl; simp at h𝒜₃