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

Goal state before:
pp: case refine_1
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 ↑𝒞
⊢ k.choose r ≤ #𝒜

Tactic:
]

Goal state after:
case refine_1
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 ↑𝒞
⊢ k.choose r ≤ #𝒜
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case e'_4.e'_3
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_1✝¹ : ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)
e_2✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
e_3✝ : (fun x ↦ V') ≍ fun x ↦ V'
e_1✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
⊢ (G.connectedComponentMk b✝).toSimpleGraph.Adj ≍ (G.connectedComponentMk b✝).toSimpleGraph.Adj

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case e'_5
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_1✝ : ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)
⊢ G.connectedComponentMk b✝ = G.connectedComponentMk b✝

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case e'_6
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_2✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
⊢ (fun x ↦ x ∈ G.connectedComponentMk b✝) = fun x ↦ x ∈ G.connectedComponentMk b✝

Tactic:
]

Goal state after:
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 ↑𝒞
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
⊢ ↑t < k

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 ↑𝒞
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
⊢ ↑t < k
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case map_rel'
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst✝ : NeZero n
C : G.Coloring (Fin n)
a b : β
left✝ : a ≠ b
w✝¹ w✝ : V
hadj : G.Adj w✝¹ w✝
ha : f w✝¹ = a
hb : f w✝ = b
⊢ (completeGraph (Fin n)).Adj (C w✝¹) (C w✝)

Tactic:
]

Goal state after:
case map_rel'
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst✝ : NeZero n
C : G.Coloring (Fin n)
a b : β
left✝ : a ≠ b
w✝¹ w✝ : V
hadj : G.Adj w✝¹ w✝
ha : f w✝¹ = a
hb : f w✝ = b
⊢ (completeGraph (Fin n)).Adj (C w✝¹) (C w✝)
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) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
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
⊢ toColex B < toColex A

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) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
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
⊢ toColex B < toColex A
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
hsx : G.connectedComponentMk a = i✝
hsy : G.connectedComponentMk a = j✝
⊢ False

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
hsx : G.connectedComponentMk a = i✝
hsy : G.connectedComponentMk a = j✝
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
hsx : G.connectedComponentMk a = i✝
hsy : i✝ = j✝
⊢ False

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
i✝ j✝ : G.ConnectedComponent
h : i✝ ≠ j✝
a : V
hsx : G.connectedComponentMk a = i✝
hsy : i✝ = j✝
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
hconn : G.Preconnected
u v : V
⊢ Nonempty (G.Walk u v)

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
hconn : G.Preconnected
u v : V
⊢ Nonempty (G.Walk u v)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ ⨅ n ∈ Set.ofPred G.Colorable, ↑n = ⨅ i, ⨅ (h : i ∈ {m | G.Colorable m}), ↑↑⟨i, h⟩

Tactic:
]

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

Goal state before:
pp: case e'_3
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
b : r = 0
⊢ ∀ (x : Finset (Fin n)), x ∉ 𝒜

Tactic:
]

Goal state after:
case e'_3
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
b : r = 0
⊢ ∀ (x : Finset (Fin n)), x ∉ 𝒜
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case e'_3
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
b : r = 0
A : Finset (Fin n)
HA : A ∈ 𝒜
⊢ #A = r

Tactic:
]

Goal state after:
case e'_3
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
b : r = 0
A : Finset (Fin n)
HA : A ∈ 𝒜
⊢ #A = r
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
h : G.Colorable n
⊢ ⨅ n ∈ Set.ofPred G.Colorable, ↑n = ⨅ a ∈ {n' | G.Colorable n'}, ↑a

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

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.Colorable n
⊢ {n' | G.Colorable n'}.Nonempty
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
⊢ (n - 1).choose (r - 1) < #𝒜

Tactic:
]

Goal state after:
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
⊢ (n - 1).choose (r - 1) < #𝒜
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n✝ : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst✝ : Fintype α
n : ℕ
hc : G.Colorable n
hn : card (Fin n) ≤ card α
⊢ G.Coloring α

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
n✝ : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
inst✝ : Fintype α
n : ℕ
hc : G.Colorable n
hn : card (Fin n) ≤ card α
⊢ G.Coloring α
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 r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ False

Tactic:
]

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.Connectivity.Connected

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
v w v' w' : V
p : G.Walk v' w'
h : s(v, w) ∉ p.edges
e : Sym2 V
ep : e ∈ p.edges
⊢ e ∈ G.edgeSet \ {s(v, w)}

Tactic:
]

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
v w v' w' : V
p : G.Walk v' w'
h : s(v, w) ∉ p.edges
e : Sym2 V
ep : e ∈ p.edges
⊢ e ∈ G.edgeSet \ {s(v, w)}
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
⊢ (∀ (x : G.Walk v w), s(v, w) ∈ x.edges) ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges

Tactic:
]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ ↑(sInf {n' | G.Colorable n'}) ≤ ↑n

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ ↑(sInf {n' | G.Colorable n'}) ≤ ↑n
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ ⨅ n ∈ Set.ofPred G.Colorable, ↑n ≠ ⊤ ↔ ∃ n, G.Colorable n

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
⊢ ⨅ n ∈ Set.ofPred G.Colorable, ↑n ≠ ⊤ ↔ ∃ n, G.Colorable n
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case e'_2.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
⊢ n = n

pp: case e'_2.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
⊢ 0 < n

Tactic:
]

Goal state after:
case e'_2.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
⊢ 0 < n
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ ↑n
this : ∃ n, G.Colorable n
⊢ G.Colorable n

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ ↑n
this : ∃ n, G.Colorable n
⊢ G.Colorable n
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
h : sInf {n' | G.Colorable n'} ≤ n
m : ℕ
hm : G.Colorable m
⊢ G.Colorable n

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
h : sInf {n' | G.Colorable n'} ≤ n
m : ℕ
hm : G.Colorable m
⊢ G.Colorable n
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
h : sInf {n' | G.Colorable n'} ≤ n
m : ℕ
hm : G.Colorable m
this : G.Colorable (sInf {n' | G.Colorable n'})
⊢ G.Colorable n

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
h : sInf {n' | G.Colorable n'} ≤ n
m : ℕ
hm : G.Colorable m
this : G.Colorable (sInf {n' | G.Colorable n'})
⊢ G.Colorable n
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
⊢ False

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
hc : c.IsTrail
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
⊢ False
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case e'_2.e'_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
⊢ r = r

pp: case e'_2.e'_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
⊢ 0 < r

Tactic:
]

Goal state after:
case e'_2.e'_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
⊢ 0 < r
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) * 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 ∈ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∉ ℬ
⊢ f₁ (insert a s) * 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
n : ℕ
⊢ G.Colorable (n + 1) ∧ ¬G.Colorable n ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n

Tactic:
]

Goal state after:
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

V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ {n' | G.Colorable n'}.Nonempty
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case e'_3.e'_6
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
⊢ r = r

pp: case e'_3.e'_6
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
⊢ 0 < r

Tactic:
]

Goal state after:
case e'_3.e'_6
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
⊢ 0 < r
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ G.Colorable 1

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ G.Colorable 1
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) ↑𝒜ᶜˢ
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ #𝒜 + #(∂^[n - 2 * r] 𝒜ᶜˢ) = #𝒜 + #(∂^[n - 2 * r] 𝒜ᶜˢ)

Tactic:
]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
⊢ 0 < sInf {n' | G.Colorable n'}

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
⊢ 0 < sInf {n' | G.Colorable n'}
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
hc : ((pvu.append puw).edges ++ pwv.edges).Nodup
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
⊢ False

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
c : G.Walk u u
he : s(v, w) ∈ c.edges
hw : w ∈ (c.takeUntil v ⋯).support
hv : v ∈ c.support
puw : G.Walk u w := (c.takeUntil v hv).takeUntil w hw
pwv : G.Walk w v := (c.takeUntil v hv).dropUntil w hw
pvu : G.Walk v u := c.dropUntil v hv
hc : ((pvu.append puw).edges ++ pwv.edges).Nodup
this : c = (puw.append pwv).append pvu
hbq : s(v, w) ∈ (pvu.append puw).edges
hpq' : s(v, w) ∈ pwv.edges
⊢ False
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) * f₂ (insert a t) ≤ 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) * f₂ (insert a 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
h : ∃ n, G.Colorable n
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
h : ∃ n, G.Colorable n
⊢ G.Colorable G.chromaticNumber.toNat
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: 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

Tactic:
]

Goal state after:
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
⊢ s(v, w) ∉ (↑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
⊢ s(v, w) ∉ (↑p.toPath).edges
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
⊢ ⨅ n ∈ Set.ofPred G.Colorable, ↑n ≤ ⨅ n ∈ Set.ofPred G'.Colorable, ↑n

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
V' : Type u_4
G' : SimpleGraph V'
h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n
⊢ ⨅ n ∈ Set.ofPred G.Colorable, ↑n ≤ ⨅ n ∈ Set.ofPred G'.Colorable, ↑n