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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
s : Set α
⊢ s = ∅ → s ≠ {⊥}

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
inst✝ : Subsingleton α
s : Set α
⊢ s = ∅ → s ≠ {⊥}
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ insert b s

pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ (insert b s).Intersecting

Tactic:
·

Goal state after:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ insert b s
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ b ∈ ↑(insert b s)

pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ (↑(insert b s)).Intersecting

Tactic:
·

Goal state after:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ b ∈ ↑(insert b s)
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

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

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

Tactic:
·

Goal state after:
case h₁
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ
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₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
⊢ a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀

pp: case inr
β : 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₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : 0 < c₀ * d₁
⊢ a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀

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₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
⊢ a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

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

Tactic:
·

Goal state after:
case h₂
α : 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.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
⊢ #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)

pp: case inr
ι : 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 : #s ≤ Fintype.card α
⊢ #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)

Tactic:
·

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
⊢ #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
h✝ : insert a t ∈ 𝒜
⊢ f t ≤ f t + f (insert a t)

pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
h✝ : insert a t ∉ 𝒜
⊢ f t ≤ f t + 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
h✝ : insert a t ∈ 𝒜
⊢ f t ≤ f t + f (insert a t)
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
h✝ : insert a t ∉ 𝒜
⊢ f t ≤ f t + 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
hf : 0 ≤ f
ht : t ∈ 𝒜
ha : a ∉ t
h✝ : insert a t ∉ 𝒜
⊢ f t ≤ f t + 0
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h✝ : s ∈ 𝒜
⊢ f t ≤ f s + f t

pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h✝ : s ∉ 𝒜
⊢ f t ≤ 0 + f t

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h✝ : s ∈ 𝒜
⊢ f t ≤ f s + f t
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h✝ : s ∉ 𝒜
⊢ f t ≤ 0 + f t

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h✝ : s ∉ 𝒜
⊢ f t ≤ 0 + f t
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: case pos
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : #s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
⊢ ∃ t, s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting

pp: case neg
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : #s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s).Intersecting
h : ∃ t, (↑t).Intersecting ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t, s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : #s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
⊢ ∃ t, s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (∃ a ∉ t, #s = #(insert a t) ∧ toColex (insert a t) ≤ toColex s) →
    #(s.erase (s.min' hs)) = #t ∧ toColex t ≤ toColex (s.erase (s.min' hs))

pp: case mpr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ #(s.erase (s.min' hs)) = #t ∧ toColex t ≤ toColex (s.erase (s.min' hs)) →
    ∃ a ∉ t, #s = #(insert a t) ∧ toColex (insert a t) ≤ toColex s

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (∃ a ∉ t, #s = #(insert a t) ∧ toColex (insert a t) ≤ toColex s) →
    #(s.erase (s.min' hs)) = #t ∧ toColex t ≤ toColex (s.erase (s.min' hs))
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: case inr.cons.refine_1
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ IsUpperSet ↑(s.biUnion f')

pp: case inr.cons.refine_2
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ IsLowerSet ↑(f' i)ᶜ

pp: case inr.cons.refine_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * Fintype.card (Finset α) + 2 * (#(s.biUnion f') * #(f' i)ᶜ) ≤
    2 * 2 ^ Fintype.card α * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi)))

Tactic:
·

Goal state after:
case inr.cons.refine_1
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ IsUpperSet ↑(s.biUnion f')
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mp.left
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts : toColex (insert a t) ≤ toColex s
⊢ #(s.erase (s.min' hs)) = #t

pp: case mp.right
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts : toColex (insert a t) ≤ toColex s
⊢ toColex t ≤ toColex (s.erase (s.min' hs))

Tactic:
·

Goal state after:
case mp.left
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts : toColex (insert a t) ≤ toColex s
⊢ #(s.erase (s.min' hs)) = #t
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mp.right
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts : toColex (insert a t) ≤ toColex s
⊢ toColex t ≤ toColex (s.erase (s.min' hs))

Tactic:
·

Goal state after:
case mp.right
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts : toColex (insert a t) ≤ toColex s
⊢ toColex t ≤ toColex (s.erase (s.min' hs))
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: case inr.cons.refine_2
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ IsLowerSet ↑(f' i)ᶜ

pp: case inr.cons.refine_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * Fintype.card (Finset α) + 2 * (#(s.biUnion f') * #(f' i)ᶜ) ≤
    2 * 2 ^ Fintype.card α * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi)))

Tactic:
·

Goal state after:
case inr.cons.refine_2
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ IsLowerSet ↑(f' i)ᶜ
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ r ≤ #(bipartiteBelow (fun x1 x2 ↦ x1 ⊆ x2) (∂ 𝒜) s)

pp: case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun x1 x2 ↦ x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - r + 1

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ r ≤ #(bipartiteBelow (fun x1 x2 ↦ x1 ⊆ x2) (∂ 𝒜) s)
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ∅ ∉ 𝒜

Tactic:
← mem_coe,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ∅ ∉ ↑𝒜
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
cards' : #(s.erase (s.min' hs)) = #(s.erase (s.min' hs))
⊢ ∃ a ∉ s.erase (s.min' hs),
    #s = #(insert a (s.erase (s.min' hs))) ∧
      (insert a (s.erase (s.min' hs)) = s ∨
        ∃ w ∈ s,
          w ∉ insert a (s.erase (s.min' hs)) ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a (s.erase (s.min' hs)) ↔ a_1 ∈ s))

pp: case mpr.inr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
⊢ ∃ a ∉ t,
    #s = #(insert a t) ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))

Tactic:
·

Goal state after:
case mpr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
cards' : #(s.erase (s.min' hs)) = #(s.erase (s.min' hs))
⊢ ∃ a ∉ s.erase (s.min' hs),
    #s = #(insert a (s.erase (s.min' hs))) ∧
      (insert a (s.erase (s.min' hs)) = s ∨
        ∃ w ∈ s,
          w ∉ insert a (s.erase (s.min' hs)) ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a (s.erase (s.min' hs)) ↔ a_1 ∈ s))
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r ↑𝒜
hr' : Fintype.card α < r
⊢ ↑(#𝒜) / ↑((Fintype.card α).choose r) ≤ ↑(#(∂ 𝒜)) / ↑((Fintype.card α).choose (r - 1))

pp: case inr
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r ↑𝒜
hr' : r ≤ Fintype.card α
⊢ ↑(#𝒜) / ↑((Fintype.card α).choose r) ≤ ↑(#(∂ 𝒜)) / ↑((Fintype.card α).choose (r - 1))

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r ↑𝒜
hr' : Fintype.card α < r
⊢ ↑(#𝒜) / ↑((Fintype.card α).choose r) ≤ ↑(#(∂ 𝒜)) / ↑((Fintype.card α).choose (r - 1))
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk✝ : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
hjk : j < k
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)

pp: case mpr.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)

Tactic:
·

Goal state after:
case mpr.inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk✝ : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
hjk : j < k
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)