mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case pos
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
b a : α
h✝ : b ≤ a
⊢ ({b ∈ {b} | b ≤ a}.inf' ⋯ fun x ↦ x) = b

pp: case neg
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
b a : α
h✝ : ¬b ≤ a
⊢ ⊥ = ⊥

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
b a : α
h✝ : b ≤ a
⊢ ({b ∈ {b} | b ≤ a}.inf' ⋯ fun x ↦ x) = b

case neg
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
b a : α
h✝ : ¬b ≤ a
⊢ ⊥ = ⊥
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ ∀ ⦃x : α⦄, x ∈ s ○ t → x ∈ s ⊻ t

Tactic:
mem_sups,

Goal state after:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ ∀ ⦃x : α⦄, x ∈ s ○ t → ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = x
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeInf α
inst✝⁴ : SemilatticeInf β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE β
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
e : α ≃o β
s : Finset α
a : α
this : e a ∈ upperClosure ↑(map e.toEmbedding s) ↔ a ∈ upperClosure ↑s
⊢ e (s.truncatedInf a) = (map e.toEmbedding s).truncatedInf (e a)

Tactic:
truncatedInf,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeInf α
inst✝⁴ : SemilatticeInf β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE β
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
e : α ≃o β
s : Finset α
a : α
this : e a ∈ upperClosure ↑(map e.toEmbedding s) ↔ a ∈ upperClosure ↑s
⊢ e (if h : a ∈ upperClosure ↑s then {b ∈ s | b ≤ a}.inf' ⋯ id else ⊥) =
    if h : e a ∈ upperClosure ↑(map e.toEmbedding s) then {b ∈ map e.toEmbedding s | b ≤ e a}.inf' ⋯ id else ⊥
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: case pos
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
a b : α
h : Disjoint a b
⊢ {a} ○ {b} = {a ⊔ b}

pp: case neg
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
a b : α
h : ¬Disjoint a b
⊢ {a} ○ {b} = ∅

Tactic:
<;>

Goal state after:
case pos
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
a b : α
h : Disjoint a b
⊢ {a} ○ {b} = {a ⊔ b}

case neg
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
a b : α
h : ¬Disjoint a b
⊢ {a} ○ {b} = ∅
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case zero
α : Type u_1
inst✝ : DecidableEq α
⊢ ∂^[0] ∅ = ∅

pp: case succ
α : Type u_1
inst✝ : DecidableEq α
n✝ : ℕ
a✝ : ∂^[n✝] ∅ = ∅
⊢ ∂^[n✝ + 1] ∅ = ∅

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝ : DecidableEq α
⊢ ∂^[0] ∅ = ∅

case succ
α : Type u_1
inst✝ : DecidableEq α
n✝ : ℕ
a✝ : ∂^[n✝] ∅ = ∅
⊢ ∂^[n✝ + 1] ∅ = ∅
Module: Mathlib.Order.Irreducible

Goal state before:
pp: case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupPrime a
i : ι
s : Finset ι
a✝ : i ∉ s
ih : a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i
⊢ a ≤ (insert i s).sup f ↔ ∃ i_1 ∈ insert i s, a ≤ f i_1

Tactic:
simp only [exists_mem_insert, sup_insert, ha.le_sup, ih]

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ lowerClosure ↑𝒜
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure ↑𝒜
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ lowerClosure ↑𝒜
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ lowerClosure ↑𝒜
⊢ #((𝒜 ∪ ℬ).truncatedSup s) + #((𝒜 ⊼ ℬ).truncatedSup s) = #(𝒜.truncatedSup s) + #(ℬ.truncatedSup s)
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ upperClosure ↑𝒜
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ upperClosure ↑𝒜
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ upperClosure ↑𝒜
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ upperClosure ↑𝒜
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case isTrue
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
h✝ : IsEmpty α
⊢ ofIsEmpty (a ⊔ b) = ofIsEmpty a ∪ ofIsEmpty b

pp: case isFalse
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
h✝ : ¬IsEmpty α
⊢ (have this := Fintype.toOrderBot α;
      RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
        { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊔ b) =
    (have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∪
      (have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
h✝ : IsEmpty α
⊢ ofIsEmpty (a ⊔ b) = ofIsEmpty a ∪ ofIsEmpty b

case isFalse
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
h✝ : ¬IsEmpty α
⊢ (have this := Fintype.toOrderBot α;
      RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
        { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊔ b) =
    (have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∪
      (have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case isTrue
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
h✝ : IsEmpty α
⊢ ofIsEmpty (a ⊓ b) = ofIsEmpty a ∩ ofIsEmpty b

pp: case isFalse
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
h✝ : ¬IsEmpty α
⊢ (have this := Fintype.toOrderBot α;
      RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
        { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊓ b) =
    (have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∩
      (have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
h✝ : IsEmpty α
⊢ ofIsEmpty (a ⊓ b) = ofIsEmpty a ∩ ofIsEmpty b

case isFalse
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
h✝ : ¬IsEmpty α
⊢ (have this := Fintype.toOrderBot α;
      RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
        { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊓ b) =
    (have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∩
      (have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
t : Finset α
h✝ : t ⊆ s
⊢ (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t))

pp: case neg
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
t : Finset α
h✝ : ¬t ⊆ s
⊢ (↑(card α) - ↑(#⊤)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) = 0

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
t : Finset α
h✝ : t ⊆ s
⊢ (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
    (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t))

case neg
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
t : Finset α
h✝ : ¬t ⊆ s
⊢ (↑(card α) - ↑(#⊤)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) = 0
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ 1 = ∑ j ∈ range (#s + 1), ∑ t ∈ powersetCard j s, (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t))

Tactic:
← binomial_sum_eq ((card_lt_iff_ne_univ _).2 hs),

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ ∑ i ∈ range (#s + 1), ↑((#s).choose i) * (↑(card α) - ↑(#s)) / ((↑(card α) - ↑i) * ↑((card α).choose i)) =
    ∑ j ∈ range (#s + 1), ∑ t ∈ powersetCard j s, (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t))
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsLowerSet ↑ℬ
this : (Fintype.card (Finset α) - #𝒜) * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ)
⊢ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ

Tactic:
Fintype.card_finset,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsLowerSet ↑ℬ
this : (2 ^ Fintype.card α - #𝒜) * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ)
⊢ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ (Fintype.card (Finset α) - #𝒜) * #ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ)

Tactic:
Fintype.card_finset,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ (2 ^ Fintype.card α - #𝒜) * #ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ)
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝² : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝¹ : v \ u = v
this✝ : x ∉ u
hus : u ⊆ s
w : α
hwB : ¬¬(w ∈ s ∪ v → w ∈ u)
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∉ u
⊢ False

Tactic:
Classical.not_not

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝² : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝¹ : v \ u = v
this✝ : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∈ s ∪ v → w ∈ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∉ u
⊢ False
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
⊢ Fintype.card (Finset α) - #{⊥} = 2 ^ Fintype.card α - 1

Tactic:
Fintype.card_finset,

Goal state after:
case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
⊢ 2 ^ Fintype.card α - #{⊥} = 2 ^ Fintype.card α - 1
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case inl
β : Type u_2
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ 0
h₀₁ : a₀ * b₁ ≤ 0
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
⊢ 0 ≤ c₀ * d₁ + c₁ * d₀

pp: case inl
β : Type u_2
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ 0
h₀₁ : a₀ * b₁ ≤ 0
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
⊢ 0 ≤ a₁ * b₀

pp: case inl
β : Type u_2
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ 0
h₀₁ : a₀ * b₁ ≤ 0
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
⊢ 0 ≤ a₀ * b₁

Tactic:
<;>

Goal state after:
case inl
β : Type u_2
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ 0
h₀₁ : a₀ * b₁ ≤ 0
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
⊢ 0 ≤ c₀ * d₁ + c₁ * d₀

case inl
β : Type u_2
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ 0
h₀₁ : a₀ * b₁ ≤ 0
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
⊢ 0 ≤ a₁ * b₀

case inl
β : Type u_2
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ 0
h₀₁ : a₀ * b₁ ≤ 0
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
⊢ 0 ≤ a₀ * b₁
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ t ∈ {s, insert a s}

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ t ∈ {s}

pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ t ∈ {insert a s}

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ t ∈ ∅

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ t ∈ {s, insert a s}

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ t ∈ {s}

case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ t ∈ {insert a s}

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔ t ∈ ∅
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ t = s ∨ t = insert a s → t ∈ 𝒜

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ t ∈ 𝒜 ∧ (t = s ∨ t = insert a s) ↔ t = s

pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ t ∈ 𝒜 ∧ (t = s ∨ t = insert a s) ↔ t = insert a s

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ t ∈ 𝒜 → ¬t = s ∧ ¬t = insert a s

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ t = s ∨ t = insert a s → t ∈ 𝒜

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ t ∈ 𝒜 ∧ (t = s ∨ t = insert a s) ↔ t = s

case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ t ∈ 𝒜 ∧ (t = s ∨ t = insert a s) ↔ t = insert a s

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ t ∈ 𝒜 → ¬t = s ∧ ¬t = insert a s
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
⊢ collapse 𝒜 a f s = (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0

Tactic:
collapse,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
⊢ ∑ t ∈ 𝒜 with t.erase a = s, f t = (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ ∑ x ∈ {s, insert a s}, f x = f s + f (insert a s)

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ ∑ x ∈ {s}, f x = f s + 0

pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ ∑ x ∈ {insert a s}, f x = 0 + f (insert a s)

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ ∑ x ∈ ∅, f x = 0 + 0

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ ∑ x ∈ {s, insert a s}, f x = f s + f (insert a s)

case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ ∑ x ∈ {s}, f x = f s + 0

case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ ∑ x ∈ {insert a s}, f x = 0 + f (insert a s)

case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ ∑ x ∈ ∅, f x = 0 + 0
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝³ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝² : v \ u = v
this✝¹ : x ∉ u
hus : u ⊆ s
w : α
hwB : w ∈ s ∪ v → w ∈ u
hw𝒜' : insert w ((s ∪ v) \ u) ∈ 𝒜'
this✝ : v ⊆ insert w ((s ∪ v) \ u)
hwu : w ∉ u
this : (insert w ((s ∪ v) \ u) ∪ u) \ v ∈ 𝒜
⊢ insert w s = (insert w ((s ∪ v) \ u) ∪ u) \ v

Tactic:
rw [insert_union, sdiff_union_of_subset (hus.trans subset_union_left),
    insert_sdiff_of_notMem _ (hwu ∘ hwB ∘ mem_union_right _), union_sdiff_cancel_right hsv]

Goal state after: