mathlib-initiative/mathlib-tactics huggingface dataset:
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 β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ (f₁ s + 0) * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

pp: case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ (0 + f₁ (insert a s)) * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

pp: case neg
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ (0 + 0) * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ (f₁ s + 0) * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∈ t
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∉ t
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∈ t
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
a : {A ∈ 𝒜 | compress U V A ∉ 𝒜} = ∅
⊢ {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ ∅ = 𝒜

Tactic:
union_empty

Goal state after:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
a : {A ∈ 𝒜 | compress U V A ∉ 𝒜} = ∅
⊢ {a ∈ 𝒜 | compress U V a ∈ 𝒜} = 𝒜
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ ∅ = 𝒜
a : {A ∈ 𝒜 | compress U V A ∉ 𝒜} = ∅
⊢ {a ∈ 𝒜 | compress U V a ∈ 𝒜} = 𝒜

Tactic:
union_empty

Goal state after:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} = 𝒜
a : {A ∈ 𝒜 | compress U V A ∉ 𝒜} = ∅
⊢ {a ∈ 𝒜 | compress U V a ∈ 𝒜} = 𝒜
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∉ t
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∉ t
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∈ 𝒜 ∧ u.erase a ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

pp: case inr
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∈ 𝒜 ∧ u.erase a ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∉ s
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case pos.inl
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

pp: case pos.inr
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∉ 𝒜 ∧ insert a v ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
·

Goal state after:
case pos.inl
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case ha
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∈ ℬ
⊢ 0 ≤ f₄ (s ∪ t) + f₄ (s ∪ insert a t)

pp: case hbc
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∈ ℬ
⊢ f₃ (s ∩ t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t)

Tactic:
·

Goal state after:
case ha
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∈ ℬ
⊢ 0 ≤ f₄ (s ∪ t) + f₄ (s ∪ insert a t)
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case hbc
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∈ ℬ
⊢ f₃ (s ∩ t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t)

Tactic:
·

Goal state after:
case hbc
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∈ ℬ
⊢ f₃ (s ∩ t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t)
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∉ s
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∉ s
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case mp
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ s → x ∈ {x | (mkClasses c H) x y}

pp: case mpr
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ {x | (mkClasses c H) x y} → x ∈ s

Tactic:
·

Goal state after:
case mp
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ s → x ∈ {x | (mkClasses c H) x y}
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case mpr
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ {x | (mkClasses c H) x y} → x ∈ s

Tactic:
·

Goal state after:
case mpr
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ {x | (mkClasses c H) x y} → x ∈ s
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case left
α : Type u_1
r : Setoid α
f : α → ↑r.classes := ⋯
f_respects_relation : ∀ (a b : α), r a b → f a = f b
⊢ Function.Injective (Quot.lift f f_respects_relation)

pp: case right
α : Type u_1
r : Setoid α
f : α → ↑r.classes := ⋯
f_respects_relation : ∀ (a b : α), r a b → f a = f b
⊢ Function.Surjective (Quot.lift f f_respects_relation)

Tactic:
·

Goal state after:
case left
α : Type u_1
r : Setoid α
f : α → ↑r.classes := ⋯
f_respects_relation : ∀ (a b : α), r a b → f a = f b
⊢ Function.Injective (Quot.lift f f_respects_relation)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
A : Finset (Fin n)
hA : A ∈ {a ∈ 𝒜 | compress U V a ∉ 𝒜}
⊢ ∑ x ∈ image Fin.val (compress U V A), 2 ^ x < ∑ x ∈ image Fin.val A, 2 ^ x

Tactic:
rw [geomSum_lt_geomSum_iff_toColex_lt_toColex le_rfl,
    toColex_image_lt_toColex_image Fin.val_strictMono]

Goal state after:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
A : Finset (Fin n)
hA : A ∈ {a ∈ 𝒜 | compress U V a ∉ 𝒜}
⊢ toColex (compress U V A) < toColex A
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 β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∉ ℬ
h✝ : insert a t ∈ ℬ
⊢ f₁ s * 0 + f₁ s * f₂ (insert a t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

pp: case neg
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∉ ℬ
h✝ : insert a t ∉ ℬ
⊢ f₁ s * 0 + f₁ s * 0 ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∉ ℬ
h✝ : insert a t ∈ ℬ
⊢ f₁ s * 0 + f₁ s * f₂ (insert a t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inl
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) := {t | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : usable = ∅
⊢ ∃ ℬ, #(∂ ℬ) ≤ #(∂ 𝒜) ∧ #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ

pp: case inr
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) := {t | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : usable.Nonempty
⊢ ∃ ℬ, #(∂ ℬ) ≤ #(∂ 𝒜) ∧ #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ

Tactic:
·

Goal state after:
case inl
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) := {t | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : usable = ∅
⊢ ∃ ℬ, #(∂ ℬ) ≤ #(∂ 𝒜) ∧ #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
u v : V
⊢ G.Reachable u v → Relation.ReflTransGen G.Adj u v

pp: case mpr
V : Type u
G : SimpleGraph V
u v : V
⊢ Relation.ReflTransGen G.Adj u v → G.Reachable u v

Tactic:
·

Goal state after:
case mp
V : Type u
G : SimpleGraph V
u v : V
⊢ G.Reachable u v → Relation.ReflTransGen G.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
u v : V
⊢ Relation.ReflTransGen G.Adj u v → G.Reachable u v

Tactic:
·

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
u v : V
⊢ Relation.ReflTransGen G.Adj u v → G.Reachable u v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
v' : V
hv' : v' ∈ H.verts
p : G.Walk v' v
hnp : p.Nil
⊢ v ∈ H.verts

pp: case neg
V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
v' : V
hv' : v' ∈ H.verts
p : G.Walk v' v
hnp : ¬p.Nil
⊢ v ∈ H.verts

Tactic:
·

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
v' : V
hv' : v' ∈ H.verts
p : G.Walk v' v
hnp : p.Nil
⊢ v ∈ H.verts
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
⊢ v ∈ H.verts

Tactic:
let rec aux {v' : V} (hv' : v' ∈ H.verts) (p : G.Walk v' v) : v ∈ H.verts := by
    by_cases hnp : p.Nil
    · exact hnp.eq ▸ hv'
    exact aux (H.edge_vert (h _ hv' _ (Walk.adj_snd hnp)).symm) p.tail
  termination_by p.length
  decreasing_by {
    rw [← Walk.length_tail_add_one hnp]
    lia
  }
  exact aux hu hr.some

Goal state after:
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 β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∉ ℬ
h✝ : insert a t ∉ ℬ
⊢ f₁ s * 0 + f₁ s * 0 ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∉ ℬ
h✝ : insert a t ∉ ℬ
⊢ f₁ s * 0 + f₁ s * 0 ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)