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

Goal state before:
pp: case inr.cons.refine_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * Fintype.card (Finset α) + 2 * (#(s.biUnion f') * (Fintype.card (Finset α) - #(f' i))) ≤
    2 * 2 ^ Fintype.card α * 2 ^ Fintype.card α - 2 * 2 ^ Fintype.card α * 2 ^ (Fintype.card α - #(cons i s hi))

Tactic:
Fintype.card_finset,

Goal state after:
case inr.cons.refine_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * 2 ^ Fintype.card α + 2 * (#(s.biUnion f') * (2 ^ Fintype.card α - #(f' i))) ≤
    2 * 2 ^ Fintype.card α * 2 ^ Fintype.card α - 2 * 2 ^ Fintype.card α * 2 ^ (Fintype.card α - #(cons i s hi))
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r ↑𝒜
hr' : Fintype.card α < r
⊢ ↑(#𝒜) / 0 ≤ ↑(#(∂ 𝒜)) / ↑((Fintype.card α).choose (r - 1))

Tactic:
div_zero

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r ↑𝒜
hr' : Fintype.card α < r
⊢ 0 ≤ ↑(#(∂ 𝒜)) / ↑((Fintype.card α).choose (r - 1))
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case inr
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ ↑(#𝒜) * ↑((Fintype.card α).choose (r - 1)) ≤ ↑(#(∂ 𝒜)) * ↑((Fintype.card α).choose r)

pp: case inr.hb
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < ↑((Fintype.card α).choose r)

pp: case inr.hd
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < ↑((Fintype.card α).choose (r - 1))

Tactic:
<;>

Goal state after:
case inr
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ ↑(#𝒜) * ↑((Fintype.card α).choose (r - 1)) ≤ ↑(#(∂ 𝒜)) * ↑((Fintype.card α).choose r)

case inr.hb
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < ↑((Fintype.card α).choose r)

case inr.hd
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
hr' : r ≤ Fintype.card α
h𝒜 : #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)
⊢ 0 < ↑((Fintype.card α).choose (r - 1))
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_3
α : 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)
⊢ #(memberSubfamily a 𝒜).shatterer + #(nonMemberSubfamily a 𝒜).shatterer ≤ #𝒜.shatterer

Tactic:
← card_union_add_card_inter,

Goal state after:
case refine_3
α : 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)
⊢ #((memberSubfamily a 𝒜).shatterer ∪ (nonMemberSubfamily a 𝒜).shatterer) +
      #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer) ≤
    #𝒜.shatterer
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ ↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) ≤ 1 * ↑((Fintype.card α).choose (Fintype.card α - Fintype.card α))

pp: 𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ 0 < ↑((Fintype.card α).choose (Fintype.card α - Fintype.card α))

Tactic:
<;>

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ ↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) ≤ 1 * ↑((Fintype.card α).choose (Fintype.card α - Fintype.card α))

𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ 0 < ↑((Fintype.card α).choose (Fintype.card α - Fintype.card α))
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
x _y : α
h : ∀ s ∈ c, x ∈ s → _y ∈ s
s : Set α
hs : s ∈ c
hy : _y ∈ s
⊢ x ∈ s

Tactic:
obtain ⟨t, ⟨ht, hx⟩, _⟩ := H x

Goal state after:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
x _y : α
h : ∀ s ∈ c, x ∈ s → _y ∈ s
s : Set α
hs : s ∈ c
hy : _y ∈ s
t : Set α
right✝ : ∀ (y : Set α), (fun b ↦ b ∈ c ∧ x ∈ b) y → y = t
ht : t ∈ c
hx : x ∈ t
⊢ x ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
⊢ G.connectedComponentMk v = c → G.connectedComponentMk w = c

pp: case mpr
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
⊢ G.connectedComponentMk w = c → G.connectedComponentMk v = c

Tactic:
<;>

Goal state after:
case mp
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
⊢ G.connectedComponentMk v = c → G.connectedComponentMk w = c

case mpr
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
⊢ G.connectedComponentMk w = c → G.connectedComponentMk v = c
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk v = c
⊢ G.connectedComponentMk w = c

pp: case mpr
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk w = c
⊢ G.connectedComponentMk v = c

Tactic:
<;>

Goal state after:
case mp
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk v = c
⊢ G.connectedComponentMk w = c

case mpr
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk w = c
⊢ G.connectedComponentMk v = c
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk v = c
⊢ G.connectedComponentMk w = G.connectedComponentMk v

pp: case mpr
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk w = c
⊢ G.connectedComponentMk v = G.connectedComponentMk w

Tactic:
<;>

Goal state after:
case mp
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk v = c
⊢ G.connectedComponentMk w = G.connectedComponentMk v

case mpr
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk w = c
⊢ G.connectedComponentMk v = G.connectedComponentMk w
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
⊢ C.toSimpleGraph.spanningCoe.Adj v w → v ∈ C.supp ∧ G.Adj v w

Tactic:
intro h
    simp_all only [map_adj, SetLike.coe_sort_coe, Subtype.exists, mem_supp_iff]
    obtain ⟨_, a, _, _, h₁, rfl, rfl⟩ := h
    exact ⟨a, h₁⟩

Goal state after:
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 - 1).succ

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 - 1).succ

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 - 1).succ

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
⊢ n = (n - 1).succ

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 - 1).succ

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 - 1).succ
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:
by rw [card_union_of_disjoint ‹_›]

Goal state after:
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 ≠ ⊤
a b : V
hne : a ≠ b
right✝ : ¬G.Adj a b
x : V
h' : ¬x ≠ b
⊢ a ∈ Finset.univ.erase b

Tactic:
by simp [hne]

Goal state after:
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 ≠ ⊤
⊢ False

Tactic:
have : G.chromaticNumber ≤ Fintype.card V - 1 := by
    obtain ⟨a, b, hne, _⟩ := ne_top_iff_exists_not_adj.mp hh
    apply chromaticNumber_le_iff_colorable.mpr
    suffices G.Coloring (Finset.univ.erase b) by simpa using Coloring.colorable this
    apply Coloring.mk (fun x ↦ if h' : x ≠ b then ⟨x, by simp [h']⟩ else ⟨a, by simp [hne]⟩)
    grind [Adj.ne', adj_symm]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
hh : G ≠ ⊤
this : G.chromaticNumber ≤ ↑(card V) - 1
⊢ False
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

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_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

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 inl
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
w : V ⊕ W
val✝ : V
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val✝) w → (Sum.inl val✝).isRight ≠ w.isRight

pp: case inr
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
w : V ⊕ W
val✝ : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val✝) w → (Sum.inr val✝).isRight ≠ w.isRight

Tactic:
<;>

Goal state after:
case inl
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
w : V ⊕ W
val✝ : V
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val✝) w → (Sum.inl val✝).isRight ≠ w.isRight

case inr
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
w : V ⊕ W
val✝ : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val✝) w → (Sum.inr val✝).isRight ≠ w.isRight
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case inl.inl
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ val✝ : V
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val✝¹) (Sum.inl val✝) → (Sum.inl val✝¹).isRight ≠ (Sum.inl val✝).isRight

pp: case inl.inr
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ : V
val✝ : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val✝¹) (Sum.inr val✝) → (Sum.inl val✝¹).isRight ≠ (Sum.inr val✝).isRight

pp: case inr.inl
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ : W
val✝ : V
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val✝¹) (Sum.inl val✝) → (Sum.inr val✝¹).isRight ≠ (Sum.inl val✝).isRight

pp: case inr.inr
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ val✝ : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val✝¹) (Sum.inr val✝) → (Sum.inr val✝¹).isRight ≠ (Sum.inr val✝).isRight

Tactic:
<;>

Goal state after:
case inl.inl
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ val✝ : V
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val✝¹) (Sum.inl val✝) → (Sum.inl val✝¹).isRight ≠ (Sum.inl val✝).isRight

case inl.inr
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ : V
val✝ : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val✝¹) (Sum.inr val✝) → (Sum.inl val✝¹).isRight ≠ (Sum.inr val✝).isRight

case inr.inl
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ : W
val✝ : V
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val✝¹) (Sum.inl val✝) → (Sum.inr val✝¹).isRight ≠ (Sum.inl val✝).isRight

case inr.inr
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ val✝ : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val✝¹) (Sum.inr val✝) → (Sum.inr val✝¹).isRight ≠ (Sum.inr val✝).isRight
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
⊢ {w | w ∈ t ∧ G.Adj v w} ⊆ t

Tactic:
exact Set.sep_subset t (G.Adj v ·)

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

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
hs : v ∈ s
ht : w ∈ t
⊢ (completeGraph (Fin 2)).Adj (s.indicator 1 v) (s.indicator 1 w)

pp: case inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
ht : v ∈ t
hs : w ∈ s
⊢ (completeGraph (Fin 2)).Adj (s.indicator 1 v) (s.indicator 1 w)

Tactic:
<;>

Goal state after:
case inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
hs : v ∈ s
ht : w ∈ t
⊢ (completeGraph (Fin 2)).Adj (s.indicator 1 v) (s.indicator 1 w)

case inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
ht : v ∈ t
hs : w ∈ s
⊢ (completeGraph (Fin 2)).Adj (s.indicator 1 v) (s.indicator 1 w)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
this : G.Adj u w.snd
s : Set (Sym2 V)
hs : s.encard < ↑2
⊢ (G.deleteEdges s).Reachable u w.snd

Tactic:
by_cases! h' : s = {s(u, w.snd)}

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
this : G.Adj u w.snd
s : Set (Sym2 V)
hs : s.encard < ↑2
h' : s = {s(u, w.snd)}
⊢ (G.deleteEdges s).Reachable u w.snd

case neg
V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
w : G.Walk u v
hw : w.IsPath
this : G.Adj u w.snd
s : Set (Sym2 V)
hs : s.encard < ↑2
h' : s ≠ {s(u, w.snd)}
⊢ (G.deleteEdges s).Reachable u w.snd
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
f₁ f₂ f₃ f₄ : Finset α → β
inst✝¹ : ExistsAddOfLE β
inst✝ : Finite α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (s t : Finset α), f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
this : Fintype α
⊢ ∀ ⦃s : Finset α⦄, s ⊆ univ → ∀ ⦃t : Finset α⦄, t ⊆ univ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
f₁ f₂ f₃ f₄ : Finset α → β
inst✝¹ : ExistsAddOfLE β
inst✝ : Finite α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (s t : Finset α), f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
this : Fintype α
⊢ 𝒜 ⊆ univ.powerset

pp: case refine_3
α : Type u_1
β : Type u_2
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
f₁ f₂ f₃ f₄ : Finset α → β
inst✝¹ : ExistsAddOfLE β
inst✝ : Finite α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (s t : Finset α), f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
this : Fintype α
⊢ ℬ ⊆ univ.powerset

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
f₁ f₂ f₃ f₄ : Finset α → β
inst✝¹ : ExistsAddOfLE β
inst✝ : Finite α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (s t : Finset α), f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
this : Fintype α
⊢ ∀ ⦃s : Finset α⦄, s ⊆ univ → ∀ ⦃t : Finset α⦄, t ⊆ univ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)

case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
f₁ f₂ f₃ f₄ : Finset α → β
inst✝¹ : ExistsAddOfLE β
inst✝ : Finite α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (s t : Finset α), f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
this : Fintype α
⊢ 𝒜 ⊆ univ.powerset

case refine_3
α : Type u_1
β : Type u_2
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
f₁ f₂ f₃ f₄ : Finset α → β
inst✝¹ : ExistsAddOfLE β
inst✝ : Finite α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (s t : Finset α), f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
this : Fintype α
⊢ ℬ ⊆ univ.powerset
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
w a b : V
hvw : G.Adj a w
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb✝ : b ∈ (G.subgraphOfAdj hvw).verts
hb : b = a ∨ b = w
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb✝⟩

pp: case inr
V : Type u
G : SimpleGraph V
v a b : V
hvw : G.Adj v a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb✝ : b ∈ (G.subgraphOfAdj hvw).verts
hb : b = v ∨ b = a
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb✝⟩

Tactic:
<;>

Goal state after:
case inl
V : Type u
G : SimpleGraph V
w a b : V
hvw : G.Adj a w
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb✝ : b ∈ (G.subgraphOfAdj hvw).verts
hb : b = a ∨ b = w
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb✝⟩

case inr
V : Type u
G : SimpleGraph V
v a b : V
hvw : G.Adj v a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb✝ : b ∈ (G.subgraphOfAdj hvw).verts
hb : b = v ∨ b = a
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb✝⟩
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
huv : G.IsEdgeReachable 2 u v
huy : ¬G.IsEdgeReachable 2 u x
⊢ ?m.25

Tactic:
by simpa [isEdgeReachable_two] using huy

Goal state after: