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 : Nonempty α
⊢ ∑ s : Finset α, (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) =
    HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹) + 1
have 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
Tactic: rw [← powerset_univ, powerset_card_disjiUnion, sum_disjiUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
n : ℕ
s : Finset α
hs : Membership.mem (γ := Finset (Finset α)) (powersetCard n univ) s
⊢ (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑(#s) : ℚ) * (↑((card α).choose #s) : ℚ)) =
    (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ) * (↑((card α).choose n) : ℚ))
have rw : (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ) * (↑((card α).choose n) : ℚ)) =
  (↑(card α) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑n : ℚ) * (↑((card α).choose n) : ℚ))
Tactic: rw [mem_powersetCard_univ.1 hs]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Nonempty α
⊢ ∑ 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
have 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) : ℚ))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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) : ℚ))
⊢ ∑ 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
have 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
Tactic: simp_rw [Finset.sum_congr rfl this, sum_const, card_powersetCard, card_univ, nsmul_eq_mul,
    mul_div, mul_comm, ← mul_div]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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) : ℚ))
⊢ ∑ x ∈ range (card α + 1),
      (↑(card α) : ℚ) *
        ((↑((card α).choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ) * (↑((card α).choose x) : ℚ))) =
    HMul.hMul (α := ℚ) (↑(card α) : ℚ) (∑ k ∈ range (card α), (↑k : ℚ)⁻¹) + 1
have 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 : ℚ)⁻¹)
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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 : ℚ))⁻¹
have hb : Ne (α := ℚ) (↑((card α).choose n) : ℚ) 0
Tactic: rw [div_mul_cancel_right₀]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
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) : ℚ))
⊢ 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 : ℚ)⁻¹)
have this₁ : ∀ (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'
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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 : ℚ))⁻¹
⊢ 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 : ℚ)⁻¹)
have simp : Eq (α := ℚ) (∑ x ∈ range (card α + 1), (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ))⁻¹)
    (∑ x ∈ range (card α + 1), (↑x : ℚ)⁻¹) ∨
  card α = 0
Tactic: simp only [Finset.sum_congr rfl this, mul_eq_mul_left_iff, cast_eq_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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 (α := ℚ) (∑ x ∈ range (card α + 1), (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑x : ℚ))⁻¹)
      (∑ x ∈ range (card α + 1), (↑x : ℚ)⁻¹) ∨
    card α = 0
have h : ∀ (a : ℕ) (ha : a ∈ range (card α + 1)), (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑a : ℚ))⁻¹ = (↑(card α + 1 - 1 - a) : ℚ)⁻¹
Tactic: convert! Or.inl <| sum_range_reflect _ _ with a ha
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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)
⊢ (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑a : ℚ))⁻¹ = (↑(card α + 1 - 1 - a) : ℚ)⁻¹
have h : (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑a : ℚ))⁻¹ = (↑(card α - a) : ℚ)⁻¹
Tactic: rw [add_tsub_cancel_right, cast_sub (mem_range_succ_iff.mp ha)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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) : ℚ)⁻¹
⊢ (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑a : ℚ))⁻¹ = (↑(card α + 1 - 1 - a) : ℚ)⁻¹
have h₁ : (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑a : ℚ))⁻¹ = (HSub.hSub (α := ℚ) (↑(card α) : ℚ) (↑a : ℚ))⁻¹
Tactic: rw [add_tsub_cancel_right, cast_sub (mem_range_succ_iff.mp ha)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
s t : Finset α
a : α
inst_1 : DecidableEq α
⊢ Membership.mem (γ := LowerSet α) (lowerClosure (↑(s ∪ t) : Set α)) a ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∨
      Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
have rw : Membership.mem (γ := LowerSet α) (lowerClosure ((↑s : Set α) ∪ (↑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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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
⊢ Membership.mem (γ := LowerSet α) (lowerClosure (↑(s ∪ t) : Set α)) a ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∨
      Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
have 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
Tactic: rw [coe_union, lowerClosure_union, LowerSet.mem_sup_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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
⊢ Membership.mem (γ := LowerSet α) (lowerClosure (↑(s ∪ t) : Set α)) a ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a ∨
      Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
have 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
Tactic: rw [coe_union, lowerClosure_union, LowerSet.mem_sup_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : DecidableLE α
inst_2 : OrderTop α
b a : α
⊢ truncatedSup {b} a = if a ≤ b then b else ⊤
have simp : (if a ≤ b then sup' ({b ∈ {b} | a ≤ b}) sorry fun (x : α) ↦ x else ⊤) = if a ≤ b then b else ⊤
Tactic: simp [truncatedSup]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : DecidableLE α
inst_2 : OrderTop α
b a : α
⊢ (if a ≤ b then sup' ({b ∈ {b} | a ≤ b}) ⋯ fun (x : α) ↦ x else ⊤) = if a ≤ b then b else ⊤
have pos : a ≤ b → (sup' ({b ∈ {b} | a ≤ b}) sorry fun (x : α) ↦ x) = b
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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
⊢ (if a ≤ b then sup' ({b ∈ {b} | a ≤ b}) ⋯ fun (x : α) ↦ x else ⊤) = if a ≤ b then b else ⊤
have neg : ¬a ≤ b → Eq.{u_1 + 1} (α := α) ⊤ ⊤
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
⊢ a ≤ s.truncatedSup a
have rw : a ≤ if h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a then {b ∈ s | a ≤ b}.sup' sorry id else ⊤
Tactic: rw [truncatedSup]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
⊢ a ≤ if h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a then {b ∈ s | a ≤ b}.sup' ⋯ id else ⊤
have pos : ∀ (h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a), a ≤ {b ∈ s | a ≤ b}.sup' sorry id
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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
⊢ a ≤ if h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a then {b ∈ s | a ≤ b}.sup' ⋯ id else ⊤
have neg : ∀ (h : a ∉ lowerClosure (↑s : Set α)), a ≤ ⊤
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
⊢ a ≤ {b ∈ s | a ≤ b}.sup' ⋯ id
have pos : ∀ (ℬ : α) (hb : ℬ ∈ (↑s : Set α)) (h : a ≤ ℬ), a ≤ {b ∈ s | a ≤ b}.sup' sorry id
Tactic: obtain ⟨ℬ, hb, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : BoundedOrder β
inst_3 : DecidableLE α
inst_4 : OrderTop α
inst_5 : DecidableLE β
e : α ≃o β
s : Finset α
a : α
⊢ (e : (a : α) → β) (s.truncatedSup a) =
    (map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s).truncatedSup
      ((e : (a : α) → β) a)
have this : Membership.mem (α := β) (γ := LowerSet β)
    (lowerClosure
      (↑(map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s) : Set β))
    ((e : (a : α) → β) a : β) ↔
  Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
Tactic: have : e a ∈ lowerClosure (s.map e.toEquiv.toEmbedding : Set β) ↔ a ∈ lowerClosure s := by simp
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : BoundedOrder β
inst_3 : DecidableLE α
inst_4 : OrderTop α
inst_5 : DecidableLE β
e : α ≃o β
s : Finset α
a : α
this :
  Membership.mem (α := β) (γ := LowerSet β)
      (lowerClosure
        (↑(map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s) : Set β))
      ((e : (a : α) → β) a : β) ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
⊢ (e : (a : α) → β) (s.truncatedSup a) =
    (map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s).truncatedSup
      ((e : (a : α) → β) a)
have simp_rw : Eq.{u_2 + 1} (α := β)
  (if h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a then
    {b ∈ s | a ≤ b}.sup' sorry ((⇑e : (a : α) → β) ∘ id)
  else ⊤)
  (if h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a then
    {b ∈ map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s |
          (e : (a : α) → β) a ≤ b}.sup'
      sorry id
  else ⊤)
Tactic: simp_rw [truncatedSup, apply_dite e, map_finset_sup', map_top, this]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : BoundedOrder β
inst_3 : DecidableLE α
inst_4 : OrderTop α
inst_5 : DecidableLE β
e : α ≃o β
s : Finset α
a : α
this :
  Membership.mem (α := β) (γ := LowerSet β)
      (lowerClosure
        (↑(map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s) : Set β))
      ((e : (a : α) → β) a : β) ↔
    Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
⊢ Eq.{u_2 + 1} (α := β)
    (if h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a then
      {b ∈ s | a ≤ b}.sup' ⋯ ((⇑e : (a : α) → β) ∘ id)
    else ⊤)
    (if h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a then
      {b ∈ map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s |
            (e : (a : α) → β) a ≤ b}.sup'
        ⋯ id
    else ⊤)
have e_t : ∀ (h : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a),
  {b ∈ s | a ≤ b}.sup' sorry ((⇑e : (a : α) → β) ∘ id) =
    {b ∈ map e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toEmbedding s |
          (e : (a : α) → β) a ≤ b}.sup'
      sorry id
Tactic: congr with h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) (↑s : Set α)
ha : a ∈ s
⊢ s.truncatedSup a = a
have refine : s.truncatedSup a ≤ a
Tactic: refine le_antisymm ?_ le_truncatedSup
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
s : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) (↑s : Set α)
ha : a ∈ s
⊢ s.truncatedSup a ≤ a
have simp_rw : ∀ (b : α), b ∈ s ∧ a ≤ b → id b ≤ a
Tactic: simp_rw [truncatedSup_of_mem (subset_lowerClosure ha), sup'_le_iff, mem_filter]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
Goal:
α : Type u_1
inst : SemilatticeSup α
s t : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
inst_3 : DecidableEq α
hs : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
ht : a ∉ lowerClosure (↑t : Set α)
⊢ (s ∪ t).truncatedSup a = s.truncatedSup a
have ht₁ : ∀ x ∈ t, ¬a ≤ x
Tactic: simp only [mem_lowerClosure, mem_coe, not_exists, not_and] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
s t : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
inst_3 : DecidableEq α
hs : a ∉ lowerClosure (↑s : Set α)
ht : Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
⊢ (s ∪ t).truncatedSup a = t.truncatedSup a
have rw : (t ∪ s).truncatedSup a = t.truncatedSup a
Tactic: rw [union_comm, truncatedSup_union_left ht hs]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
s t : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : OrderTop α
inst_3 : DecidableEq α
hs : a ∉ lowerClosure (↑s : Set α)
ht : Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
rw : (t ∪ s).truncatedSup a = t.truncatedSup a
⊢ (s ∪ t).truncatedSup a = t.truncatedSup a
have rw₁ : t.truncatedSup a = t.truncatedSup a
Tactic: rw [union_comm, truncatedSup_union_left ht hs]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
s t : Finset α
a : α
inst_1 : DecidableEq α
⊢ Membership.mem (γ := UpperSet α) (upperClosure (↑(s ∪ t) : Set α)) a ↔
    Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∨
      Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
have rw : Membership.mem (γ := UpperSet α) (upperClosure ((↑s : Set α) ∪ (↑t : Set α))) a ↔
  Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∨
    Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
Tactic: rw [coe_union, upperClosure_union, UpperSet.mem_inf_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
s t : Finset α
a : α
inst_1 : DecidableEq α
rw :
  Membership.mem (γ := UpperSet α) (upperClosure ((↑s : Set α) ∪ (↑t : Set α))) a ↔
    Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∨
      Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
⊢ Membership.mem (γ := UpperSet α) (upperClosure (↑(s ∪ t) : Set α)) a ↔
    Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∨
      Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
have rw₁ : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α) ⊓ upperClosure (↑t : Set α)) a ↔
  Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∨
    Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
Tactic: rw [coe_union, upperClosure_union, UpperSet.mem_inf_iff]