awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑𝒜 : Set (Finset α))) s
hℬ : s ∉ lowerClosure (↑ℬ : Set (Finset α))
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have neg : #(𝒜.truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
Tactic: rw [truncatedSup_union_left h𝒜 hℬ, truncatedSup_of_notMem hℬ,
      truncatedSup_infs_of_notMem fun h ↦ hℬ h.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑𝒜 : Set (Finset α))) s
hℬ : s ∉ lowerClosure (↑ℬ : Set (Finset α))
neg : #(𝒜.truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have neg₁ : #(𝒜.truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + card.{u_1} (α := α) ⊤
Tactic: rw [truncatedSup_union_left h𝒜 hℬ, truncatedSup_of_notMem hℬ,
      truncatedSup_infs_of_notMem fun h ↦ hℬ h.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑𝒜 : Set (Finset α))) s
hℬ : s ∉ lowerClosure (↑ℬ : Set (Finset α))
neg : #(𝒜.truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
neg₁ : #(𝒜.truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + card.{u_1} (α := α) ⊤
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have neg₂ : #(𝒜.truncatedSup s) + card.{u_1} (α := α) ⊤ = #(𝒜.truncatedSup s) + card.{u_1} (α := α) ⊤
Tactic: rw [truncatedSup_union_left h𝒜 hℬ, truncatedSup_of_notMem hℬ,
      truncatedSup_infs_of_notMem fun h ↦ hℬ h.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure (↑𝒜 : Set (Finset α))
hℬ : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑ℬ : Set (Finset α))) s
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have pos : #(ℬ.truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
Tactic: rw [truncatedSup_union_right h𝒜 hℬ, truncatedSup_of_notMem h𝒜,
      truncatedSup_infs_of_notMem fun h ↦ h𝒜 h.1, add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure (↑𝒜 : Set (Finset α))
hℬ : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑ℬ : Set (Finset α))) s
pos : #(ℬ.truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have pos₁ : #(ℬ.truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = card.{u_1} (α := α) ⊤ + #(ℬ.truncatedSup s)
Tactic: rw [truncatedSup_union_right h𝒜 hℬ, truncatedSup_of_notMem h𝒜,
      truncatedSup_infs_of_notMem fun h ↦ h𝒜 h.1, add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure (↑𝒜 : Set (Finset α))
hℬ : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑ℬ : Set (Finset α))) s
pos : #(ℬ.truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
pos₁ : #(ℬ.truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = card.{u_1} (α := α) ⊤ + #(ℬ.truncatedSup s)
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have pos₂ : #(ℬ.truncatedSup s) + card.{u_1} (α := α) ⊤ = card.{u_1} (α := α) ⊤ + #(ℬ.truncatedSup s)
Tactic: rw [truncatedSup_union_right h𝒜 hℬ, truncatedSup_of_notMem h𝒜,
      truncatedSup_infs_of_notMem fun h ↦ h𝒜 h.1, add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure (↑𝒜 : Set (Finset α))
hℬ : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑ℬ : Set (Finset α))) s
pos : #(ℬ.truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
pos₁ : #(ℬ.truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = card.{u_1} (α := α) ⊤ + #(ℬ.truncatedSup s)
pos₂ : #(ℬ.truncatedSup s) + card.{u_1} (α := α) ⊤ = card.{u_1} (α := α) ⊤ + #(ℬ.truncatedSup s)
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have pos₃ : card.{u_1} (α := α) ⊤ + #(ℬ.truncatedSup s) = card.{u_1} (α := α) ⊤ + #(ℬ.truncatedSup s)
Tactic: rw [truncatedSup_union_right h𝒜 hℬ, truncatedSup_of_notMem h𝒜,
      truncatedSup_infs_of_notMem fun h ↦ h𝒜 h.1, add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure (↑𝒜 : Set (Finset α))
hℬ : s ∉ lowerClosure (↑ℬ : Set (Finset α))
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have neg : #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = card.{u_1} (α := α) ⊤ + #(ℬ.truncatedSup s)
Tactic: rw [truncatedSup_of_notMem h𝒜, truncatedSup_of_notMem hℬ,
      truncatedSup_union_of_notMem h𝒜 hℬ, truncatedSup_infs_of_notMem fun h ↦ h𝒜 h.1]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure (↑𝒜 : Set (Finset α))
hℬ : s ∉ lowerClosure (↑ℬ : Set (Finset α))
neg : #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = card.{u_1} (α := α) ⊤ + #(ℬ.truncatedSup s)
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have neg₁ : #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = card.{u_1} (α := α) ⊤ + card.{u_1} (α := α) ⊤
Tactic: rw [truncatedSup_of_notMem h𝒜, truncatedSup_of_notMem hℬ,
      truncatedSup_union_of_notMem h𝒜 hℬ, truncatedSup_infs_of_notMem fun h ↦ h𝒜 h.1]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure (↑𝒜 : Set (Finset α))
hℬ : s ∉ lowerClosure (↑ℬ : Set (Finset α))
neg : #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = card.{u_1} (α := α) ⊤ + #(ℬ.truncatedSup s)
neg₁ : #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = card.{u_1} (α := α) ⊤ + card.{u_1} (α := α) ⊤
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have neg₂ : card.{u_1} (α := α) ⊤ + #((𝒜 ⊼ ℬ).truncatedSup s) = card.{u_1} (α := α) ⊤ + card.{u_1} (α := α) ⊤
Tactic: rw [truncatedSup_of_notMem h𝒜, truncatedSup_of_notMem hℬ,
      truncatedSup_union_of_notMem h𝒜 hℬ, truncatedSup_infs_of_notMem fun h ↦ h𝒜 h.1]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure (↑𝒜 : Set (Finset α))
hℬ : s ∉ lowerClosure (↑ℬ : Set (Finset α))
neg : #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = card.{u_1} (α := α) ⊤ + #(ℬ.truncatedSup s)
neg₁ : #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = card.{u_1} (α := α) ⊤ + card.{u_1} (α := α) ⊤
neg₂ : card.{u_1} (α := α) ⊤ + #((𝒜 ⊼ ℬ).truncatedSup s) = card.{u_1} (α := α) ⊤ + card.{u_1} (α := α) ⊤
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
have neg₃ : card.{u_1} (α := α) ⊤ + card.{u_1} (α := α) ⊤ = card.{u_1} (α := α) ⊤ + card.{u_1} (α := α) ⊤
Tactic: rw [truncatedSup_of_notMem h𝒜, truncatedSup_of_notMem hℬ,
      truncatedSup_union_of_notMem h𝒜 hℬ, truncatedSup_infs_of_notMem fun h ↦ h𝒜 h.1]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have pos : ∀ (h𝒜 : Membership.mem (γ := UpperSet (Finset α)) (upperClosure (↑𝒜 : Set (Finset α))) s),
  #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
Tactic: by_cases h𝒜 : s ∈ upperClosure (𝒜 : Set <| Finset α)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
pos :
  ∀ (h𝒜 : Membership.mem (γ := UpperSet (Finset α)) (upperClosure (↑𝒜 : Set (Finset α))) s),
    #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have neg : ∀ (h𝒜 : s ∉ upperClosure (↑𝒜 : Set (Finset α))),
  #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
Tactic: by_cases h𝒜 : s ∈ upperClosure (𝒜 : Set <| Finset α)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : Membership.mem (γ := UpperSet (Finset α)) (upperClosure (↑𝒜 : Set (Finset α))) s
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have pos : ∀ (hℬ : Membership.mem (γ := UpperSet (Finset α)) (upperClosure (↑ℬ : Set (Finset α))) s),
  #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
Tactic: by_cases hℬ : s ∈ upperClosure (ℬ : Set <| Finset α)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : Membership.mem (γ := UpperSet (Finset α)) (upperClosure (↑𝒜 : Set (Finset α))) s
pos :
  ∀ (hℬ : Membership.mem (γ := UpperSet (Finset α)) (upperClosure (↑ℬ : Set (Finset α))) s),
    #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have neg : ∀ (hℬ : s ∉ upperClosure (↑ℬ : Set (Finset α))),
  #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
Tactic: by_cases hℬ : s ∈ upperClosure (ℬ : Set <| Finset α)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ upperClosure (↑𝒜 : Set (Finset α))
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have pos : ∀ (hℬ : Membership.mem (γ := UpperSet (Finset α)) (upperClosure (↑ℬ : Set (Finset α))) s),
  #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
Tactic: by_cases hℬ : s ∈ upperClosure (ℬ : Set <| Finset α)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ upperClosure (↑𝒜 : Set (Finset α))
pos :
  ∀ (hℬ : Membership.mem (γ := UpperSet (Finset α)) (upperClosure (↑ℬ : Set (Finset α))) s),
    #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have neg : ∀ (hℬ : s ∉ upperClosure (↑ℬ : Set (Finset α))),
  #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
Tactic: by_cases hℬ : s ∈ upperClosure (ℬ : Set <| Finset α)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : Membership.mem (γ := UpperSet (Finset α)) (upperClosure (↑𝒜 : Set (Finset α))) s
hℬ : Membership.mem (γ := UpperSet (Finset α)) (upperClosure (↑ℬ : Set (Finset α))) s
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have pos : #(𝒜.truncatedInf s ⊓ ℬ.truncatedInf s) + #(𝒜.truncatedInf s ⊔ ℬ.truncatedInf s) =
  #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
Tactic: rw [truncatedInf_union h𝒜 hℬ, truncatedInf_sups h𝒜 hℬ]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : Membership.mem (γ := UpperSet (Finset α)) (upperClosure (↑𝒜 : Set (Finset α))) s
hℬ : s ∉ upperClosure (↑ℬ : Set (Finset α))
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have neg : #(𝒜.truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
Tactic: rw [truncatedInf_union_left h𝒜 hℬ, truncatedInf_of_notMem hℬ,
      truncatedInf_sups_of_notMem fun h ↦ hℬ h.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : Membership.mem (γ := UpperSet (Finset α)) (upperClosure (↑𝒜 : Set (Finset α))) s
hℬ : s ∉ upperClosure (↑ℬ : Set (Finset α))
neg : #(𝒜.truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have neg₁ : #(𝒜.truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + card.{u_1} (α := α) ⊥
Tactic: rw [truncatedInf_union_left h𝒜 hℬ, truncatedInf_of_notMem hℬ,
      truncatedInf_sups_of_notMem fun h ↦ hℬ h.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : Membership.mem (γ := UpperSet (Finset α)) (upperClosure (↑𝒜 : Set (Finset α))) s
hℬ : s ∉ upperClosure (↑ℬ : Set (Finset α))
neg : #(𝒜.truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
neg₁ : #(𝒜.truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + card.{u_1} (α := α) ⊥
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have neg₂ : #(𝒜.truncatedInf s) + card.{u_1} (α := α) ⊥ = #(𝒜.truncatedInf s) + card.{u_1} (α := α) ⊥
Tactic: rw [truncatedInf_union_left h𝒜 hℬ, truncatedInf_of_notMem hℬ,
      truncatedInf_sups_of_notMem fun h ↦ hℬ h.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ upperClosure (↑𝒜 : Set (Finset α))
hℬ : Membership.mem (γ := UpperSet (Finset α)) (upperClosure (↑ℬ : Set (Finset α))) s
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have pos : #(ℬ.truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
Tactic: rw [truncatedInf_union_right h𝒜 hℬ, truncatedInf_of_notMem h𝒜,
      truncatedInf_sups_of_notMem fun h ↦ h𝒜 h.1, add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ upperClosure (↑𝒜 : Set (Finset α))
hℬ : Membership.mem (γ := UpperSet (Finset α)) (upperClosure (↑ℬ : Set (Finset α))) s
pos : #(ℬ.truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have pos₁ : #(ℬ.truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = card.{u_1} (α := α) ⊥ + #(ℬ.truncatedInf s)
Tactic: rw [truncatedInf_union_right h𝒜 hℬ, truncatedInf_of_notMem h𝒜,
      truncatedInf_sups_of_notMem fun h ↦ h𝒜 h.1, add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ upperClosure (↑𝒜 : Set (Finset α))
hℬ : Membership.mem (γ := UpperSet (Finset α)) (upperClosure (↑ℬ : Set (Finset α))) s
pos : #(ℬ.truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
pos₁ : #(ℬ.truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = card.{u_1} (α := α) ⊥ + #(ℬ.truncatedInf s)
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have pos₂ : #(ℬ.truncatedInf s) + card.{u_1} (α := α) ⊥ = card.{u_1} (α := α) ⊥ + #(ℬ.truncatedInf s)
Tactic: rw [truncatedInf_union_right h𝒜 hℬ, truncatedInf_of_notMem h𝒜,
      truncatedInf_sups_of_notMem fun h ↦ h𝒜 h.1, add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ upperClosure (↑𝒜 : Set (Finset α))
hℬ : Membership.mem (γ := UpperSet (Finset α)) (upperClosure (↑ℬ : Set (Finset α))) s
pos : #(ℬ.truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
pos₁ : #(ℬ.truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = card.{u_1} (α := α) ⊥ + #(ℬ.truncatedInf s)
pos₂ : #(ℬ.truncatedInf s) + card.{u_1} (α := α) ⊥ = card.{u_1} (α := α) ⊥ + #(ℬ.truncatedInf s)
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have pos₃ : card.{u_1} (α := α) ⊥ + #(ℬ.truncatedInf s) = card.{u_1} (α := α) ⊥ + #(ℬ.truncatedInf s)
Tactic: rw [truncatedInf_union_right h𝒜 hℬ, truncatedInf_of_notMem h𝒜,
      truncatedInf_sups_of_notMem fun h ↦ h𝒜 h.1, add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ upperClosure (↑𝒜 : Set (Finset α))
hℬ : s ∉ upperClosure (↑ℬ : Set (Finset α))
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have neg : #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = card.{u_1} (α := α) ⊥ + #(ℬ.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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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)
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have neg₁ : #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = card.{u_1} (α := α) ⊥ + card.{u_1} (α := α) ⊥
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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} (α := α) ⊥
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have neg₂ : card.{u_1} (α := α) ⊥ + #((𝒜 ⊻ ℬ).truncatedInf s) = card.{u_1} (α := α) ⊥ + card.{u_1} (α := α) ⊥
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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} (α := α) ⊥
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
have neg₃ : card.{u_1} (α := α) ⊥ + card.{u_1} (α := α) ⊥ = card.{u_1} (α := α) ⊥ + card.{u_1} (α := α) ⊥
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]
-- 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 α,
        (↑(#((𝒜 ∪ ℬ).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) : ℚ)))
have 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) : ℚ))
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 →
      (↑(#((𝒜 ∪ ℬ).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) : ℚ))
have simp_rw : ∀ (s : Finset α), Membership.mem (γ := Finset (Finset α)) univ s → True
Tactic: simp_rw [← add_div, ← Nat.cast_add, card_truncatedSup_union_add_card_truncatedSup_infs]