awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
i : ℕ
h₁_1 : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
this : (↑(m.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ)
rw :
  HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹ -
      (↑(n.choose (i + 1)) : ℚ) *
        (HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ) * (HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)⁻¹)⁻¹ =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
⊢ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹ -
      HMul.hMul (α := ℚ) (↑(n.choose (i + 1)) : ℚ) (↑(m.choose (i + 1)) : ℚ)⁻¹ =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))

Tactic:
rw [(eq_mul_inv_iff_mul_eq₀ hi₄).mpr this]

Premises used: Iff.mpr, eq_mul_inv_iff_mul_eq₀
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
i : ℕ
h₁_1 : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
this : (↑(m.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ)
⊢ Eq (α := ℚ) (↑(n.choose (i + 1) * (i + 1)) : ℚ) (↑(n.choose i * (n - i)) : ℚ)

Tactic:
have := congr_arg ((↑) : ℕ → ℚ) (choose_succ_right_eq n i)
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
i : ℕ
h₁_1 : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
this_1 :
  (↑(m.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ)
this : Eq (α := ℚ) (↑(n.choose (i + 1) * (i + 1)) : ℚ) (↑(n.choose i * (n - i)) : ℚ)
⊢ (↑(n.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(n - i) : ℚ)

Tactic:
push_cast at this
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
i : ℕ
h₁_1 : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
this_1 :
  (↑(m.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ)
this : (↑(n.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(n - i) : ℚ)
rw :
  HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹ -
      HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(n - i) : ℚ) * (HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)⁻¹ *
        (HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ) * (HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)⁻¹)⁻¹ =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
⊢ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹ -
      (↑(n.choose (i + 1)) : ℚ) *
        (HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ) * (HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)⁻¹)⁻¹ =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))

Tactic:
rw [(eq_mul_inv_iff_mul_eq₀ hi₄).mpr this]

Premises used: Iff.mpr, eq_mul_inv_iff_mul_eq₀
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
i : ℕ
h₁_1 : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
this_1 :
  (↑(m.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ)
this : (↑(n.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(n - i) : ℚ)
⊢ HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) ≠ 0

Tactic:
have : (m - i : ℚ) ≠ 0 := sub_ne_zero_of_ne (cast_lt.mpr h₂).ne'
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
i : ℕ
h₁_1 : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
this_1 :
  (↑(m.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ)
this_2 :
  (↑(n.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(n - i) : ℚ)
this : HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) ≠ 0
⊢ Ne (α := ℚ) (↑(m.choose i) : ℚ) 0

Tactic:
have : (m.choose i : ℚ) ≠ 0 := cast_ne_zero.2 (choose_pos h₂.le).ne'
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
i : ℕ
h₁_1 : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
this_1 :
  (↑(m.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ)
this_2 :
  (↑(n.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(n - i) : ℚ)
this_3 : HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) ≠ 0
this : Ne (α := ℚ) (↑(m.choose i) : ℚ) 0
⊢ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹ -
      HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(n - i) : ℚ) * (HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)⁻¹ *
        (HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ) * (HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)⁻¹)⁻¹ =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))

Tactic:
simp [field, *]
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
rw :
  ∑ i ∈ range (Finset.card.{u_1} (α := α) univ + 1),
      ∑ x ∈ powersetCard i univ,
        (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#x) : ℚ) * (↑((card α).choose #x) : ℚ)) =
    HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹) + 1
⊢ ∑ s : Finset α, (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) =
    HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹) + 1

Tactic:
rw [← powerset_univ, powerset_card_disjiUnion, sum_disjiUnion]

Premises used: Finset.powerset_card_disjiUnion, Finset.powerset_univ, Finset.sum_disjiUnion
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
n : ℕ
s : Finset α
hs : Membership.mem (γ := Finset (Finset α)) (powersetCard n univ) s
rw rw₁ :
  (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ) * (↑((card α).choose n) : ℚ)) =
    (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ) * (↑((card α).choose n) : ℚ))
⊢ (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) =
    (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ) * (↑((card α).choose n) : ℚ))

Tactic:
rw [mem_powersetCard_univ.1 hs]

Premises used: Finset.mem_powersetCard_univ, Iff.mp
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
⊢ ∀ {x : ℕ} (s : Finset α),
    Membership.mem (γ := Finset (Finset α)) (powersetCard x univ) s →
      (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) =
        (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ) * (↑((card α).choose x) : ℚ))

Tactic:
have : ∀ {x : ℕ}, ∀ s ∈ powersetCard x (univ : Finset α),
    (card α / ((card α - #s) * (card α).choose #s) : ℚ) =
      card α / ((card α - x) * (card α).choose x) := by
    intro n s hs
    rw [mem_powersetCard_univ.1 hs]
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
this :
  ∀ {x : ℕ} (s : Finset α),
    Membership.mem (γ := Finset (Finset α)) (powersetCard x univ) s →
      (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) =
        (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ) * (↑((card α).choose x) : ℚ))
simp_rw :
  ∑ x ∈ range (card α + 1),
      (↑(card α) : ℚ) *
        ((↑((card α).choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ) * (↑((card α).choose x) : ℚ))) =
    HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹) + 1
⊢ ∑ i ∈ range (Finset.card.{u_1} (α := α) univ + 1),
      ∑ x ∈ powersetCard i univ,
        (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#x) : ℚ) * (↑((card α).choose #x) : ℚ)) =
    HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹) + 1

Tactic:
simp_rw [Finset.sum_congr rfl this, sum_const, card_powersetCard, card_univ, nsmul_eq_mul,
    mul_div, mul_comm, ← mul_div]

Premises used: mul_div, Finset.card_univ, mul_comm, nsmul_eq_mul, Finset.card_powersetCard, Finset.sum_congr, rfl, Finset.sum_const
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
this :
  ∀ {x : ℕ} (s : Finset α),
    Membership.mem (γ := Finset (Finset α)) (powersetCard x univ) s →
      (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) =
        (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ) * (↑((card α).choose x) : ℚ))
rw :
  HMul.hMul (α := ℚ) (↑(card α) : ℚ)
      (∑ i ∈ range (card α + 1),
        (↑((card α).choose i) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑i : ℚ) * (↑((card α).choose i) : ℚ))) =
    HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ x ∈ range (card α + 1), (↑x : ℚ)⁻¹)
⊢ ∑ x ∈ range (card α + 1),
      (↑(card α) : ℚ) *
        ((↑((card α).choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ) * (↑((card α).choose x) : ℚ))) =
    HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹) + 1

Tactic:
rw [← mul_sum, ← mul_inv_cancel₀ (cast_ne_zero.mpr card_ne_zero : (card α : ℚ) ≠ 0), ← mul_add,
    add_comm _ ((card α)⁻¹ : ℚ), ← sum_insert (f := fun x : ℕ ↦ (x⁻¹ : ℚ)) notMem_range_self,
    ← range_add_one]

Premises used: Iff.mpr, Finset.mul_sum, mul_inv_cancel₀, Fintype.card, Finset.range_add_one, Nat.cast, add_comm, Fintype.card_ne_zero, Inv.inv, Finset.notMem_range_self, mul_add, Finset.sum_insert, Nat.cast_ne_zero
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
this :
  ∀ {x : ℕ} (s : Finset α),
    Membership.mem (γ := Finset (Finset α)) (powersetCard x univ) s →
      (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) =
        (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ) * (↑((card α).choose x) : ℚ))
n : ℕ
hn : n ∈ range (card α + 1)
hb : Ne (α := ℚ) (↑((card α).choose n) : ℚ) 0
⊢ (↑((card α).choose n) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ) * (↑((card α).choose n) : ℚ)) =
    (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ))⁻¹

Tactic:
rw [div_mul_cancel_right₀]

Premises used: div_mul_cancel_right₀
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
this :
  ∀ {x : ℕ} (s : Finset α),
    Membership.mem (γ := Finset (Finset α)) (powersetCard x univ) s →
      (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) =
        (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ) * (↑((card α).choose x) : ℚ))
n : ℕ
hn : n ∈ range (card α + 1)
⊢ Ne (α := ℚ) (↑((card α).choose n) : ℚ) 0

Tactic:
cast_ne_zero.2 (choose_pos <| mem_range_succ_iff.1 hn).ne'

Premises used: Iff.mpr, Finset.mem_range_succ_iff, LT.lt.ne', Nat.choose_pos, Iff.mp, Nat.cast_ne_zero
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
this :
  ∀ {x : ℕ} (s : Finset α),
    Membership.mem (γ := Finset (Finset α)) (powersetCard x univ) s →
      (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) =
        (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ) * (↑((card α).choose x) : ℚ))
n : ℕ
hn : n ∈ range (card α + 1)
⊢ Ne (α := ℚ) (↑((card α).choose n) : ℚ) 0

Tactic:
exact cast_ne_zero.2 (choose_pos <| mem_range_succ_iff.1 hn).ne'

Premises used: Iff.mpr, Finset.mem_range_succ_iff, LT.lt.ne', Nat.choose_pos, Iff.mp, Nat.cast_ne_zero
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
this :
  ∀ {x : ℕ} (s : Finset α),
    Membership.mem (γ := Finset (Finset α)) (powersetCard x univ) s →
      (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) =
        (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ) * (↑((card α).choose x) : ℚ))
⊢ ∀ (n : ℕ) (hn : n ∈ range (card α + 1)),
    (↑((card α).choose n) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ) * (↑((card α).choose n) : ℚ)) =
      (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ))⁻¹

Tactic:
have (n) (hn : n ∈ range (card α + 1)) :
      ((card α).choose n / ((card α - n) * (card α).choose n) : ℚ) = (card α - n : ℚ)⁻¹ := by
    rw [div_mul_cancel_right₀]
    exact cast_ne_zero.2 (choose_pos <| mem_range_succ_iff.1 hn).ne'
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
this_1 :
  ∀ {x : ℕ} (s : Finset α),
    Membership.mem (γ := Finset (Finset α)) (powersetCard x univ) s →
      (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) =
        (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ) * (↑((card α).choose x) : ℚ))
this :
  ∀ (n : ℕ) (hn : n ∈ range (card α + 1)),
    (↑((card α).choose n) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ) * (↑((card α).choose n) : ℚ)) =
      (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ))⁻¹
simp :
  Eq (α := ℚ) (∑ x ∈ range (card α + 1), (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ))⁻¹)
      (∑ x ∈ range (card α + 1), (↑x : ℚ)⁻¹) ∨
    card α = 0
⊢ HMul.hMul (α := ℚ) (↑(card α) : ℚ)
      (∑ i ∈ range (card α + 1),
        (↑((card α).choose i) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑i : ℚ) * (↑((card α).choose i) : ℚ))) =
    HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ x ∈ range (card α + 1), (↑x : ℚ)⁻¹)

Tactic:
simp only [Finset.sum_congr rfl this, mul_eq_mul_left_iff, cast_eq_zero]

Premises used: mul_eq_mul_left_iff, Nat.cast_eq_zero, Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
this_1 :
  ∀ {x : ℕ} (s : Finset α),
    Membership.mem (γ := Finset (Finset α)) (powersetCard x univ) s →
      (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) =
        (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ) * (↑((card α).choose x) : ℚ))
this :
  ∀ (n : ℕ) (hn : n ∈ range (card α + 1)),
    (↑((card α).choose n) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ) * (↑((card α).choose n) : ℚ)) =
      (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ))⁻¹
⊢ Eq (α := ℚ) (∑ j ∈ range (card α + 1), (↑(card α + 1 - 1 - j) : ℚ)⁻¹) (∑ j ∈ range (card α + 1), (↑j : ℚ)⁻¹) ∨
    card α = 0

Tactic:
Or.inl <| sum_range_reflect _ _

Premises used: Finset.sum_range_reflect, Or.inl
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
this_1 :
  ∀ {x : ℕ} (s : Finset α),
    Membership.mem (γ := Finset (Finset α)) (powersetCard x univ) s →
      (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) =
        (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ) * (↑((card α).choose x) : ℚ))
this :
  ∀ (n : ℕ) (hn : n ∈ range (card α + 1)),
    (↑((card α).choose n) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ) * (↑((card α).choose n) : ℚ)) =
      (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ))⁻¹
h :
  ∀ (a : ℕ) (ha : a ∈ range (card α + 1)),
    (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑a : ℚ))⁻¹ = (↑(card α + 1 - 1 - a) : ℚ)⁻¹
⊢ Eq (α := ℚ) (∑ x ∈ range (card α + 1), (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ))⁻¹)
      (∑ x ∈ range (card α + 1), (↑x : ℚ)⁻¹) ∨
    card α = 0

Tactic:
convert! Or.inl <| sum_range_reflect _ _ with a ha

Premises used: Finset.sum_range_reflect, Or.inl
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
this_1 :
  ∀ {x : ℕ} (s : Finset α),
    Membership.mem (γ := Finset (Finset α)) (powersetCard x univ) s →
      (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) =
        (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ) * (↑((card α).choose x) : ℚ))
this :
  ∀ (n : ℕ) (hn : n ∈ range (card α + 1)),
    (↑((card α).choose n) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ) * (↑((card α).choose n) : ℚ)) =
      (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ))⁻¹
a : ℕ
ha : a ∈ range (card α + 1)
h : (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑a : ℚ))⁻¹ = (↑(card α - a) : ℚ)⁻¹
h₁ h₂ : (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑a : ℚ))⁻¹ = (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑a : ℚ))⁻¹
⊢ (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑a : ℚ))⁻¹ = (↑(card α + 1 - 1 - a) : ℚ)⁻¹

Tactic:
rw [add_tsub_cancel_right, cast_sub (mem_range_succ_iff.mp ha)]

Premises used: Nat.cast_sub, Finset.mem_range_succ_iff, Iff.mp, add_tsub_cancel_right
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
⊢ Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a → {b ∈ s | a ≤ b}.Nonempty

Tactic:
fun ⟨b, hb, hab⟩ ↦ ⟨b, mem_filter.2 ⟨hb, hab⟩⟩

Premises used: Iff.mpr, LE.le, And.intro, _private.0.Finset.sup_aux.match_1, Exists.intro, Finset.Nonempty, Finset.mem_filter, Finset.filter
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s t : Finset α
a : α
inst_1 : DecidableEq α
rw :
  Membership.mem (γ := LowerSet α) (lowerClosure ((↑s : Set α) ∪ (↑t : Set α))) a ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∨
      Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
rw₁ :
  Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α) ⊔ lowerClosure (↑t : Set α)) a ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∨
      Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
rw₂ rw₃ :
  Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∨
      Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∨
      Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
⊢ Membership.mem (γ := LowerSet α) (lowerClosure (↑(s ∪ t) : Set α)) a ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∨
      Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a

Tactic:
rw [coe_union, lowerClosure_union, LowerSet.mem_sup_iff]

Premises used: lowerClosure_union, Finset.coe_union, LowerSet.mem_sup_iff
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
⊢ s.truncatedSup a = {b ∈ s | a ≤ b}.sup' ⋯ id

Tactic:
dif_pos h

Premises used: dif_pos, Finset.truncatedSup
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
h : a ∉ lowerClosure (↑s : Set α)
⊢ s.truncatedSup a = ⊤

Tactic:
dif_neg h

Premises used: dif_neg, Finset.truncatedSup
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : DecidableLE α
inst_2 : OrderTop α
a : α
⊢ a ∉ lowerClosure (↑∅ : Set α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : DecidableLE α
inst_2 : OrderTop α
b a : α
simp : (if a ≤ b then sup' ({b ∈ {b} | a ≤ b}) ⋯ fun (x : α) ↦ x else ⊤) = if a ≤ b then b else ⊤
⊢ truncatedSup {b} a = if a ≤ b then b else ⊤

Tactic:
simp [truncatedSup]

Premises used: Finset.truncatedSup
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : DecidableLE α
inst_2 : OrderTop α
b a : α
pos : a ≤ b → (sup' ({b ∈ {b} | a ≤ b}) ⋯ fun (x : α) ↦ x) = b
neg : ¬a ≤ b → Eq.{u_1 + 1} (α := α) ⊤ ⊤
⊢ (if a ≤ b then sup' ({b ∈ {b} | a ≤ b}) ⋯ fun (x : α) ↦ x else ⊤) = if a ≤ b then b else ⊤

Tactic:
split_ifs
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : DecidableLE α
inst_2 : OrderTop α
b a : α
h : a ≤ b
⊢ (sup' ({b ∈ {b} | a ≤ b}) ⋯ fun (x : α) ↦ x) = b

Tactic:
simp [Finset.filter_true_of_mem, *]

Premises used: Finset.filter_true_of_mem
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : DecidableLE α
inst_2 : OrderTop α
b a : α
h : ¬a ≤ b
⊢ Eq.{u_1 + 1} (α := α) ⊤ ⊤

Tactic:
simp [Finset.filter_true_of_mem, *]

Premises used: Finset.filter_true_of_mem
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
rw : a ≤ if h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a then {b ∈ s | a ≤ b}.sup' ⋯ id else ⊤
⊢ a ≤ s.truncatedSup a

Tactic:
rw [truncatedSup]

Premises used: Finset.truncatedSup
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
pos : ∀ (h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a), a ≤ {b ∈ s | a ≤ b}.sup' ⋯ id
neg : ∀ (h : a ∉ lowerClosure (↑s : Set α)), a ≤ ⊤
⊢ a ≤ if h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a then {b ∈ s | a ≤ b}.sup' ⋯ id else ⊤

Tactic:
split_ifs with h
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
pos : ∀ (ℬ : α) (hb : ℬ ∈ (↑s : Set α)) (h : a ≤ ℬ), a ≤ {b ∈ s | a ≤ b}.sup' ⋯ id
⊢ a ≤ {b ∈ s | a ≤ b}.sup' ⋯ id

Tactic:
obtain ⟨ℬ, hb, h⟩ := h
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
ℬ : α
hb : ℬ ∈ (↑s : Set α)
h : a ≤ ℬ
⊢ a ≤ {b ∈ s | a ≤ b}.sup' ⋯ id

Tactic:
h.trans <| le_sup' id <| mem_filter.2 ⟨hb, h⟩

Premises used: Iff.mpr, id, And.intro, Finset.mem_filter, LE.le.trans, Finset.le_sup'
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
ℬ : α
hb : ℬ ∈ (↑s : Set α)
h : a ≤ ℬ
⊢ a ≤ {b ∈ s | a ≤ b}.sup' ⋯ id

Tactic:
exact h.trans <| le_sup' id <| mem_filter.2 ⟨hb, h⟩

Premises used: Iff.mpr, id, And.intro, Finset.mem_filter, LE.le.trans, Finset.le_sup'
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
h : a ∉ lowerClosure (↑s : Set α)
⊢ a ≤ ⊤

Tactic:
le_top

Premises used: le_top