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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ⊆ s) ∧ (s ⊔ U) \ V ≠ s
⊢ ∃ w ∈ s \ ((s ⊔ U) \ V), {a ∈ (s ⊔ U) \ V | w < a} = {a ∈ s | w < a}

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ⊆ s) ∧ (s ⊔ U) \ V ≠ s
⊢ ∃ w ∈ s \ ((s ⊔ U) \ V), {a ∈ (s ⊔ U) \ V | w < a} = {a ∈ s | w < a}
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝒜 # k ∪ ∂ (falling (k + 1) 𝒜) ↔ s ∈ falling k 𝒜
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ image (fun t ↦ univ ∩ t) 𝒜 = univ ↔ 𝒜 = univ

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ image (fun t ↦ univ ∩ t) 𝒜 = univ ↔ 𝒜 = univ
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ s ∈ 𝒜.biUnion powerset

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ s ∈ 𝒜.biUnion powerset
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
⊢ 𝒜.shatterer.Shatters s ↔ 𝒜.Shatters s

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
⊢ 𝒜.shatterer.Shatters s ↔ 𝒜.Shatters s
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
s : Finset α
h₁ : s ∈ ∂ (falling n 𝒜)
h₂ : s ∈ 𝒜 # m
⊢ False

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
s : Finset α
h₁ : s ∈ ∂ (falling n 𝒜)
h₂ : s ∈ 𝒜 # m
⊢ False
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ #𝒜.shatterer ≤ ∑ k ≤ 𝒜.vcDim, (Fintype.card α).choose k

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ #𝒜.shatterer ≤ ∑ k ≤ 𝒜.vcDim, (Fintype.card α).choose k
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 ∉ 𝒜}
⊢ ∑ a ∈ compress U V A, 2 ^ ↑a < ∑ a ∈ A, 2 ^ ↑a

Tactic:
[

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 ∉ 𝒜}
⊢ ∑ a ∈ compress U V A, 2 ^ ↑a < ∑ a ∈ A, 2 ^ ↑a
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
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
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 𝒜
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)
⊢ ∃ ℬ, #(∂ ℬ) ≤ #(∂ 𝒜) ∧ #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ

Tactic:
obtain ⟨-, hUV', hu, hv, hmax⟩ := hUV.2.1

Goal state after:
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
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 𝒜
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)
hUV' : #(U, V).1 = #(U, V).2
hu : (U, V).1.Nonempty
hv : (U, V).2.Nonempty
hmax : (U, V).1.max' hu < (U, V).2.max' hv
⊢ ∃ ℬ, #(∂ ℬ) ≤ #(∂ 𝒜) ∧ #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
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)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
h : G.IsUniversal v
⊢ G.Connected

Tactic:
refine connected_iff _ |>.mpr ⟨fun u w ↦ ?_, ⟨v⟩⟩

Goal state after:
V : Type u
G : SimpleGraph V
v : V
h : G.IsUniversal v
u w : V
⊢ G.Reachable u w
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
⊢ v ∈ ⋃ c, ⋃ (_ : c.supp ⊆ c'.supp), c.supp ↔ v ∈ c'.supp

Tactic:
[

Goal state after:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
⊢ v ∈ ⋃ c, ⋃ (_ : c.supp ⊆ c'.supp), c.supp ↔ v ∈ c'.supp
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case refine_2
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
⊢ ∀ ⦃s t : Finset (Fin n)⦄, s ∈ 𝒞 → toColex t < toColex s ∧ #t = r → t ∈ 𝒞

Tactic:
[

Goal state after:
case refine_2
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
⊢ ∀ ⦃s t : Finset (Fin n)⦄, s ∈ 𝒞 → toColex t < toColex s ∧ #t = r → t ∈ 𝒞
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ Pairwise fun c c' ↦ Disjoint c.supp c'.supp

Tactic:
[

Goal state after:
V : Type u
G : SimpleGraph V
⊢ Pairwise fun c c' ↦ Disjoint c.supp c'.supp
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := ⋯
𝒞 : Finset (Finset (Fin n)) := ⋯
this✝ : Set.Sized r ↑𝒞
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ #A = r
HB₁ : toColex B < toColex A
HB₂ : #B = r
t : Fin n
ht : t ∈ B
this : toColex (image Fin.val B) < toColex (image Fin.val A)
⊢ ∀ b ∈ image Fin.val A, b < k

Tactic:
[

Goal state after:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := ⋯
𝒞 : Finset (Finset (Fin n)) := ⋯
this✝ : Set.Sized r ↑𝒞
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ #A = r
HB₁ : toColex B < toColex A
HB₂ : #B = r
t : Fin n
ht : t ∈ B
this : toColex (image Fin.val B) < toColex (image Fin.val A)
⊢ ∀ b ∈ image Fin.val A, b < k
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inr
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this✝ : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this : r ≤ n
⊢ False

Tactic:
have : 1 ≤ n := ‹1 ≤ r›.trans ‹r ≤ n›

Goal state after:
case inr
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this✝¹ : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this✝ : r ≤ n
this : 1 ≤ n
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
⊢ s(v, w) ∉ (Walk.map (Hom.ofLE ⋯) p).edges

Tactic:
[

Goal state after:
case h
V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
⊢ s(v, w) ∉ (Walk.map (Hom.ofLE ⋯) p).edges
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inr
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this✝² : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
kk : (n - 1).choose (n - r - (n - 2 * r)) ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ False

Tactic:
this

Goal state after:
case inr
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this✝² : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), C v < n
⊢ G.Colorable n

Tactic:
refine ⟨Coloring.mk ?_ ?_⟩

Goal state after:
case mpr.refine_1
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), C v < n
⊢ V → Fin n

case mpr.refine_2
V : Type u
G : SimpleGraph V
n : ℕ
C : G.Coloring ℕ
Cf : ∀ (v : V), C v < n
⊢ ∀ {v w : V}, G.Adj v w → ?mpr.refine_1 v ≠ ?mpr.refine_1 w
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₁ (insert a s) * 0 + f₁ (insert a 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₁ (insert a s) * 0 + f₁ (insert a s) * 0 ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ 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 β
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 ∉ 𝒜
⊢ (0 + 0) * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
hh : G ≠ ⊤
this : ↑(card V) ≤ ↑(card V) - 1
⊢ False

Tactic:
← ENat.natCast_one,

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
hh : G ≠ ⊤
this : ↑(card V) ≤ ↑(card V) - ↑1
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
⊢ ∑ v ∈ s, G.degree v = ∑ w ∈ t, G.degree w

Tactic:
[

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
⊢ ∑ v ∈ s, G.degree v = ∑ w ∈ t, G.degree w
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
⊢ ∑ v ∈ s.attach, #(bipartiteAbove G.Adj t ↑v) = ∑ w ∈ t.attach, #(bipartiteBelow G.Adj s ↑w)

Tactic:
[

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
⊢ ∑ v ∈ s.attach, #(bipartiteAbove G.Adj t ↑v) = ∑ w ∈ t.attach, #(bipartiteBelow G.Adj s ↑w)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : G.IsBipartiteWith ↑s ↑t
hsub : G.support.toFinset ⊆ s ∪ t
⊢ ∑ v ∈ s ∪ t, G.degree v = 2 * #G.edgeFinset

Tactic:
rw [← Finset.sum_subset hsub, ← sum_degrees_support_eq_twice_card_edges]

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : G.IsBipartiteWith ↑s ↑t
hsub : G.support.toFinset ⊆ s ∪ t
⊢ ∀ x ∈ s ∪ t, x ∉ G.support.toFinset → G.degree x = 0
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected
v : ↑H.verts
inst✝ : Fintype ↑(H.neighborSet ↑v)
⊢ H.degree ↑v = 0 ↔ H.verts.Subsingleton

Tactic:
by
  refine ⟨fun hv ↦ Set.not_nontrivial_iff.mp fun hn ↦ ?_, (degree_eq_zero_of_subsingleton H _ ·)⟩
  have := hn.coe_sort
  simpa [hv] using h.coe.degree_pos_of_nontrivial v

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : α → β
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t
⊢ (∑ a ∈ s, f₁ a) * ∑ a ∈ t, f₂ a ≤ (∑ a ∈ s ⊼ t, f₃ a) * ∑ a ∈ s ⊻ t, f₄ a

Tactic:
obtain ⟨β, _, _, g, hg⟩ := exists_birkhoff_representation L

Goal state after:
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
⊢ (∑ a ∈ s, f₁ a) * ∑ a ∈ t, f₂ a ≤ (∑ a ∈ s ⊼ t, f₃ a) * ∑ a ∈ s ⊻ t, f₄ a
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case refine_1.inl.inl
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
a b : ↥L
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 (g b) ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ∩ g b) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g a ∪ g b)

Tactic:
[

Goal state after:
case refine_1.inl.inl
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
a b : ↥L
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 (g b) ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ∩ g b) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g a ∪ g b)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
s : Finset V
inst✝ : DecidableRel G.Adj
hv : v ∈ s
h_bipartite : (between (↑s) (↑s)ᶜ G).IsBipartiteWith ↑s ↑sᶜ
⊢ G.degree v ≤ (between (↑s) (↑s)ᶜ G).degree v + #s

Tactic:
[

Goal state after:
V : Type u_1
v : V
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
s : Finset V
inst✝ : DecidableRel G.Adj
hv : v ∈ s
h_bipartite : (between (↑s) (↑s)ᶜ G).IsBipartiteWith ↑s ↑sᶜ
⊢ G.degree v ≤ (between (↑s) (↑s)ᶜ G).degree v + #s
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
s : Finset V
inst✝ : DecidableRel G.Adj
hw : w ∈ sᶜ
h_bipartite : (between (↑s) (↑s)ᶜ G).IsBipartiteWith ↑s ↑sᶜ
⊢ G.degree w ≤ (between (↑s) (↑s)ᶜ G).degree w + #sᶜ

Tactic:
[

Goal state after:
V : Type u_1
w : V
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
s : Finset V
inst✝ : DecidableRel G.Adj
hw : w ∈ sᶜ
h_bipartite : (between (↑s) (↑s)ᶜ G).IsBipartiteWith ↑s ↑sᶜ
⊢ G.degree w ≤ (between (↑s) (↑s)ᶜ G).degree w + #sᶜ
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h✝ : G.IsBipartite
hv : Finite V
s t : Set V
h : G.IsBipartiteWith s t
⊢ 4 * G.edgeSet.encard ≤ ENat.card V ^ 2

Tactic:
h.encard_edgeSet_le

Goal state after:
V : Type u_1
G : SimpleGraph V
h✝ : G.IsBipartite
hv : Finite V
s t : Set V
h : G.IsBipartiteWith s t
⊢ 4 * (s.encard * t.encard) ≤ ENat.card V ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ w.toSubgraph.IsInduced ↔ w.IsChordless

Tactic:
[

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ w.toSubgraph.IsInduced ↔ w.IsChordless
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V ⊕ V
val✝¹ val✝ : V
hadj : G.bipartiteDoubleCover.Adj (Sum.inl val✝¹) (Sum.inl val✝)
⊢ (completeBipartiteGraph V V).Adj (Sum.inl val✝¹) (Sum.inl val✝)

Tactic:
by simp at hadj

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V ⊕ V
val✝¹ val✝ : V
hadj : G.bipartiteDoubleCover.Adj (Sum.inr val✝¹) (Sum.inr val✝)
⊢ (completeBipartiteGraph V V).Adj (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
by simp at hadj

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ sInf (Set.range fun x ↦ ↑x.reverse.length) = G.edist v u

Tactic:
[

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ sInf (Set.range fun x ↦ ↑x.reverse.length) = G.edist v u
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
⊢ completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover ↔ completeBipartiteGraph α β ⊑ G

Tactic:
[

Goal state after:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
⊢ completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover ↔ completeBipartiteGraph α β ⊑ G