mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
hs : SupIrred s
⊢ ∃ a, Iic a = s

pp: case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
⊢ (∃ a, Iic a = s) → SupIrred s

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
hs : SupIrred s
⊢ ∃ a, Iic a = s
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
t : Finset α
⊢ (∃ u, (∃ a t, a ∉ t ∧ insert a t = u ∧ #t = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜) →
    ∃ a ∈ t, ∃ u, #u = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜

Tactic:
·

Goal state after:
case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
t : Finset α
⊢ (∃ u, (∃ a t, a ∉ t ∧ insert a t = u ∧ #t = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜) →
    ∃ a ∈ t, ∃ u, #u = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
⊢ (∃ a, Iic a = s) → SupIrred s

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
s : LowerSet α
inst✝ : Finite α
⊢ (∃ a, Iic a = s) → SupIrred s
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h✝ : ¬(Disjoint u b ∧ v ≤ b)
hba : b = a
⊢ Disjoint v a

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h✝ : ¬(Disjoint u b ∧ v ≤ b)
hba : b = a
⊢ Disjoint v a
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) → ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k

pp: case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k) → ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) → ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
h : a ∈ s ∧ compress u v a ∈ s
⊢ (a ⊔ v) \ u ∈ s

pp: case inr
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
hba : compress u v b = a
⊢ (a ⊔ v) \ u ∈ s

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
h : a ∈ s ∧ compress u v a ∈ s
⊢ (a ⊔ v) \ u ∈ s
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k) → ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k) → ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
s : LowerSet { a // SupIrred a }
a : { a // SupIrred a }
ha : a ∈ ↑{ carrier := {b | ↑b ≤ (↑s).toFinset.sup Subtype.val}, lower' := ⋯ }
⊢ a ∈ ↑s

pp: case refine_2
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
s : LowerSet { a // SupIrred a }
a : { a // SupIrred a }
ha : a ∈ ↑s
⊢ a ∈ ↑{ carrier := {b | ↑b ≤ (↑s).toFinset.sup Subtype.val}, lower' := ⋯ }

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
s : LowerSet { a // SupIrred a }
a : { a // SupIrred a }
ha : a ∈ ↑{ carrier := {b | ↑b ≤ (↑s).toFinset.sup Subtype.val}, lower' := ⋯ }
⊢ a ∈ ↑s
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ (a ⊔ v) \ u ∈ s

pp: case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : ¬(Disjoint u b ∧ v ≤ b)
hba : b = a
⊢ (a ⊔ v) \ u ∈ s

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : Disjoint u b ∧ v ≤ b
hba : (b ⊔ u) \ v = a
⊢ (a ⊔ v) \ u ∈ s
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
s : LowerSet { a // SupIrred a }
a : { a // SupIrred a }
ha : a ∈ ↑s
⊢ a ∈ ↑{ carrier := {b | ↑b ≤ (↑s).toFinset.sup Subtype.val}, lower' := ⋯ }

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
s : LowerSet { a // SupIrred a }
a : { a // SupIrred a }
ha : a ∈ ↑s
⊢ a ∈ ↑{ carrier := {b | ↑b ≤ (↑s).toFinset.sup Subtype.val}, lower' := ⋯ }
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case pos
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
h : IsEmpty α
⊢ α ↪o Set { a // SupIrred a }

pp: case neg
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
h : Nonempty α
⊢ α ↪o Set { a // SupIrred a }

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
h : IsEmpty α
⊢ α ↪o Set { a // SupIrred a }
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : ¬(Disjoint u b ∧ v ≤ b)
hba : b = a
⊢ (a ⊔ v) \ u ∈ s

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
ha : a ∉ s
b : α
hb : b ∈ s
h : ¬(Disjoint u b ∧ v ≤ b)
hba : b = a
⊢ (a ⊔ v) \ u ∈ s
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hva : v ≤ a
hua : Disjoint u a
left✝ : a ∈ s
ha : (a ⊔ u) \ v ∈ s
⊢ (a ⊔ u) \ v ∈ s

pp: case inr
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
hva : v ≤ compress u v b
hua : Disjoint u (compress u v b)
left✝ : compress u v b ∉ s
⊢ (compress u v b ⊔ u) \ v ∈ s

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hva : v ≤ a
hua : Disjoint u a
left✝ : a ∈ s
ha : (a ⊔ u) \ v ∈ s
⊢ (a ⊔ u) \ v ∈ s
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case succ.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s) → ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s

pp: case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s) → ∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s

Tactic:
·

Goal state after:
case succ.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s) → ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s) → ∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s

Tactic:
·

Goal state after:
case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s) → ∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : #t + (k + 1) = #s
⊢ #t + 1 ≤ #s

Tactic:
by lia

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
ha : a ∈ s ∧ compress u v a ∈ s
⊢ a ∈ s

pp: case inr
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hb : b ∈ s
h : compress u v b = a
⊢ a ∈ s

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
ha : a ∈ s ∧ compress u v a ∈ s
⊢ a ∈ s
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ a ∈ s

pp: case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hb : b ∈ s
h✝ : ¬(Disjoint u b ∧ v ≤ b)
h : b = a
⊢ a ∈ s

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hb : b ∈ s
h✝ : Disjoint u b ∧ v ≤ b
h : (b ⊔ u) \ v = a
⊢ a ∈ s
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hb : b ∈ s
h✝ : ¬(Disjoint u b ∧ v ≤ b)
h : b = a
⊢ a ∈ s

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hb : b ∈ s
h✝ : ¬(Disjoint u b ∧ v ≤ b)
h : b = a
⊢ a ∈ s
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : Disjoint u a ∧ v ⊆ a
⊢ #((a ⊔ u) \ v) = #a

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : ¬(Disjoint u a ∧ v ⊆ a)
⊢ #a = #a

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : Disjoint u a ∧ v ⊆ a
⊢ #((a ⊔ u) \ v) = #a
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: case empty.inl
α : Type u_1
inst✝ : DecidableEq α
ℬ : Finset (Finset α)
hℬ : IsLowerSet ↑ℬ
hℬs : ℬ = ∅ ∨ ℬ = {∅}
h𝒜 : IsLowerSet ↑∅
⊢ #∅ * #ℬ ≤ 2 ^ #∅ * #(∅ ∩ ℬ)

pp: case empty.inr
α : Type u_1
inst✝ : DecidableEq α
ℬ : Finset (Finset α)
hℬ : IsLowerSet ↑ℬ
hℬs : ℬ = ∅ ∨ ℬ = {∅}
h𝒜 : IsLowerSet ↑{∅}
⊢ #{∅} * #ℬ ≤ 2 ^ #∅ * #({∅} ∩ ℬ)

Tactic:
·

Goal state after:
case empty.inl
α : Type u_1
inst✝ : DecidableEq α
ℬ : Finset (Finset α)
hℬ : IsLowerSet ↑ℬ
hℬs : ℬ = ∅ ∨ ℬ = {∅}
h𝒜 : IsLowerSet ↑∅
⊢ #∅ * #ℬ ≤ 2 ^ #∅ * #(∅ ∩ ℬ)
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: case empty.inr.inl
α : Type u_1
inst✝ : DecidableEq α
h𝒜 : IsLowerSet ↑{∅}
hℬ : IsLowerSet ↑∅
⊢ #{∅} * #∅ ≤ 2 ^ #∅ * #({∅} ∩ ∅)

pp: case empty.inr.inr
α : Type u_1
inst✝ : DecidableEq α
h𝒜 hℬ : IsLowerSet ↑{∅}
⊢ #{∅} * #{∅} ≤ 2 ^ #∅ * #({∅} ∩ {∅})

Tactic:
·

Goal state after:
case empty.inr.inl
α : Type u_1
inst✝ : DecidableEq α
h𝒜 : IsLowerSet ↑{∅}
hℬ : IsLowerSet ↑∅
⊢ #{∅} * #∅ ≤ 2 ^ #∅ * #({∅} ∩ ∅)
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : ¬(Disjoint u a ∧ v ⊆ a)
⊢ #a = #a

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : ¬(Disjoint u a ∧ v ⊆ a)
⊢ #a = #a
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: case empty.inr.inr
α : Type u_1
inst✝ : DecidableEq α
h𝒜 hℬ : IsLowerSet ↑{∅}
⊢ #{∅} * #{∅} ≤ 2 ^ #∅ * #({∅} ∩ {∅})

Tactic:
·

Goal state after:
case empty.inr.inr
α : Type u_1
inst✝ : DecidableEq α
h𝒜 hℬ : IsLowerSet ↑{∅}
⊢ #{∅} * #{∅} ≤ 2 ^ #∅ * #({∅} ∩ {∅})
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
s : Finset α
hs : s ∈ 𝒜 ∧ compress u v s ∈ 𝒜
⊢ #s = r

pp: case inr
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
t : Finset α
ht : t ∈ 𝒜
huvt : compress u v t ∉ 𝒜
⊢ #(compress u v t) = r

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
s : Finset α
hs : s ∈ 𝒜 ∧ compress u v s ∈ 𝒜
⊢ #s = r
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case inr
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
t : Finset α
ht : t ∈ 𝒜
huvt : compress u v t ∉ 𝒜
⊢ #(compress u v t) = r

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
t : Finset α
ht : t ∈ 𝒜
huvt : compress u v t ∉ 𝒜
⊢ #(compress u v t) = r
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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∉ ∂ 𝒜
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s

pp: case pos
α : 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s

Tactic:
·

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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∉ ∂ 𝒜
⊢ s ∈ ∂ 𝒜 ∧ compress u v s ∈ ∂ 𝒜 ∨ s ∉ ∂ 𝒜 ∧ ∃ b ∈ ∂ 𝒜, compress u v b = s
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case ind.inl
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
m : ℕ
ih : ∀ (𝒜 : Finset (Finset α)), #𝒜 < m → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
a : Finset α
h𝒜₁ : {a}.Nonempty
h𝒜₂ : univ ∉ {a}
hm : m = #{a}
⊢ supSum {a} = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

pp: case ind.inr
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
m : ℕ
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
hm : m = #𝒜
ih : ∀ (𝒜 : Finset (Finset α)), #𝒜 < m → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
h𝒜₃ : 𝒜.Nontrivial
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
·

Goal state after:
case ind.inl
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
m : ℕ
ih : ∀ (𝒜 : Finset (Finset α)), #𝒜 < m → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
a : Finset α
h𝒜₁ : {a}.Nonempty
h𝒜₂ : univ ∉ {a}
hm : m = #{a}
⊢ supSum {a} = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
huvs : ¬(Disjoint u s ∧ v ⊆ s)
⊢ s ∈ ∂ 𝒜

pp: case pos
α : 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
huvs : Disjoint u s ∧ v ⊆ s
⊢ (s ⊔ u) \ v ∈ ∂ 𝒜

Tactic:
·

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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
s : Finset α
hs' : s ∈ ∂ 𝒜'
hs : s ∈ ∂ 𝒜
huvs : ¬(Disjoint u s ∧ v ⊆ s)
⊢ s ∈ ∂ 𝒜
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case ind.inr.zero
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
h𝒜₃ : 𝒜.Nontrivial
hm : 0 = #𝒜
ih : ∀ (𝒜 : Finset (Finset α)), #𝒜 < 0 → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

pp: case ind.inr.succ
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
h𝒜₃ : 𝒜.Nontrivial
n✝ : ℕ
hm : n✝ + 1 = #𝒜
ih :
  ∀ (𝒜 : Finset (Finset α)), #𝒜 < n✝ + 1 → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
·

Goal state after:
case ind.inr.zero
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
h𝒜₃ : 𝒜.Nontrivial
hm : 0 = #𝒜
ih : ∀ (𝒜 : Finset (Finset α)), #𝒜 < 0 → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∈ u
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜

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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜

Tactic:
·

Goal state after:
case pos
α : 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∈ u
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜
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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜

Tactic:
·

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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case neg.refine_1
α : 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ a ∈ (t ⊔ u) \ v

pp: case neg.refine_2
α : 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ ((t ⊔ u) \ v).erase a = (t.erase a ⊔ u) \ v

Tactic:
·

Goal state after:
case neg.refine_1
α : 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 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ a ∈ (t ⊔ u) \ v