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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
⊢ ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y ∈ 𝒜

Tactic:
refine
        sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) ?_
          (disjoint_of_subset_left (erase_subset _ _) disjoint_sdiff)

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this : v \ u = v
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
⊢ v.erase y ⊆ (insert x s ∪ v) \ u
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ 2 ^ Fintype.card α * #(ℬ ∩ 𝒜) ≤ #ℬ * #𝒜

Tactic:
exact hℬ.card_inter_le_finset h𝒜

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

Goal state before:
pp: case inl
β : Type u_2
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
⊢ a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀

Tactic:
rw [hcd] at h₀₁ h₁₀

Goal state after:
case inl
β : Type u_2
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ 0
h₀₁ : a₀ * b₁ ≤ 0
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : c₀ * d₁ = 0
⊢ a₀ * b₁ + a₁ * b₀ ≤ c₀ * d₁ + c₁ * d₀
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this : 𝒜 ⊆ {∅}
⊢ IsInitSeg (∂ 𝒜) (0 - 1)

Tactic:
have := shadow_monotone this

Goal state after:
case intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
this✝ : 𝒜 ⊆ {∅}
this : ∂ 𝒜 ⊆ ∂ {∅}
⊢ IsInitSeg (∂ 𝒜) (0 - 1)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
⊢ (B \ A).max' hV < (A \ B).max' hU

Tactic:
obtain hlt | heq | hgt := lt_trichotomy (max' _ hU) (max' _ hV)

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hlt : (A \ B).max' hU < (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
heq : (A \ B).max' hU = (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hgt : (B \ A).max' hV < (A \ B).max' hU
⊢ (B \ A).max' hV < (A \ B).max' hU
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 * f₂ t + f₁ s * 0 ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
rw [mul_zero, add_zero]
      exact (h ‹_› ‹_›).trans <| mul_le_mul (le_collapse_of_mem ‹_› h₃ rfl <|
        inter_mem_infs ‹_› ‹_›) (le_collapse_of_mem ‹_› h₄ rfl <| union_mem_sups ‹_› ‹_›)
        (h₄ _) <| collapse_nonneg h₃ _

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
huv : u ≠ v
hreach : G.Reachable u v
⊢ (G.neighborSet u).Nonempty

Tactic:
obtain ⟨_ | @⟨u, x, v, hadj, w'⟩⟩ := hreach

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
huv : u ≠ u
⊢ (G.neighborSet u).Nonempty

case cons
V : Type u
G : SimpleGraph V
u v : V
huv : u ≠ v
x : V
hadj : G.Adj u x
w' : G.Walk x v
⊢ (G.neighborSet u).Nonempty
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
hx : x ∈ f (hs.index x) ⁻¹' t
⊢ x ∈ ⋃ i, s i ∩ f i ⁻¹' t

Tactic:
exact mem_iUnion_of_mem (hs.index x) (mem_inter (hs.mem_index x) hx)

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

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

Tactic:
not_exists_not

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

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.Subgraph

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

Tactic:
apply Adj.reachable

Goal state after:
case inl.inr
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj a b
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Adj ⟨a, ha⟩ ⟨b, hb⟩
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

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

Tactic:
apply Adj.reachable

Goal state after:
case inr.inl
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj b a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Adj ⟨a, ha⟩ ⟨b, hb⟩
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
w : V
h' : G.Reachable u w
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
← ENat.natCast_le_natCast,

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
w : V
h' : G.Reachable u w
⊢ ↑(G.dist u w) ≤ ↑(G.dist u v + G.dist v w)
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Reachable v w
u : V
h' : G.Reachable u w
⊢ G.dist u w ≤ G.dist u v + G.dist v w

Tactic:
← ENat.natCast_le_natCast,

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Reachable v w
u : V
h' : G.Reachable u w
⊢ ↑(G.dist u w) ≤ ↑(G.dist u v + G.dist v w)
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : GeneralizedBooleanAlgebra α
s✝ t✝ s t : Finset α
⊢ map { toFun := ⇑liftLatticeHom, inj' := ⋯ } (s \\ t) =
    map { toFun := ⇑liftLatticeHom, inj' := ⋯ } s \\ map { toFun := ⇑liftLatticeHom, inj' := ⋯ } t

Tactic:
simp_rw [map_eq_image]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : GeneralizedBooleanAlgebra α
s✝ t✝ s t : Finset α
⊢ image (⇑{ toFun := ⇑liftLatticeHom, inj' := ⋯ }) (s \\ t) =
    image (⇑{ toFun := ⇑liftLatticeHom, inj' := ⋯ }) s \\ image (⇑{ toFun := ⇑liftLatticeHom, inj' := ⋯ }) t
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
⊢ p.bypass = p

Tactic:
apply bypass_eq_self_of_length_le_length_bypass

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
⊢ p.length ≤ p.bypass.length
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.length = G.dist v w
hl : 1 < G.dist v w
hnp : ¬p.Nil
this✝ : p.tail.tail.length < p.tail.length
this : p.tail.length < p.length
hv : v = p.getVert 2
⊢ G.dist v w ≤ p.tail.tail.length

Tactic:
simpa [hv, p.getVert_tail] using dist_le p.tail.tail

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : ↑wH.length = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := (Walk.boxProdLeft H x.2 wG).append (Walk.boxProdRight G y.1 wH)
⊢ w_app.length = wG.length + wH.length

Tactic:
unfold w_app Walk.boxProdLeft Walk.boxProdRight

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : ↑wH.length = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := (Walk.boxProdLeft H x.2 wG).append (Walk.boxProdRight G y.1 wH)
⊢ ((Walk.map (G.boxProdLeft H x.2).toHom wG).append (Walk.map (G.boxProdRight H y.1).toHom wH)).length =
    wG.length + wH.length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ (⊤.induce {u, v}).Preconnected

Tactic:
exact (top_induce_pair_connected_of_adj huv).preconnected

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

Goal state before:
pp: V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Preconnected

Tactic:
by
  rintro (v₁ | w₁) (v₂ | w₂)
  · exact ((hG v₁ v₂).map Embedding.sumInl.toHom).mono le_sup_left
  · exact (hG ..).sum_sup_edge (hH ..)
  · exact ((hG ..).sum_sup_edge (hH ..)).symm
  · exact ((hH w₁ w₂).map Embedding.sumInr.toHom).mono le_sup_left

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
a b : α
⊢ ReflTransGen (Function.swap (hasse α).Adj) b a

Tactic:
exact
    reflTransGen_of_pred _ (fun c hc => Or.inl <| pred_covBy_of_not_isMin hc.1.not_isMin)
      fun c hc => Or.inr <| pred_covBy_of_not_isMin hc.1.not_isMin

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∈ q.support
⊢ q = p.concat hadj

Tactic:
have hw : w ∉ p.support := hG.ne_mem_support_of_support_of_adj_of_isPath hq hp hadj.symm hv

Goal state after:
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hv : v ∈ q.support
hw : w ∉ p.support
⊢ q = p.concat hadj
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Finite V
this : (α : Type ?u.21) → [Finite α] → Fintype α
T : SimpleGraph V
hle : T ≤ G
hT : T.IsTree
⊢ Nat.card V ≤ Nat.card ↑G.edgeSet + 1

Tactic:
rw [Nat.card_eq_fintype_card, ← hT.card_edgeFinset, add_le_add_iff_right,
    Nat.card_eq_fintype_card, ← edgeFinset_card]

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
h : G.Connected
hV : Finite V
this : (α : Type u_1) → [Finite α] → Fintype α
T : SimpleGraph V
hle : T ≤ G
hT : T.IsTree
⊢ T.edgeFinset.card ≤ G.edgeFinset.card
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
h : G.Colorable 2
⊢ ∀ (u : α) (w : G.Walk u u), ¬Odd w.length

Tactic:
intro _ w ho

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
h : G.Colorable 2
u✝ : α
w : G.Walk u✝ u✝
ho : Odd w.length
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr.a
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w ∈ {i ∈ range r | c ≡ n + i [MOD r]}
mx : x ∈ {i ∈ range r | c ≡ n + i [MOD r]}
⊢ w = x

Tactic:
simp only [mem_filter, mem_range] at mw mx

Goal state after:
case inr.a
n r c : ℕ
hr : r > 0
w x : ℕ
mw : w < r ∧ c ≡ n + w [MOD r]
mx : x < r ∧ c ≡ n + x [MOD r]
⊢ w = x
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
⊢ #(turanGraph (n + r) r).edgeFinset = #(turanGraph n r).edgeFinset + n * (r - 1) + r.choose 2

Tactic:
rw [← mul_right_inj' two_ne_zero]

Goal state after:
n r : ℕ
⊢ 2 * #(turanGraph (n + r) r).edgeFinset = 2 * (#(turanGraph n r).edgeFinset + n * (r - 1) + r.choose 2)
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : Finite α
inst✝ : Nontrivial α
⊢ G.ediam = ⊤ ↔ G.diam = 0

Tactic:
diam_eq_zero_iff_ediam_eq_top

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝¹ : Finite α
inst✝ : Nontrivial α
⊢ G.ediam = ⊤ ↔ G.ediam = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Subsingleton α
u : α
⊢ G.radius = 0

Tactic:
radius_eq_zero_iff

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Subsingleton α
u : α
⊢ Nonempty α ∧ Subsingleton α
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
K : Set V
G : SimpleGraph V
v w : V
vK : v ∉ K
wK : w ∉ K
a : G.Adj v w
⊢ (induce Kᶜ G).Reachable ⟨v, vK⟩ ⟨w, wK⟩

Tactic:
apply Adj.reachable

Goal state after:
V : Type u
K : Set V
G : SimpleGraph V
v w : V
vK : v ∉ K
wK : w ∉ K
a : G.Adj v w
⊢ (induce Kᶜ G).Adj ⟨v, vK⟩ ⟨w, wK⟩
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
⊢ ↑N * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t) - ↑r * ↑t' * (↑t' - ↑t)

Tactic:
rw [← add_sub_cancel_right (N : ℝ) (r * t' : ℝ), sub_mul]

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
ε : ℝ
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
⊢ (↑N + ↑r * ↑t') * (↑t' - ↑t) - ↑r * ↑t' * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t) - ↑r * ↑t' * (↑t' - ↑t)
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (⇑C) (↑(insert w₁ s)) Set.univ
this : Set.SurjOn (⇑C) (↑(insert w₂ t)) Set.univ
x : α
hx : x ∈ ↑(insert w₁ s)
hcx : C x = C v
y : α
hy : y ∈ ↑(insert w₂ t)
hcy : C y = C v
⊢ False

Tactic:
rw [coe_insert] at *

Goal state after:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (⇑C) (insert w₁ ↑s) Set.univ
this : Set.SurjOn (⇑C) (insert w₂ ↑t) Set.univ
x : α
hx : x ∈ insert w₁ ↑s
hcx : C x = C v
y : α
hy : y ∈ insert w₂ ↑t
hcy : C y = C v
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
⊢ M.IsPerfectMatching ↔ ∀ (v : V), ∃! w, M.Adj v w

Tactic:
refine ⟨?_, fun hm => ⟨fun v _ => hm v, fun v => ?_⟩⟩

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
⊢ M.IsPerfectMatching → ∀ (v : V), ∃! w, M.Adj v w

case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : ∀ (v : V), ∃! w, M.Adj v w
v : V
⊢ v ∈ M.verts
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
⊢ Even (Fintype.card ↑c.supp)

Tactic:
by
  #adaptation_note /-- https://github.com/leanprover/lean4/pull/5020
  some instances that use the chain of coercions
  `[SetLike X], X → Set α → Sort _` are
  blocked by the discrimination tree. This can be fixed by redeclaring the instance for `X`
  using the double coercion but the proper fix seems to avoid the double coercion. -/
  let : DecidablePred fun x ↦ x ∈ (M.induce c.supp).verts := fun a ↦ G.instDecidableMemSupp c a
  have := (hM.induce_connectedComponent_isMatching c).even_card
  simp only [Subgraph.induce_verts, Set.toFinset_card] at this
  exact this

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

Goal state before:
pp: V : Type u_1
R : Type u_2
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : NonAssocSemiring R
v : V
vec : V → R
⊢ (degMatrix R G *ᵥ vec) v = ↑(G.degree v) * vec v

Tactic:
by
  rw [degMatrix, mulVec_diagonal]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v : V
⊢ (c.toSimpleGraph.spanningCoe.neighborSet v).Nonempty → (c.toSimpleGraph.spanningCoe.neighborSet v).ncard = 2

Tactic:
⟨w, hw⟩

Goal state after:
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v w : V
hw : w ∈ c.toSimpleGraph.spanningCoe.neighborSet v
⊢ (c.toSimpleGraph.spanningCoe.neighborSet v).ncard = 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
hr_ne_1 : r ≠ 1
⊢ (1 - 1 / (↑r - 1) + 1 / ((↑r - 1) * ↑r) + ε) * ↑n = (1 - 1 / ↑(r - 1) + ε') * ↑n

Tactic:
← Nat.cast_pred hr_pos,

Goal state after:
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
hr_ne_1 : r ≠ 1
⊢ (1 - 1 / ↑(r - 1) + 1 / (↑(r - 1) * ↑r) + ε) * ↑n = (1 - 1 / ↑(r - 1) + ε') * ↑n
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
hne : v ≠ w
⊢ #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2

Tactic:
rw [compl_adj] at ha

Goal state after:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ #(((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})) = n - (2 * k - μ) - 2
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
⊢ (M.spanningCoe ∆ M'.spanningCoe).IsAlternating M.spanningCoe

Tactic:
intro v w w' hww' hvw hvw'
  obtain ⟨v1, hm1, hv1⟩ := hM.1 (hM.2 v)
  obtain ⟨v2, hm2, hv2⟩ := hM'.1 (hM'.2 v)
  simp only [symmDiff_def] at *
  aesop

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective ⇑f
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
this✝ : IsAntichain H.Adj sᶜ
this : IsAntichain G.Adj (⇑f ⁻¹' sᶜ)
⊢ G.vertexCoverNum ≤ H.vertexCoverNum

Tactic:
have : G.IsVertexCover (f ⁻¹' s) :=
    isIndepSet_compl_iff_isVertexCover.mp <| G.isIndepSet_iff_isAntichain_adj.mpr this

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
h : G ⊑ H
f : G →g H
hf : Function.Injective ⇑f
s : Set W
hs₁ : s.encard = H.vertexCoverNum
hs₂ : H.IsVertexCover s
this✝¹ : IsAntichain H.Adj sᶜ
this✝ : IsAntichain G.Adj (⇑f ⁻¹' sᶜ)
this : G.IsVertexCover (⇑f ⁻¹' s)
⊢ G.vertexCoverNum ≤ H.vertexCoverNum