awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
s t : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
inst_3 : DecidableEq α
hs : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a
ht : ∀ x ∈ t, ¬x ≤ a
⊢ (s ∪ t).truncatedInf a = s.truncatedInf a

Tactic:
simp only [truncatedInf_of_mem, hs, filter_union, filter_false_of_mem ht, union_empty,
    upper_aux.2 (Or.inl hs)]

Premises used: Iff.mpr, Finset.filter_false_of_mem, _private.0.Finset.upper_aux, Finset.union_empty, Or.inl, Finset.filter_union, Finset.truncatedInf_of_mem
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
s t : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
inst_3 : DecidableEq α
hs : a ∉ upperClosure (↑s : Set α)
ht : Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
rw : (t ∪ s).truncatedInf a = t.truncatedInf a
rw₁ rw₂ : t.truncatedInf a = t.truncatedInf a
⊢ (s ∪ t).truncatedInf a = t.truncatedInf a

Tactic:
rw [union_comm, truncatedInf_union_left ht hs]

Premises used: Finset.union_comm, Finset.truncatedInf_union_left
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
s t : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
inst_3 : DecidableEq α
hs : a ∉ upperClosure (↑s : Set α)
ht : a ∉ upperClosure (↑t : Set α)
rw : a ∉ upperClosure (↑s : Set α) ⊓ upperClosure (↑t : Set α)
⊢ a ∉ upperClosure (↑(s ∪ t) : Set α)

Tactic:
rw [coe_union, upperClosure_union]

Premises used: upperClosure_union, Finset.coe_union
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
s t : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
inst_3 : DecidableEq α
hs : a ∉ upperClosure (↑s : Set α)
ht : a ∉ upperClosure (↑t : Set α)
⊢ a ∉ upperClosure (↑s : Set α) ⊓ upperClosure (↑t : Set α)

Tactic:
fun h ↦ h.elim hs ht

Premises used: Or.elim, Not
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : SemilatticeInf α
s t : Finset α
a : α
inst_1 : DecidableLE α
inst_2 : BoundedOrder α
inst_3 : DecidableEq α
hs : a ∉ upperClosure (↑s : Set α)
ht : a ∉ upperClosure (↑t : Set α)
⊢ a ∉ upperClosure (↑s : Set α) ⊓ upperClosure (↑t : Set α)

Tactic:
exact fun h ↦ h.elim hs ht
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
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_infs, lowerClosure_infs, LowerSet.mem_inf_iff]

Premises used: LowerSet.mem_inf_iff, Finset.coe_infs, lowerClosure_infs
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
rw :
  Membership.mem (γ := UpperSet α) (upperClosure ((↑s : Set α) ⊻ (↑t : Set α))) a ↔
    Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∧
      Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
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
rw₂ rw₃ :
  Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a ∧
      Membership.mem (γ := UpperSet α) (upperClosure (↑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

Tactic:
rw [coe_sups, upperClosure_sups, UpperSet.mem_sup_iff]

Premises used: upperClosure_sups, UpperSet.mem_sup_iff, Finset.coe_sups
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
inst_2 : DecidableLE α
inst_3 : BoundedOrder α
hs : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
ht : Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
simp :
  Eq (α := α) (({b ∈ s | a ≤ b} ⊼ {b ∈ t | a ≤ b}).sup' ⋯ fun (x : α) ↦ id x)
    (({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' ⋯ fun (i : α × α) ↦ id i.1 ⊓ id i.2)
⊢ (s ⊼ t).truncatedSup a = s.truncatedSup a ⊓ t.truncatedSup a

Tactic:
simp only [truncatedSup_of_mem, hs, ht, infs_aux.2 ⟨hs, ht⟩, sup'_inf_sup', filter_infs_le]

Premises used: Iff.mpr, Finset.truncatedSup_of_mem, Finset.filter_infs_le, Finset.sup'_inf_sup', And.intro, _private.0.Finset.infs_aux
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
inst_2 : DecidableLE α
inst_3 : BoundedOrder α
hs : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
ht : Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
rw :
  Eq (α := α)
    (({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' ⋯ ((fun (x : α) ↦ id x) ∘ Function.uncurry fun (x1 x2 : α) ↦ x1 ⊓ x2))
    (({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' ⋯ fun (i : α × α) ↦ id i.1 ⊓ id i.2)
⊢ Eq (α := α)
    (sup' (image (Function.uncurry fun (x1 x2 : α) ↦ x1 ⊓ x2) ({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b})) ⋯ fun (x : α) ↦
      id x)
    (({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' ⋯ fun (i : α × α) ↦ id i.1 ⊓ id i.2)

Tactic:
rw [sup'_image]

Premises used: Finset.sup'_image
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
inst_2 : DecidableLE α
inst_3 : BoundedOrder α
hs : Membership.mem (γ := LowerSet α) (lowerClosure (↑s : Set α)) a
ht : Membership.mem (γ := LowerSet α) (lowerClosure (↑t : Set α)) a
⊢ Eq (α := α)
    (({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' ⋯ ((fun (x : α) ↦ id x) ∘ Function.uncurry fun (x1 x2 : α) ↦ x1 ⊓ x2))
    (({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' ⋯ fun (i : α × α) ↦ id i.1 ⊓ id i.2)

Tactic:
simp [Function.uncurry_def]

Premises used: Function.uncurry_def
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
inst_2 : DecidableLE α
inst_3 : BoundedOrder α
hs : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a
ht : Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
simp :
  Eq (α := α) (({b ∈ s | b ≤ a} ⊻ {b ∈ t | b ≤ a}).inf' ⋯ fun (x : α) ↦ id x)
    (({b ∈ s | b ≤ a} ×ˢ {b ∈ t | b ≤ a}).inf' ⋯ fun (i : α × α) ↦ id i.1 ⊔ id i.2)
⊢ (s ⊻ t).truncatedInf a = s.truncatedInf a ⊔ t.truncatedInf a

Tactic:
simp only [truncatedInf_of_mem, hs, ht, sups_aux.2 ⟨hs, ht⟩, inf'_sup_inf', filter_sups_le]

Premises used: Iff.mpr, Finset.inf'_sup_inf', Finset.filter_sups_le, And.intro, _private.0.Finset.sups_aux, Finset.truncatedInf_of_mem
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
inst_2 : DecidableLE α
inst_3 : BoundedOrder α
hs : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a
ht : Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
rw :
  Eq (α := α)
    (({b ∈ s | b ≤ a} ×ˢ {b ∈ t | b ≤ a}).inf' ⋯ ((fun (x : α) ↦ id x) ∘ Function.uncurry fun (x1 x2 : α) ↦ x1 ⊔ x2))
    (({b ∈ s | b ≤ a} ×ˢ {b ∈ t | b ≤ a}).inf' ⋯ fun (i : α × α) ↦ id i.1 ⊔ id i.2)
⊢ Eq (α := α)
    (inf' (image (Function.uncurry fun (x1 x2 : α) ↦ x1 ⊔ x2) ({b ∈ s | b ≤ a} ×ˢ {b ∈ t | b ≤ a})) ⋯ fun (x : α) ↦
      id x)
    (({b ∈ s | b ≤ a} ×ˢ {b ∈ t | b ≤ a}).inf' ⋯ fun (i : α × α) ↦ id i.1 ⊔ id i.2)

Tactic:
rw [inf'_image]

Premises used: Finset.inf'_image
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
inst_2 : DecidableLE α
inst_3 : BoundedOrder α
hs : Membership.mem (γ := UpperSet α) (upperClosure (↑s : Set α)) a
ht : Membership.mem (γ := UpperSet α) (upperClosure (↑t : Set α)) a
⊢ Eq (α := α)
    (({b ∈ s | b ≤ a} ×ˢ {b ∈ t | b ≤ a}).inf' ⋯ ((fun (x : α) ↦ id x) ∘ Function.uncurry fun (x1 x2 : α) ↦ x1 ⊔ x2))
    (({b ∈ s | b ≤ a} ×ˢ {b ∈ t | b ≤ a}).inf' ⋯ fun (i : α × α) ↦ id i.1 ⊔ id i.2)

Tactic:
simp [Function.uncurry_def]

Premises used: Function.uncurry_def
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
inst_2 : DecidableLE α
inst_3 : BoundedOrder α
ha : a ∉ lowerClosure (↑s : Set α) ⊓ lowerClosure (↑t : Set α)
rwa : a ∉ lowerClosure ((↑s : Set α) ⊼ (↑t : Set α))
rwa₁ rwa₂ rwa₃ rwa₄ : a ∉ lowerClosure (↑s : Set α) ⊓ lowerClosure (↑t : Set α)
⊢ a ∉ lowerClosure (↑(s ⊼ t) : Set α)

Tactic:
rwa [coe_infs, lowerClosure_infs]

Premises used: Finset.coe_infs, lowerClosure_infs
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : DecidableEq α
s t : Finset α
a : α
inst_2 : DecidableLE α
inst_3 : BoundedOrder α
ha : a ∉ upperClosure (↑s : Set α) ⊔ upperClosure (↑t : Set α)
rwa : a ∉ upperClosure ((↑s : Set α) ⊻ (↑t : Set α))
rwa₁ rwa₂ rwa₃ rwa₄ : a ∉ upperClosure (↑s : Set α) ⊔ upperClosure (↑t : Set α)
⊢ a ∉ upperClosure (↑(s ⊻ t) : Set α)

Tactic:
rwa [coe_sups, upperClosure_sups]

Premises used: upperClosure_sups, Finset.coe_sups
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : DecidableLE α
s : Finset α
a : α
⊢ (s.truncatedSup a)ᶜ = sᶜˢ.truncatedInf aᶜ

Tactic:
map_truncatedSup (OrderIso.compl α) _ _

Premises used: Finset.inf', Finset.truncatedInf, Set.Mem, setOf, Finset.compls, WithTop.some, WithTop.untop, Finset.map_truncatedSup, OrderIso.compl, OrderDual, Finset.inf, WithTop
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : DecidableLE α
s : Finset α
a : α
⊢ (s.truncatedInf a)ᶜ = sᶜˢ.truncatedSup aᶜ

Tactic:
map_truncatedInf (OrderIso.compl α) _ _

Premises used: WithBot.some, WithBot, Finset.map_truncatedInf, Set.Mem, setOf, Finset.compls, WithBot.unbot, Finset.truncatedSup, OrderIso.compl, Finset.sup, OrderDual, Finset.sup'
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
pos :
  ∀ (h𝒜 : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑𝒜 : Set (Finset α))) s),
    #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
neg :
  ∀ (h𝒜 : s ∉ lowerClosure (↑𝒜 : Set (Finset α))),
    #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

Tactic:
by_cases h𝒜 : s ∈ lowerClosure (𝒜 : Set <| Finset α)

Premises used: SetLike.coe, lowerClosure
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑𝒜 : Set (Finset α))) s
pos :
  ∀ (hℬ : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑ℬ : Set (Finset α))) s),
    #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
neg :
  ∀ (hℬ : s ∉ lowerClosure (↑ℬ : Set (Finset α))),
    #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

Tactic:
by_cases hℬ : s ∈ lowerClosure (ℬ : Set <| Finset α)

Premises used: SetLike.coe, lowerClosure
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure (↑𝒜 : Set (Finset α))
pos :
  ∀ (hℬ : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑ℬ : Set (Finset α))) s),
    #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
neg :
  ∀ (hℬ : s ∉ lowerClosure (↑ℬ : Set (Finset α))),
    #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

Tactic:
by_cases hℬ : s ∈ lowerClosure (ℬ : Set <| Finset α)

Premises used: SetLike.coe, lowerClosure
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑𝒜 : Set (Finset α))) s
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) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

Tactic:
rw [truncatedSup_union h𝒜 hℬ, truncatedSup_infs h𝒜 hℬ]

Premises used: Finset.truncatedSup_infs, Finset.truncatedSup_union
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑𝒜 : Set (Finset α))) s
hℬ : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑ℬ : Set (Finset α))) s
⊢ #(𝒜.truncatedSup s ⊔ ℬ.truncatedSup s) + #(𝒜.truncatedSup s ⊓ ℬ.truncatedSup s) =
    #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

Tactic:
card_union_add_card_inter _ _

Premises used: Finset.card_union_add_card_inter
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑𝒜 : Set (Finset α))) s
hℬ : Membership.mem (γ := LowerSet (Finset α)) (lowerClosure (↑ℬ : Set (Finset α))) s
⊢ #(𝒜.truncatedSup s ⊔ ℬ.truncatedSup s) + #(𝒜.truncatedSup s ⊓ ℬ.truncatedSup s) =
    #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

Tactic:
exact card_union_add_card_inter _ _

Premises used: Finset.card_union_add_card_inter
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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} (α := α) ⊤
neg₂ neg₃ : #(𝒜.truncatedSup s) + card.{u_1} (α := α) ⊤ = #(𝒜.truncatedSup s) + card.{u_1} (α := α) ⊤
⊢ #((𝒜 ∪ ℬ).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]

Premises used: Finset.truncatedSup_union_left, And.right, Finset.truncatedSup_infs_of_notMem, Finset.truncatedSup_of_notMem
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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)
pos₃ pos₄ : card.{u_1} (α := α) ⊤ + #(ℬ.truncatedSup s) = card.{u_1} (α := α) ⊤ + #(ℬ.truncatedSup s)
⊢ #((𝒜 ∪ ℬ).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]

Premises used: add_comm, Finset.truncatedSup_union_right, And.left, Finset.truncatedSup_infs_of_notMem, Finset.truncatedSup_of_notMem
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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} (α := α) ⊤
neg₃ neg₄ : card.{u_1} (α := α) ⊤ + card.{u_1} (α := α) ⊤ = card.{u_1} (α := α) ⊤ + card.{u_1} (α := α) ⊤
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.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]

Premises used: Finset.truncatedSup_union_of_notMem, And.left, Finset.truncatedSup_infs_of_notMem, Finset.truncatedSup_of_notMem
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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)
neg :
  ∀ (h𝒜 : s ∉ upperClosure (↑𝒜 : Set (Finset α))),
    #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)

Tactic:
by_cases h𝒜 : s ∈ upperClosure (𝒜 : Set <| Finset α)

Premises used: upperClosure, SetLike.coe
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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)
neg :
  ∀ (hℬ : s ∉ upperClosure (↑ℬ : Set (Finset α))),
    #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)

Tactic:
by_cases hℬ : s ∈ upperClosure (ℬ : Set <| Finset α)

Premises used: upperClosure, SetLike.coe
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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)
neg :
  ∀ (hℬ : s ∉ upperClosure (↑ℬ : Set (Finset α))),
    #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)

Tactic:
by_cases hℬ : s ∈ upperClosure (ℬ : Set <| Finset α)

Premises used: upperClosure, SetLike.coe
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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
pos :
  #(𝒜.truncatedInf s ⊓ ℬ.truncatedInf s) + #(𝒜.truncatedInf s ⊔ ℬ.truncatedInf s) =
    #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)

Tactic:
rw [truncatedInf_union h𝒜 hℬ, truncatedInf_sups h𝒜 hℬ]

Premises used: Finset.truncatedInf_union, Finset.truncatedInf_sups
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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) =
    #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)

Tactic:
card_inter_add_card_union _ _

Premises used: Finset.card_inter_add_card_union
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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) =
    #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)

Tactic:
exact card_inter_add_card_union _ _

Premises used: Finset.card_inter_add_card_union
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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} (α := α) ⊥
neg₂ neg₃ : #(𝒜.truncatedInf s) + card.{u_1} (α := α) ⊥ = #(𝒜.truncatedInf s) + card.{u_1} (α := α) ⊥
⊢ #((𝒜 ∪ ℬ).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]

Premises used: Finset.truncatedInf_union_left, Finset.truncatedInf_sups_of_notMem, And.right, Finset.truncatedInf_of_notMem
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
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)
pos₃ pos₄ : card.{u_1} (α := α) ⊥ + #(ℬ.truncatedInf s) = card.{u_1} (α := α) ⊥ + #(ℬ.truncatedInf s)
⊢ #((𝒜 ∪ ℬ).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]

Premises used: add_comm, Finset.truncatedInf_sups_of_notMem, And.left, Finset.truncatedInf_union_right, Finset.truncatedInf_of_notMem