mathlib-initiative/mathlib-tactics huggingface dataset:
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₄ (insert a s ∪ insert a 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₄ (insert a s ∪ insert a t) ≤ collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
v w v' w' : V
⊢ (G.deleteEdges {s(v, w)}).Reachable v' w' → ∃ p, s(v, w) ∉ p.edges

pp: case mpr
V : Type u
G : SimpleGraph V
v w v' w' : V
⊢ (∃ p, s(v, w) ∉ p.edges) → (G.deleteEdges {s(v, w)}).Reachable v' w'

Tactic:
·

Goal state after:
case mp
V : Type u
G : SimpleGraph V
v w v' w' : V
⊢ (G.deleteEdges {s(v, w)}).Reachable v' w' → ∃ p, s(v, w) ∉ p.edges
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
⊢ ∃ p, s(v, w) ∉ p.edges

Tactic:
use p.map (.ofLE (by simp))

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: 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) ↑𝒜ᶜˢ
⊢ n - 2 * r ≤ n - r

Tactic:
by lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n → ∃ C, ∀ (v : V), C v < n

pp: case mpr
V : Type u
G : SimpleGraph V
n : ℕ
⊢ (∃ C, ∀ (v : V), C v < n) → G.Colorable n

Tactic:
·

Goal state after:
case mp
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n → ∃ C, ∀ (v : V), C v < n
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
v w v' w' : V
⊢ (∃ p, s(v, w) ∉ p.edges) → (G.deleteEdges {s(v, w)}).Reachable v' w'

Tactic:
·

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
v w v' w' : V
⊢ (∃ p, s(v, w) ∉ p.edges) → (G.deleteEdges {s(v, w)}).Reachable v' w'
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

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

Tactic:
·

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
n : ℕ
⊢ (∃ C, ∀ (v : V), C v < n) → G.Colorable n
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

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

pp: 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

Tactic:
·

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
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: 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 → ⟨C v, ⋯⟩ ≠ ⟨C w, ⋯⟩

Tactic:
·

Goal state after:
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 → ⟨C v, ⋯⟩ ≠ ⟨C w, ⋯⟩
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ G.Colorable (↑(Nat.find ?m.12)).toNat

pp: V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ {n' | G.Colorable n'}.Nonempty

Tactic:
·

Goal state after:
V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ G.Colorable (↑(Nat.find ?m.12)).toNat
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ {n' | G.Colorable n'}.Nonempty

Tactic:
·

Goal state after:
V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ {n' | G.Colorable n'}.Nonempty
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₁ (insert a s) * 0 + f₁ (insert a 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₁ (insert a s) * 0 + f₁ (insert a 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₁ (insert a s) * 0 + f₁ (insert a s) * f₂ (insert a t) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
v w : V
⊢ (G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges) → ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges

pp: case mpr
V : Type u
G : SimpleGraph V
v w : V
⊢ (∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges) → G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges

Tactic:
·

Goal state after:
case mp
V : Type u
G : SimpleGraph V
v w : V
⊢ (G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges) → ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp.refine_1
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ (Walk.cons ⋯ ↑p.toPath).IsCycle

pp: case mp.refine_2
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ s(v, w) ∈ (Walk.cons ⋯ ↑p.toPath).edges

Tactic:
·

Goal state after:
case mp.refine_1
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ (Walk.cons ⋯ ↑p.toPath).IsCycle
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp.refine_2
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ s(v, w) ∈ (Walk.cons ⋯ ↑p.toPath).edges

Tactic:
·

Goal state after:
case mp.refine_2
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ s(v, w) ∈ (Walk.cons ⋯ ↑p.toPath).edges
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
v w : V
⊢ (∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges) → G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges

Tactic:
·

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
v w : V
⊢ (∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges) → G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
h : ↑(card α) ≤ G.chromaticNumber
C : G.Coloring α
⊢ Surjective ⇑C

pp: case refine_2
V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
h : ∀ (C : G.Coloring α), Surjective ⇑C
⊢ ↑(card α) ≤ G.chromaticNumber

Tactic:
·

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
h : ↑(card α) ≤ G.chromaticNumber
C : G.Coloring α
⊢ Surjective ⇑C
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.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : ¬G.Adj x y
⊢ (G.deleteEdges {s(x, y)}).Connected

pp: case inr
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
⊢ (G.deleteEdges {s(x, y)}).Connected

Tactic:
·

Goal state after:
case inl
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : ¬G.Adj x y
⊢ (G.deleteEdges {s(x, y)}).Connected
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case e'_4.e'_1
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
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ n = Fintype.card (Fin n)

pp: case inr.convert_2
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
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ Fintype (Fin n)

pp: case inr.convert_5
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
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ Set.Sized r ↑(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)

Tactic:
·

Goal state after:
case e'_4.e'_1
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
this : n.choose r < #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ)
⊢ n = Fintype.card (Fin n)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case inr.inl
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∉ P.edges
⊢ (G.deleteEdges {s(x, y)}).Reachable x w

pp: case inr.inr
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∈ P.edges
⊢ (G.deleteEdges {s(x, y)}).Reachable x w

Tactic:
·

Goal state after:
case inr.inl
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∉ P.edges
⊢ (G.deleteEdges {s(x, y)}).Reachable x w
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
h : ∀ (C : G.Coloring α), Surjective ⇑C
⊢ ↑(card α) ≤ G.chromaticNumber

Tactic:
·

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
h : ∀ (C : G.Coloring α), Surjective ⇑C
⊢ ↑(card α) ≤ G.chromaticNumber
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: case inl
V : Type u
h✝ : Finite V
⊢ ⊤.chromaticNumber = ENat.card V

pp: case inr
V : Type u
h✝ : Infinite V
⊢ ⊤.chromaticNumber = ENat.card V

Tactic:
·

Goal state after:
case inl
V : Type u
h✝ : Finite V
⊢ ⊤.chromaticNumber = ENat.card V
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case inr
V : Type u
h✝ : Infinite V
⊢ ⊤.chromaticNumber = ENat.card V

Tactic:
·

Goal state after:
case inr
V : Type u
h✝ : Infinite V
⊢ ⊤.chromaticNumber = ENat.card V
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case calc_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset, collapse 𝒜 a f s = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s

pp: case calc_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s =
    ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s

pp: case calc_3
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s = ∑ s ∈ 𝒜, f s

Tactic:
·

Goal state after:
case calc_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset, collapse 𝒜 a f s = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
h : 2 ≤ G.chromaticNumber
⊢ G ≠ ⊥

pp: case refine_2
V : Type u
G : SimpleGraph V
h : G ≠ ⊥
⊢ 2 ≤ G.chromaticNumber

Tactic:
·

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
h : 2 ≤ G.chromaticNumber
⊢ G ≠ ⊥
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
h : G = ⊥
h' : IsEmpty V
⊢ G.chromaticNumber < 2

pp: case neg
V : Type u
G : SimpleGraph V
h : G = ⊥
h' : ¬IsEmpty V
⊢ G.chromaticNumber < 2

Tactic:
·

Goal state after:
case pos
V : Type u
G : SimpleGraph V
h : G = ⊥
h' : IsEmpty V
⊢ G.chromaticNumber < 2
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
h : G = ⊥
h' : ¬IsEmpty V
⊢ G.chromaticNumber < 2

Tactic:
·

Goal state after:
case neg
V : Type u
G : SimpleGraph V
h : G = ⊥
h' : ¬IsEmpty V
⊢ G.chromaticNumber < 2
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
⊢ ¬(G.deleteEdges {s(y, x)}).Reachable u x

Tactic:
·

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
⊢ ¬(G.deleteEdges {s(y, x)}).Reachable u x
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
h : G ≠ ⊥
⊢ 2 ≤ G.chromaticNumber

Tactic:
·

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
h : G ≠ ⊥
⊢ 2 ≤ G.chromaticNumber
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
⊢ ¬(G.deleteEdges {s(y, x)}).Reachable v x

Tactic:
·

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
hxu : x ≠ u
hxv : x ≠ v
hx : (G.neighborSet x).Subsingleton
hxw : x ∈ w.support
y : V
hxy : G.Adj x y
⊢ ¬(G.deleteEdges {s(y, x)}).Reachable v x
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case pos
V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : C (Sum.inl v) = b
⊢ ∃ a, C a = b

pp: case neg
V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : ¬C (Sum.inl v) = b
⊢ ∃ a, C a = b

Tactic:
·

Goal state after:
case pos
V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : C (Sum.inl v) = b
⊢ ∃ a, C a = b
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case pos
V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : ¬C (Sum.inl v) = b
he' : C (Sum.inr w) = b
⊢ ∃ a, C a = b

pp: case neg
V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : ¬C (Sum.inl v) = b
he' : ¬C (Sum.inr w) = b
⊢ ∃ a, C a = b

Tactic:
·

Goal state after:
case pos
V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : ¬C (Sum.inl v) = b
he' : C (Sum.inr w) = b
⊢ ∃ a, C a = b
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case neg
V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : ¬C (Sum.inl v) = b
he' : ¬C (Sum.inr w) = b
⊢ ∃ a, C a = b

Tactic:
·

Goal state after:
case neg
V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
h : (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)
he : ¬C (Sum.inl v) = b
he' : ¬C (Sum.inr w) = b
⊢ ∃ a, C a = b