mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
sintert : (s ∩ t).Nonempty
⊢ (⊤.induce (s ∪ t)).Connected

Tactic:
rw [preconnected_induce_iff] at sconn tconn

Goal state after:
V : Type u
G : SimpleGraph V
s t : Set V
sconn : (⊤.induce s).Preconnected
tconn : (⊤.induce t).Preconnected
sintert : (s ∩ t).Nonempty
⊢ (⊤.induce (s ∪ t)).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ (⊤.induce (s ∪ t)).Connected

Tactic:
rw [preconnected_induce_iff] at sconn tconn

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Preconnected
tconn : (⊤.induce t).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ (⊤.induce (s ∪ t)).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ (hasse (α × β)).Adj x y ↔ (hasse α □ hasse β).Adj x y

Tactic:
boxProd_adj,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ (hasse (α × β)).Adj x y ↔ (hasse α).Adj x.1 y.1 ∧ x.2 = y.2 ∨ (hasse β).Adj x.2 y.2 ∧ x.1 = y.1
Module: Mathlib.Combinatorics.SimpleGraph.Circulant

Goal state before:
pp: case zero
⊢ cycleGraph (0 + 1) = circulantGraph {1}

Tactic:
exact edgeFinset_inj.mp rfl

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

Goal state before:
pp: case cons.inr
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w✝ : V
head : G.Adj u' v'
tail : G.Walk v' w✝
ih : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges → tail.IsPath
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges
h' : tail.length > 0
⊢ u' ∉ tail.support

Tactic:
· by_contra hh
      apply hG <| cons head (tail.takeUntil u' hh)
      simp only [isCycle_def, isTrail_def, edges_cons, List.nodup_cons, ne_eq, reduceCtorEq,
        not_false_eq_true, support_cons, List.tail_cons, true_and]
      have : cons head (tail.takeUntil u' hh) |>.support.tail.Nodup :=
        tail.isPath_def.mp (ih hcc.2) |>.sublist <| List.IsInfix.sublist
          ⟨[], (tail.dropUntil u' hh).support.tail, by simp [← support_append]⟩
      refine ⟨⟨?_, edges_nodup_of_support_nodup this⟩, this⟩
      by_contra hhh
      refine hcc.1 s(u', v') ?_ rfl
      rw [← tail.cons_tail_eq (by simp [not_nil_iff_lt_length, h'])]
      have := IsPath.mk' this |>.eq_snd_of_mem_edges (Sym2.eq_swap ▸ hhh)
      simp [this, snd_takeUntil head.ne]

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

Goal state before:
pp: case refine_1
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ extremalNumber n₂ H₁ ≤ extremalNumber n₂ H₂

pp: case refine_2
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₂ ≃g H₁
⊢ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁

Tactic:
all_goals
    rw [← Fintype.card_fin n₂, extremalNumber_le_iff]
    intro G _ h
    apply card_edgeFinset_le_extremalNumber
    contrapose h
    exact h.trans' ⟨e.toCopy⟩

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

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : AddZeroClass α
inst✝¹ : One α
H : SimpleGraph V
inst✝ : DecidableRel H.Adj
h : IsCompl G H
⊢ adjMatrix α G + adjMatrix α Gᶜ = adjMatrix α (completeGraph V)

Tactic:
by aesop (add simp Matrix.compl)

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq V
⊢ (adjMatrix α (completeGraph V)).compl = 0

Tactic:
by aesop (add simp Matrix.compl)

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
x : V
h : G.Adj x default
h' : (f x).length ≤ 0
⊢ False

Tactic:
← hf' _ (.cons h .nil) (IsPath.nil.cons <| by simpa using h.ne),

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
x : V
h : G.Adj x default
h' : (cons h nil).length ≤ 0
⊢ False
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:
rw [← 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.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
⊢ ∃ u v, u ≠ v ∧ G.degree u = 1 ∧ G.degree v = 1

Tactic:
have ⟨u, v, p, hp, hmax⟩ := exists_isPath_forall_isPath_length_le_length G
  have ⟨u', v', hne⟩ := exists_pair_ne V
  have ⟨p', hp'⟩ := h.connected.exists_isPath u' v'
  have hnil : ¬p.Nil := by grind
  refine ⟨u, v, hp.nil_iff_eq.not.mp hnil, ?_, ?_⟩ <;>
    rw [degree_eq_one_iff_existsUnique_adj]
  · refine ⟨_, p.adj_snd hnil, fun w hadj ↦ ?_⟩
    apply h.isAcyclic.eq_snd_of_adj_start hp hadj
    have : ¬(p.cons hadj.symm).IsPath := by grind [length_cons]
    grind [hp.cons]
  · refine ⟨_, p.adj_penultimate hnil |>.symm, fun w hadj ↦ ?_⟩
    apply h.isAcyclic.eq_penultimate_of_adj_end hp hadj
    have : ¬(p.concat hadj).IsPath := by grind [length_concat]
    grind [hp.concat]

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
h : G.IsCompleteMultipartite
⊢ ∀ {a b : α},
    (completeMultipartiteGraph fun c ↦ { x // h.setoid c.out x }).Adj
        ({ toFun := fun x ↦ ⟨⟦x⟧, ⟨x, ⋯⟩⟩,
            invFun := fun x ↦
              match x with
              | ⟨fst, x⟩ => ↑x,
            left_inv := ⋯, right_inv := ⋯ }
          a)
        ({ toFun := fun x ↦ ⟨⟦x⟧, ⟨x, ⋯⟩⟩,
            invFun := fun x ↦
              match x with
              | ⟨fst, x⟩ => ↑x,
            left_inv := ⋯, right_inv := ⋯ }
          b) ↔
      G.Adj a b

Tactic:
by
    simp_rw [Equiv.coe_fn_mk, comap_adj, top_adj, ne_eq, Quotient.eq]
    intros
    change ¬¬ G.Adj _ _ ↔ _
    rw [not_not]

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v w : Fin r × Fin t
⊢ ↑v.1 ≠ ↑w.1 ↔ (completeEquipartiteGraph r t).Adj v w

Tactic:
← Fin.ext_iff.ne,

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v w : Fin r × Fin t
⊢ v.1 ≠ w.1 ↔ (completeEquipartiteGraph r t).Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ #K.verts = r * t

Tactic:
simp_rw [verts, card_disjiUnion, id_eq, sum_congr rfl fun _ ↦ K.card_mem_parts, sum_const,
    smul_eq_mul, mul_eq_mul_right_iff]

Goal state after:
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ #K.parts = r ∨ t = 0
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
⊢ Nonempty (G ≃g turanGraph (Fintype.card V) r)

Tactic:
by
  classical
  obtain ⟨zm, zp⟩ := h.isEquipartition.exists_partPreservingEquiv
  use (Equiv.subtypeUnivEquiv mem_univ).symm.trans zm
  intro a b
  simp_rw [turanGraph_adj, Equiv.trans_apply, Equiv.subtypeUnivEquiv_symm_apply]
  have := zp ⟨a, mem_univ a⟩ ⟨b, mem_univ b⟩
  rw [← h.not_adj_iff_part_eq] at this
  rw [← not_iff_not, not_ne_iff, this, card_parts]
  rcases le_or_gt r (card V) with c | c
  · rw [min_eq_right c]; rfl
  · have lc : ∀ x, zm ⟨x, _⟩ < card V := fun x ↦ (zm ⟨x, mem_univ x⟩).2
    rw [min_eq_left c.le, Nat.mod_eq_of_lt (lc a), Nat.mod_eq_of_lt (lc b),
      ← Nat.mod_eq_of_lt ((lc a).trans c), ← Nat.mod_eq_of_lt ((lc b).trans c)]; rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ (s ∩ c.supp).ncard = 1

Tactic:
Set.ncard_eq_one

Goal state after:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ ∃ a, s ∩ c.supp = {a}
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case inr
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : Nonempty α
⊢ ¬G.Connected

Tactic:
rw [connected_iff]

Goal state after:
case inr
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : Nonempty α
⊢ ¬(G.Preconnected ∧ Nonempty α)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
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✝³ x✝² : Finset V
hne : x✝³ ≠ x✝²
x✝¹ : V
h₁' : x✝¹ ∈ ↑x✝³
x✝ : V
h₂' : x✝ ∈ ↑x✝²
w✝¹ : Fin r
h₁ : map { toFun := fun j ↦ f (w✝¹, j), inj' := ⋯ } univ = x✝³
w✝ : Fin r
h₂ : map { toFun := fun j ↦ f (w✝, j), inj' := ⋯ } univ = x✝²
⊢ G.Adj x✝¹ x✝

Tactic:
← 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✝³ x✝² : Finset V
hne : x✝³ ≠ x✝²
x✝¹ x✝ : V
h₂' : x✝ ∈ ↑x✝²
w✝¹ : Fin r
h₁' : x✝¹ ∈ ↑(map { toFun := fun j ↦ f (w✝¹, j), inj' := ⋯ } univ)
h₁ : map { toFun := fun j ↦ f (w✝¹, j), inj' := ⋯ } univ = x✝³
w✝ : Fin r
h₂ : map { toFun := fun j ↦ f (w✝, j), inj' := ⋯ } univ = x✝²
⊢ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_2.refine_4
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
⊢ (↑(cons s K.parts ⋯)).Pairwise fun x1 x2 ↦ G.IsCompleteBetween ↑x1 ↑x2

Tactic:
rw [coe_cons]

Goal state after:
case neg.refine_2.refine_4
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
⊢ (insert s ↑K.parts).Pairwise fun x1 x2 ↦ G.IsCompleteBetween ↑x1 ↑x2
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
x : V
xnL : x ∉ L
⊢ ∃ x_1 ∈ ↑(G.componentComplMk xnL), x_1 ∈ ↑(hom h (G.componentComplMk xnL))

Tactic:
exact ⟨x, ⟨xnL, rfl⟩, ⟨fun xK => xnL (h xK), rfl⟩⟩

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

Goal state before:
pp: case inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
hr : r > 0
H : SimpleGraph V
w✝ : DecidableRel H.Adj
maxH : H.IsTuranMaximal r
⊢ let n := Fintype.card V;
  #G.edgeFinset ≤ (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2

Tactic:
convert! maxH.2 cf

Goal state after:
case e'_4
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
hr : r > 0
H : SimpleGraph V
w✝ : DecidableRel H.Adj
maxH : H.IsTuranMaximal r
⊢ (Fintype.card V ^ 2 - (Fintype.card V % r) ^ 2) * (r - 1) / (2 * r) + (Fintype.card V % r).choose 2 = #H.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
m : ℕ
hm : m ∈ Set.Ici 2
hx : ↑(extremalNumber m H) / ↑(m.choose 2) = x
n : ℕ
hn : m ≤ n
G : SimpleGraph (Fin n)
w✝ : DecidableRel G.Adj
hcard_edges : ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(n.choose 2)
h_free : H.Free G
⊢ H.turanDensity + ε ≤ ↑(extremalNumber n H) / ↑(n.choose 2)

Tactic:
le_div_iff₀ <| mod_cast Nat.choose_pos (hm.trans hn)

Goal state after:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
m : ℕ
hm : m ∈ Set.Ici 2
hx : ↑(extremalNumber m H) / ↑(m.choose 2) = x
n : ℕ
hn : m ≤ n
G : SimpleGraph (Fin n)
w✝ : DecidableRel G.Adj
hcard_edges : ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(n.choose 2)
h_free : H.Free G
⊢ (H.turanDensity + ε) * ↑(n.choose 2) ≤ ↑(extremalNumber n H)
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
hG : G.IsHamiltonian
a b : α
⊢ G.Reachable a b

Tactic:
by
    obtain rfl | hab := eq_or_ne a b
    · rfl
    have : Nontrivial α := ⟨a, b, hab⟩
    obtain ⟨_, p, hp⟩ := hG Fintype.one_lt_card.ne'
    have a_mem := hp.mem_support a
    have b_mem := hp.mem_support b
    exact ((p.takeUntil a a_mem).reverse.append <| p.takeUntil b b_mem).reachable

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

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype (Sym2 α)
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Semiring R
inst✝ : G.LocallyFinite
⊢ incMatrix R G * (incMatrix R G)ᵀ = of fun a b ↦ if a = b then ↑(G.degree a) else if G.Adj a b then 1 else 0

Tactic:
by
  ext a b
  dsimp
  split_ifs with h h'
  · subst b
    exact incMatrix_mul_transpose_diag (R := R) G
  · exact G.incMatrix_mul_transpose_apply_of_adj h'
  · simp only [Matrix.mul_apply, Matrix.transpose_apply,
      G.incMatrix_apply_mul_incMatrix_apply_of_not_adj h h', sum_const_zero]

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
A : Matrix V V α
h : A.IsAdjMatrix
i j : V
⊢ Aᴴ i j = A i j

Tactic:
rcases h.zero_or_one i j with heq | heq

Goal state after:
case inl
α : Type u_1
V : Type u_2
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
A : Matrix V V α
h : A.IsAdjMatrix
i j : V
heq : A i j = 0
⊢ Aᴴ i j = A i j

case inr
α : Type u_1
V : Type u_2
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
A : Matrix V V α
h : A.IsAdjMatrix
i j : V
heq : A i j = 1
⊢ Aᴴ i j = A i j
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case inl
ε : ℝ
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_eq_1 : r = 1
h0 : r ≤ 1 ∨ t' = 0
⊢ r * t' ≤ Fintype.card (Fin n)

Tactic:
hr_eq_1,

Goal state after:
case inl
ε : ℝ
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_eq_1 : r = 1
h0 : r ≤ 1 ∨ t' = 0
⊢ 1 * t' ≤ Fintype.card (Fin n)
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case neg
α : 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)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
hk : ¬k = 0
w3 : 3 ≤ #W
hap : #W - 1 + 2 * (k - 1) = #W - 3 + 2 * k
⊢ (#W - 3 + 2 * k) * ‖α‖ ≤ (2 * r + k) * ‖α‖

Tactic:
two_mul,

Goal state after:
case neg
α : 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)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
hk : ¬k = 0
w3 : 3 ≤ #W
hap : #W - 1 + 2 * (k - 1) = #W - 3 + 2 * k
⊢ (#W - 3 + (k + k)) * ‖α‖ ≤ (2 * r + k) * ‖α‖
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
a✝ : Nontrivial V
x : V
⊢ G.vertexCoverNum ≤ ENat.card V - 1

Tactic:
refine ENat.forall_natCast_le_iff_le.mp fun n hn ↦ ?_

Goal state after:
V : Type u_1
G : SimpleGraph V
a✝ : Nontrivial V
x : V
n : ℕ
hn : ↑n ≤ G.vertexCoverNum
⊢ ↑n ≤ ENat.card V - 1
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
h' : ¬G.edgeSet = ∅
⊢ G.vertexCoverNum ≤ G.edgeSet.encard

Tactic:
refine ENat.forall_natCast_le_iff_le.mp fun n hn ↦ ?_

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
h' : ¬G.edgeSet = ∅
n : ℕ
hn : ↑n ≤ G.vertexCoverNum
⊢ ↑n ≤ G.edgeSet.encard
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: case refine_1
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₁ : PlacedTile ps
⊢ ⟦Quotient.out pt₁.groupElts⟧ = pt₁.groupElts

Tactic:
rw [Quotient.out_eq]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
G' : SimpleGraph V
hG' : G'.IsAlternating M2.spanningCoe
hG'cyc : G'.IsCycles
hG'xb : ¬G'.Adj x b
hnG'ac : G'.Adj a c
hle : G' ≤ G ⊔ edge a c
⊢ ∃ M, M.IsPerfectMatching

Tactic:
have : M2.spanningCoe ∆ G' ≤ G := by
      apply Disjoint.left_le_of_le_sup_right (symmDiff_le (le_sup_of_le_right M2.spanningCoe_le)
        (le_sup_of_le_right hle))
      simp [disjoint_edge, symmDiff_def, hM2ac, hnG'ac]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
G' : SimpleGraph V
hG' : G'.IsAlternating M2.spanningCoe
hG'cyc : G'.IsCycles
hG'xb : ¬G'.Adj x b
hnG'ac : G'.Adj a c
hle : G' ≤ G ⊔ edge a c
this : M2.spanningCoe ∆ G' ≤ G
⊢ ∃ M, M.IsPerfectMatching
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
⊢ μ.colLen j2 ≤ μ.colLen j1

Tactic:
by
  convert! μ.transpose.rowLen_anti j1 j2 hj using 1 <;> simp

Goal state after:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
index : ιₚ
groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries
⊢ ((Quotient.mk'' (Quotient.out groupElts)).liftOn' (fun g ↦ g • ↑(↑ps index)) ⋯).Nonempty ↔ (↑(↑ps index)).Nonempty

Tactic:
Quotient.liftOn'_mk''

Goal state after:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
index : ιₚ
groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries
⊢ (Quotient.out groupElts • ↑(↑ps index)).Nonempty ↔ (↑(↑ps index)).Nonempty
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
index : ιₚ
groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries
⊢ ((Quotient.mk'' (Quotient.out groupElts)).liftOn' (fun g ↦ g • ↑(↑ps index)) ⋯).Finite ↔ (↑(↑ps index)).Finite

Tactic:
Quotient.liftOn'_mk''

Goal state after:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
index : ιₚ
groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries
⊢ (Quotient.out groupElts • ↑(↑ps index)).Finite ↔ (↑(↑ps index)).Finite
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case mp
m n : ℕ
h : (n + 1).ppred = some m
⊢ m.succ = n + 1

Tactic:
injection h

Goal state after:
case mp
m n : ℕ
val_eq✝ : n = m
⊢ m.succ = n + 1
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case mpr
m n : ℕ
h : m.succ = n + 1
⊢ (n + 1).ppred = some m

Tactic:
injection h

Goal state after:
case mpr
m n : ℕ
n_eq✝ : m = n
⊢ (n + 1).ppred = some m