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

Goal state before:
pp: n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
A : Finset (Fin n)
hA : A ∈ {a ∈ 𝒜 | compress U V a ∉ 𝒜}
⊢ toColex (image Fin.val (compress U V A)) < toColex (image Fin.val A)

Tactic:
toColex_image_lt_toColex_image Fin.val_strictMono

Goal state after:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
A : Finset (Fin n)
hA : A ∈ {a ∈ 𝒜 | compress U V a ∉ 𝒜}
⊢ toColex (compress U V A) < toColex A
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
⊢ ∃ ℬ, #(∂ ℬ) ≤ #(∂ 𝒜) ∧ #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ

Tactic:
set usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t | UsefulCompression t.1 t.2 ∧ ¬ IsCompressed t.1 t.2 𝒜}

Goal state after:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) := {t | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
⊢ ∃ ℬ, #(∂ ℬ) ≤ #(∂ 𝒜) ∧ #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
c : Set (Set α)
hc : IsPartition c
x : α
t : Set α
ht : (fun b ↦ b ∈ c ∧ x ∈ b) t ∧ ∀ (y : Set α), (fun b ↦ b ∈ c ∧ x ∈ b) y → y = t
⊢ t ∈ c ∧ x ∈ t

Tactic:
simp only at ht
        tauto

Goal state after:
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 (image Fin.val B) < toColex (image Fin.val A)

Tactic:
toColex_image_lt_toColex_image Fin.val_strictMono

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.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
⊢ G.chromaticNumber ≤ G'.chromaticNumber

Tactic:
rw [chromaticNumber, chromaticNumber]
  simp only [Set.mem_ofPred_eq, le_iInf_iff]
  intro m hc
  have := h _ hc
  rw [← chromaticNumber_le_iff_colorable] at this
  exact this

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

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

Tactic:
simp only [isBridge_iff, not_not] at h

Goal state after:
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
⊢ (G.deleteEdges {s(x, y)}).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
⊢ G = ⊤

Tactic:
by_contra! hh

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
inst✝ : Fintype ↑(G.neighborSet u)
h : G.IsEdgeReachable k u v
huv : u ≠ v
⊢ k ≤ G.degree u

Tactic:
by_contra! hh

Goal state after:
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
inst✝ : Fintype ↑(G.neighborSet u)
h : G.IsEdgeReachable k u v
huv : u ≠ v
hh : G.degree u < k
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
⊢ G'.edist u v ≤ G.edist u v

Tactic:
obtain ⟨_, hw⟩ := hr.exists_walk_length_eq_edist
    rw [← hw, ← Walk.length_map (.ofLE h)]
    apply edist_le

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

Tactic:
have : p.bypass = p := by
    apply bypass_eq_self_of_length_le_length_bypass
    calc p.length
      _ = G.dist u v := hp
      _ ≤ p.bypass.length := dist_le p.bypass
  rw [← this]
  apply Walk.bypass_isPath

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Connected
hH : H.Connected
this : Nonempty α
⊢ (G □ H).Connected

Tactic:
have := hH.nonempty

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Connected
hH : H.Connected
this✝ : Nonempty α
this : Nonempty β
⊢ (G □ H).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
inst✝³ : DecidableEq V
inst✝² : DecidableEq W
inst✝¹ : G.LocallyFinite
inst✝ : H.LocallyFinite
v : V
⊢ Fintype ↑(Sum.inl '' G.neighborSet v)

Tactic:
infer_instance

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

Goal state before:
pp: case inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w✝ w' : W
inst✝³ : DecidableEq V
inst✝² : DecidableEq W
inst✝¹ : G.LocallyFinite
inst✝ : H.LocallyFinite
w : W
⊢ Fintype ↑(Sum.inr '' H.neighborSet w)

Tactic:
infer_instance

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

Goal state before:
pp: n✝ : ℕ
⊢ DecidableRel
    (match n✝ + 2 with
      | 0 => ⊥
      | 1 => ⊥
      | n.succ.succ => { Adj := fun a b ↦ a - b = 1 ∨ b - a = 1, symm := ⋯, loopless := ⋯ }).Adj

Tactic:
infer_instance

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : ∀ ⦃e : Sym2 V⦄, e ∈ G.edgeSet → G.IsBridge e
v : V
c : G.Walk v v
hc : c.IsCycle
e : Sym2 V
he : e ∈ c.edges
⊢ False

Tactic:
exact (hG <| c.edges_subset_edgeSet he).notMem_edges_of_isCycle hc he

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
p : SimpleGraph V → Prop
⊢ (∃ G x, G.IsExtremal p) ↔ ∃ G, p G

Tactic:
refine ⟨fun ⟨_, _, h⟩ ↦ ⟨_, h.1⟩, fun ⟨G, hp⟩ ↦ ?_⟩

Goal state after:
V : Type u_1
inst✝ : Fintype V
p : SimpleGraph V → Prop
x✝ : ∃ G, p G
G : SimpleGraph V
hp : p G
⊢ ∃ G x, G.IsExtremal p
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
h : A.IsAdjMatrix
⊢ DecidableRel fun i j ↦ A i j = 1

Tactic:
infer_instance

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : Minimal Connected G
⊢ G.IsTree

Tactic:
rw [isTree_iff, and_iff_right h.prop, isAcyclic_iff_forall_adj_isBridge]

Goal state after:
V : Type u_1
G : SimpleGraph V
h : Minimal Connected G
⊢ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case pos
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬↑u = n + 2 - 1
h✝ : ↑v = n + 2 - 1
⊢ ⟨↑u % 2, ⋯⟩ ≠ 2

pp: case neg
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
⊢ ⟨↑u % 2, ⋯⟩ ≠ ⟨↑v % 2, ⋯⟩

Tactic:
· refine (Fin.ne_of_lt (Fin.mk_lt_of_lt_val ?_))
        exact u.val.mod_lt Nat.zero_lt_two

Goal state after:
case neg
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
⊢ ⟨↑u % 2, ⋯⟩ ≠ ⟨↑v % 2, ⋯⟩
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case a
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
hn3 : n - 3 + 3 = n
w : (cycleGraph (n - 3 + 3)).Walk 0 0 := cycleGraph.cycle (n - 3)
hOdd' : Odd w.length
⊢ 3 ≤ (cycleGraph n).chromaticNumber

Tactic:
← hn3

Goal state after:
case a
n : ℕ
h : 2 ≤ n
hOdd : Odd n
hc : (cycleGraph n).Colorable (Fintype.card (Fin 3))
hn3 : n - 3 + 3 = n
w : (cycleGraph (n - 3 + 3)).Walk 0 0 := cycleGraph.cycle (n - 3)
hOdd' : Odd w.length
⊢ 3 ≤ (cycleGraph (n - 3 + 3)).chromaticNumber
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
G' : SimpleGraph V'
K : Type u_3
K' : Type u_4
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ ∀ (x y : V), ⊤.Adj x y → (if G.Adj y x then 1 else 0) = if G.Adj x y then 1 else 0

Tactic:
by simp [G.adj_comm]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
⊢ Odd {c | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp}.ncard ↔ Odd c'.supp.ncard

Tactic:
simp_rw [← Nat.card_coe_set_eq]
  classical
  cases nonempty_fintype V
  rw [Nat.card_eq_card_toFinset c'.supp, ← disjiUnion_supp_toFinset_eq_supp_toFinset h]
  simp only [Finset.card_disjiUnion, Set.toFinset_card, Fintype.card_ofFinset]
  rw [Finset.odd_sum_iff_odd_card_odd, Nat.card_eq_fintype_card, Fintype.card_ofFinset]
  congr! 2
  ext c
  simp_rw [Set.toFinset_ofPred, mem_filter, ← Set.ncard_coe_finset, coe_filter,
    mem_supp_iff, mem_univ, true_and, supp, and_comm]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
J : SimpleGraph V
w✝ : DecidableRel J.Adj
j : J.IsTuranMaximal r
g : J ≃g turanGraph (Fintype.card V) r
⊢ G.IsTuranMaximal r

Tactic:
f.card_eq,

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
J : SimpleGraph V
w✝ : DecidableRel J.Adj
j : J.IsTuranMaximal r
g : J ≃g turanGraph (Fintype.card (Fin n)) r
⊢ G.IsTuranMaximal r
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
x : V
hx : x ∈ s
h : G.connectedComponentMk x ∈ C
⊢ (fun x_1 ↦ x_1 ∈ s ∩ (G.connectedComponentMk x).supp) x ∧
    ∀ (y : V), (fun x_1 ↦ x_1 ∈ s ∩ (G.connectedComponentMk x).supp) y → y = x

Tactic:
simp only [Set.mem_inter_iff, hx, mem_supp_iff, and_self, and_imp, true_and]

Goal state after:
case h
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
x : V
hx : x ∈ s
h : G.connectedComponentMk x ∈ C
⊢ ∀ y ∈ s, G.connectedComponentMk y = G.connectedComponentMk x → y = x
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.diam ≠ 0
⊢ Nontrivial α

Tactic:
contrapose! h
  simp [diam, h]

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

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : Set.univ ⊆ G.center
⊢ ∃ e, ∀ (u : α), G.eccent u = e

pp: case refine_2
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ∃ e, ∀ (u : α), G.eccent u = e
⊢ Set.univ ⊆ G.center

Tactic:
· use G.radius
    exact fun _ ↦ h trivial

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ∃ e, ∀ (u : α), G.eccent u = e
⊢ Set.univ ⊆ G.center
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_4
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
p✝ : Finset V
h : p✝ ∈ map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ
⊢ #p✝ = t

pp: case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ : Finset V
h₁ : x✝³ ∈ ↑(map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ)
x✝² : Finset V
h₂ : x✝² ∈ ↑(map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ)
hne : x✝³ ≠ x✝²
x✝¹ : V
h₁' : x✝¹ ∈ ↑x✝³
x✝ : V
h₂' : x✝ ∈ ↑x✝²
⊢ G.Adj x✝¹ x✝

Tactic:
· simp_rw [mem_map, mem_univ, Embedding.coeFn_mk, true_and] at h
      replace ⟨_, h⟩ := h
      simp [← h]

Goal state after:
case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ : Finset V
h₁ : x✝³ ∈ ↑(map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ)
x✝² : Finset V
h₂ : x✝² ∈ ↑(map { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } univ)
hne : x✝³ ≠ x✝²
x✝¹ : V
h₁' : x✝¹ ∈ ↑x✝³
x✝ : V
h₂' : x✝ ∈ ↑x✝²
⊢ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n✝ r : ℕ
hr : r > 0
n : ℕ
⊢ (2 * (n % r * (n / r) * (r - 1)) + r * (r - 1) * (n / r) ^ 2) * r / (2 * r) =
    n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2

Tactic:
rw [Nat.mul_div_mul_right _ _ hr, Nat.mul_add_div zero_lt_two]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk vnK
dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2
u : V
⊢ u ∈ ↑C

Tactic:
by_contra unC

Goal state after:
V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk vnK
dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2
u : V
unC : u ∉ ↑C
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case h₁.inr
n r : ℕ
hr : r > 0
⊢ n % r * r - r ≤ r * (n % r) - n % r

Tactic:
mul_comm

Goal state after:
case h₁.inr
n r : ℕ
hr : r > 0
⊢ r * (n % r) - r ≤ r * (n % r) - n % r
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: case hn
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
e : Sym2 (Fin (n + 1))
he : e ∈ G.edgeFinset
⊢ n - 1 ≤ ↑(#(bipartiteBelow (fun v e ↦ v ∉ e) univ e))

Tactic:
simp_rw [← Sym2.mem_toFinset, bipartiteBelow, filter_not, filter_mem_eq_inter, univ_inter,
      ← compl_eq_univ_sdiff, card_compl, Fintype.card_fin, card_toFinset_mem_edgeFinset ⟨e, he⟩,
      Nat.cast_id, Nat.reduceSubDiff, le_refl]

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Fintype ι
s : ι → Set α
⊢ (⋃ i, s i).encard ≤ ∑ i, (s i).encard

Tactic:
simpa using Finset.univ.set_encard_biUnion_le s

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

Goal state before:
pp: case h.inl
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd✝ : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun w ↦ N.Adj v w) w ∧ ∀ (y : V), (fun w ↦ N.Adj v w) y → y = w
y : V
h : N.Adj v y
⊢ y = w

Tactic:
exact hw.2 y h

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

Goal state before:
pp: case h.inr
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd✝ : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : ∀ ⦃a : V⦄, a ∈ N.support → a ∉ N'.support
hmN : v ∈ N.verts
w : V
hw : (fun w ↦ N.Adj v w) w ∧ ∀ (y : V), (fun w ↦ N.Adj v w) y → y = w
y : V
h : N'.Adj v y
⊢ y = w

Tactic:
simpa [(mem_support _).mpr ⟨w, hw.1⟩, (mem_support _).mpr ⟨y, h⟩] using @hd v

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Subsingleton α
v : α
⊢ List.count v p.support = 1

Tactic:
rw [nil_iff_support_eq.mp p.nil_of_subsingleton, Subsingleton.elim v a, List.count_singleton_self]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
hp : p.IsHamiltonian
this : Fintype α
⊢ Finite α

Tactic:
infer_instance

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

Goal state before:
pp: case convert_3
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : MulZeroOneClass R
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
a : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ NeZero 1

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
x✝ : α
hx : x✝ ∈ X
h : #({z ∈ W | ¬G.Adj x✝ z}) < 3
⊢ False

Tactic:
obtain ⟨_, _, hW⟩ := hw.exists_isFiveWheelLike_succ_of_not_adj_le_two hcf
      (by simpa [X] using hx) <| Nat.le_of_succ_le_succ h

Goal state after:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
x✝ : α
hx : x✝ ∈ X
h : #({z ∈ W | ¬G.Adj x✝ z}) < 3
w✝¹ w✝ : α
hW : G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x✝ (s.erase w✝¹)) (insert x✝ (t.erase w✝))
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.inr
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
h : ¬G'.Adj v w
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
w' : V
hw' : y ≠ w' ∧ G'.Adj v w'
⊢ y = w

Tactic:
simp_all [show M.Adj v y ↔ ¬M.Adj v w' by simpa using hG' hw'.1 hr.1 hw'.2]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case refine_3
ε : ℝ
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' : ℕ
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'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
y : (a : Finset (Fin n)) → a ∈ K.parts → Finset (Fin n)
hy✝ : y ∈ K.parts.pi fun x ↦ powersetCard t x
hy : ∀ (a : Finset (Fin n)) (h : a ∈ K.parts), y a h ∈ powersetCard t a
ht_le_card_filter : t ≤ #{w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
s : Finset ↥(ErdosStone.filter K t)
hs_subset : s ⊆ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
hcards : #s = t
p : Finset (Fin n)
hp : p ∈ Finset.map { toFun := fun p ↦ y ↑p ⋯, inj' := ⋯ } univ
⊢ #p = t

Tactic:
simp_rw [univ_eq_attach, Finset.mem_map, mem_attach,
          Function.Embedding.coeFn_mk, true_and, Subtype.exists] at hp
        replace ⟨p, hp, hyp⟩ := hp
        rw [← hyp]
        have hy' := mem_powersetCard.mp (hy p hp)
        exact hy'.right

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : Set V
hi : G.IsIndepSet cᶜ
v w : V
hadj : G.Adj v w
⊢ v ∈ c ∨ w ∈ c

Tactic:
by_contra! hh

Goal state after:
V : Type u_1
G : SimpleGraph V
c : Set V
hi : G.IsIndepSet cᶜ
v w : V
hadj : G.Adj v w
hh : v ∉ c ∧ w ∉ c
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
n : ℕ
h₁ : G.vertexCoverNum ≤ ↑n
h₂ : ↑n ≤ ENat.card V
⊢ ∃ s, s.encard = ↑n ∧ G.IsVertexCover s

Tactic:
by
  obtain ⟨s, hs₁, hs₂⟩ := vertexCoverNum_exists G
  obtain ⟨r, hr₁, _, hr₃⟩ :=
    Set.exists_superset_subset_encard_eq (by simp) (le_of_eq_of_le hs₁ h₁) (Set.encard_univ _ ▸ h₂)
  exact ⟨r, hr₃, hs₂.subset hr₁⟩

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

Goal state before:
pp: case refine_2
V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
⊢ ↑n ≤ (completeGraph V).vertexCoverNum

Tactic:
by_contra! hh

Goal state after:
case refine_2
V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < ↑n
⊢ False
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
⊢ G.vertexCoverNum ≤ H.vertexCoverNum

Tactic:
have := H.isIndepSet_iff_isAntichain_adj.mp <| isIndepSet_compl_iff_isVertexCover.mpr hs₂

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ᶜ
⊢ G.vertexCoverNum ≤ H.vertexCoverNum
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
i : ℕ
c : ℕ × ℕ
⊢ c ∈ μ.row i ↔ c ∈ μ ∧ c.1 = i

Tactic:
by
  simp [row]

Goal state after:
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case mp
n : ℕ
⊢ (n + 1).ppred = none → n + 1 = 0

Tactic:
intro

Goal state after:
case mp
n : ℕ
a✝ : (n + 1).ppred = none
⊢ n + 1 = 0
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case mpr
n : ℕ
⊢ n + 1 = 0 → (n + 1).ppred = none

Tactic:
intro

Goal state after:
case mpr
n : ℕ
a✝ : n + 1 = 0
⊢ (n + 1).ppred = none
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: m n k : ℕ
⊢ m.psub (n + 1) = some k ↔ k + (n + 1) = m

Tactic:
apply Option.bind_eq_some_iff.trans

Goal state after:
m n k : ℕ
⊢ (∃ a, m.psub n = some a ∧ a.ppred = some k) ↔ k + (n + 1) = m
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Primrec c
hf : Primrec f
hg : Primrec g
a : α
⊢ (Nat.casesOn (encode (c a)) (g a) fun b ↦ f (a, b).1) = bif c a then f a else g a

Tactic:
by cases c a <;> rfl

Goal state after: