mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: ι : Type u_4
V : ι → Type u_5
inst✝ : Fintype ι
f : (i : ι) → V i
⊢ (completeMultipartiteGraph V).chromaticNumber = ↑(card ι)

Tactic:
apply le_antisymm (colorable V).chromaticNumber_le

Goal state after:
ι : Type u_4
V : ι → Type u_5
inst✝ : Fintype ι
f : (i : ι) → V i
⊢ ↑(card ι) ≤ (completeMultipartiteGraph V).chromaticNumber
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : α → β
inst✝ : Fintype α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
⊢ (∑ a, f₁ a) * ∑ a, f₂ a ≤ (∑ a, f₃ a) * ∑ a, f₄ a

Tactic:
classical simpa using four_functions_theorem f₁ f₂ f₃ f₄ h₁ h₂ h₃ h₄ h univ univ

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

Goal state before:
pp: 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
f : G ↪g G'
g : H ↪g H'
u v : V ⊕ W
⊢ Sum.map (⇑f) (⇑g) u = Sum.map (⇑f) (⇑g) v → u = v

Tactic:
by cases u <;> cases v <;> simp

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

Goal state before:
pp: 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
f : G ↪g G'
g : H ↪g H'
u v : V ⊕ W
⊢ (G' ⊕g H').Adj ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } u) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } v) ↔ (G ⊕g H).Adj u v

Tactic:
by cases u <;> cases v <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ (hasse α).CliqueFree 3

Tactic:
intro s ⟨hc, hcard⟩

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Finset α
hc : (hasse α).IsClique ↑s
hcard : s.card = 3
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_1
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
⊢ ({G | H.Free G}.sup fun x ↦ #x.edgeFinset) ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

pp: case refine_2
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
⊢ ({G | H.Free G}.sup fun x ↦ #x.edgeFinset) ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
on_goal 1 =>
    replace e := e.symm

Goal state after:
case refine_1
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
⊢ ({G | H.Free G}.sup fun x ↦ #x.edgeFinset) ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

case refine_2
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
⊢ ({G | H.Free G}.sup fun x ↦ #x.edgeFinset) ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
x : V
⊢ adjMatrix α G x v = adjMatrix α G v x

Tactic:
← transpose_apply (adjMatrix α G) x v,

Goal state after:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
x : V
⊢ adjMatrix α G x v = (adjMatrix α G)ᵀ x v
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this : Nonempty V
inhabited_h : Inhabited V
⊢ G.edgeFinset.card + 1 = Fintype.card V

Tactic:
have : Finset.card ({default} : Finset V)ᶜ + 1 = Fintype.card V := by
    rw [Finset.card_compl, Finset.card_singleton, Nat.sub_add_cancel Fintype.card_pos]
  rw [← this, add_left_inj]
  choose f hf hf' using (hG.existsUnique_path · default)
  refine Eq.symm <| Finset.card_bij
          (fun w hw => ((f w).firstDart <| ?notNil).edge)
          (fun a ha => ?memEdges) ?inj ?surj
  case notNil => exact not_nil_of_ne (by simpa using hw)
  case memEdges => simp
  case inj =>
    intro a ha b hb h
    wlog h' : (f a).length ≤ (f b).length generalizing a b
    · exact Eq.symm (this _ hb _ ha h.symm (le_of_not_ge h'))
    rw [dart_edge_eq_iff] at h
    obtain (h | h) := h
    · exact (congrArg (·.fst) h)
    · have h1 : ((f a).firstDart <| not_nil_of_ne (by simpa using ha)).snd = b :=
        congrArg (·.snd) h
      have h3 := congrArg length (hf' _ ((f _).tail.copy h1 rfl) ?_)
      · rw [length_copy, ← add_left_inj 1,
          length_tail_add_one (not_nil_of_ne (by simpa using ha))] at h3
        lia
      · simp only [isPath_copy]
        exact (hf _).tail
  case surj =>
    simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
    intro x y h
    wlog h' : (f x).length ≤ (f y).length generalizing x y
    · rw [Sym2.eq_swap]
      exact this y x h.symm (le_of_not_ge h')
    refine ⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩
    · rintro rfl
      rw [← hf' _ nil IsPath.nil, length_nil,
          ← hf' _ (.cons h .nil) (IsPath.nil.cons <| by simpa using h.ne),
          length_cons, length_nil] at h'
      simp at h'
    rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
    · simp
    case contra =>
      suffices (f x).takeUntil y hy = .cons h .nil by
        rw [← take_spec _ hy] at h'
        simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
      refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
      simp [h.ne]

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

Goal state before:
pp: case neg.inl
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : u - v = 1
⊢ ¬False

Tactic:
exact id

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

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : 2 ≤ G.minDegree
this✝ : G.edgeFinset.card + 1 = Fintype.card V
this : ∑ v, G.degree v = 2 * G.edgeFinset.card
hle : Fintype.card V • 2 ≤ ∑ v, G.degree v
⊢ G.minDegree = 1

Tactic:
smul_eq_mul

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : 2 ≤ G.minDegree
this✝ : G.edgeFinset.card + 1 = Fintype.card V
this : ∑ v, G.degree v = 2 * G.edgeFinset.card
hle : Fintype.card V * 2 ≤ ∑ v, G.degree v
⊢ G.minDegree = 1
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case neg.inr
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : v - u = 1
⊢ ¬False

Tactic:
exact id

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

Goal state before:
pp: case inl
r t : ℕ
ht_eq0 : t = 0
⊢ (completeEquipartiteGraph r t).IsCompleteMultipartite

pp: case inr
r t : ℕ
ht_pos : t > 0
⊢ (completeEquipartiteGraph r t).IsCompleteMultipartite

Tactic:
· rw [completeEquipartiteGraph_eq_bot_iff.mpr (Or.inr ht_eq0)]
    exact bot_isCompleteMultipartite

Goal state after:
case inr
r t : ℕ
ht_pos : t > 0
⊢ (completeEquipartiteGraph r t).IsCompleteMultipartite
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case h₁
α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
c₁ c₂ : Fin n
v₁ : ↑(C.colorClass c₁)
v₂ : ↑(C.colorClass c₂)
hc : c₁ = c₂
hv : (F c₁) v₁ = (F c₂) v₂
v₁' : ↑(C.colorClass c₂) := ⋯
⊢ ⇑(F c₁) ≍ ⇑(F c₂)

Tactic:
hc

Goal state after:
case h₁
α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
c₁ c₂ : Fin n
v₁ : ↑(C.colorClass c₁)
v₂ : ↑(C.colorClass c₂)
hc : c₁ = c₂
hv : (F c₁) v₁ = (F c₂) v₂
v₁' : ↑(C.colorClass c₂) := ⟨↑v₁, ⋯⟩
⊢ ⇑(F c₂) ≍ ⇑(F c₂)
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
a : V
ha : a ∈ s
⊢ a ∉ c.supp

Tactic:
hc

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 : V
ha : a ∈ s
hc : a ∈ c.supp
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
v : Fin (n + r)
| ∑ i ∈ range (n + r), if ↑v % r ≠ i % r then 1 else 0

Tactic:
sum_range_add

Goal state after:
n r : ℕ
v : Fin (n + r)
| (∑ x ∈ range n, if ↑v % r ≠ x % r then 1 else 0) + ∑ x ∈ range r, if ↑v % r ≠ (n + x) % r then 1 else 0
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case mp
α : Type u_1
G : SimpleGraph α
u : α
⊢ G.eccent u ≤ 1 → ∀ (v : α), u ≠ v → G.Adj u v

pp: case mpr
α : Type u_1
G : SimpleGraph α
u : α
⊢ (∀ (v : α), u ≠ v → G.Adj u v) → G.eccent u ≤ 1

Tactic:
· intro h v huv
    have hd : G.edist u v ≤ 1 := edist_le_eccent.trans h
    have hd' : 1 ≤ G.edist u v := Order.one_le_iff_pos.mpr (G.edist_pos_of_ne huv)
    exact edist_eq_one_iff_adj.mp (le_antisymm (hd') hd).symm

Goal state after:
case mpr
α : Type u_1
G : SimpleGraph α
u : α
⊢ (∀ (v : α), u ≠ v → G.Adj u v) → G.eccent u ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ∀ (v : α), ∃ w, ¬G.Reachable v w
w✝ : α
hw : ¬G.Reachable Classical.ofNonempty w✝
⊢ ⊤ ≤ G.ediam

Tactic:
← edist_eq_top_of_not_reachable hw

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
h : ∀ (v : α), ∃ w, ¬G.Reachable v w
w✝ : α
hw : ¬G.Reachable Classical.ofNonempty w✝
⊢ G.edist Classical.ofNonempty w✝ ≤ G.ediam
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties

Goal state before:
pp: V : Type
G : SimpleGraph V
inst✝ : Finite V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
property✝ : s ∈ G.end
val✝ : Fintype V
v : V
h : v ∈ ↑(s (Opposite.op Finset.univ))
⊢ v ∈ ↑(Opposite.unop (Opposite.op Finset.univ))

Tactic:
simp only [Finset.coe_univ, Set.mem_univ]

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

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
this : ∀ (r' : ℕ), IsEmpty (Fin r' × Fin t)
h_bot : ∀ (r' : ℕ), completeEquipartiteGraph r' t = ⊥
⊢ ⊥ ⊑ G ↔ ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s

Tactic:
ht,

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
this : ∀ (r' : ℕ), IsEmpty (Fin r' × Fin t)
h_bot : ∀ (r' : ℕ), completeEquipartiteGraph r' t = ⊥
⊢ ⊥ ⊑ G ↔ ∃ K s, #s = 0 ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
⊢ n ^ 2 * (r - 1) + 2 * r * (n % r).choose 2 - (n % r) ^ 2 * (r - 1) ≤ (r - 1) * n ^ 2

Tactic:
Nat.sub_le_iff_le_add,

Goal state after:
n r : ℕ
⊢ n ^ 2 * (r - 1) + 2 * r * (n % r).choose 2 ≤ (r - 1) * n ^ 2 + (n % r) ^ 2 * (r - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
w✝ : ℕ
left✝ : w✝ ∈ Set.Ici 2
hx : ↑(extremalNumber w✝ H) / ↑(w✝.choose 2) = x
⊢ 0 ≤ x

Tactic:
← hx

Goal state after:
W : Type u_1
H : SimpleGraph W
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
w✝ : ℕ
left✝ : w✝ ∈ Set.Ici 2
hx : ↑(extremalNumber w✝ H) / ↑(w✝.choose 2) = x
⊢ 0 ≤ ↑(extremalNumber w✝ H) / ↑(w✝.choose 2)
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'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
| #({v_1 ∈ K.verts | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v}) < #K.verts - t' + t

Tactic:
enter [1, 1, 2]
    unfold CompleteEquipartiteSubgraph.verts

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
| K.parts.disjiUnion id ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: case refine_2
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
⊢ H.turanDensity + ε ≤ x

Tactic:
← hx

Goal state after:
case refine_2
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
⊢ H.turanDensity + ε ≤ ↑(extremalNumber m H) / ↑(m.choose 2)
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a : α
w : G.Walk a a
hwc : w.IsCircuit
hlg : ↑w.length < G.egirth
w' : G.Walk a a := w.cycleBypass
⊢ False

Tactic:
have hwc' : w'.IsCycle := hwc.isCycle_cycleBypass

Goal state after:
α : Type u_1
G : SimpleGraph α
a : α
w : G.Walk a a
hwc : w.IsCircuit
hlg : ↑w.length < G.egirth
w' : G.Walk a a := w.cycleBypass
hwc' : w'.IsCycle
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: n s t : ℕ
α : Type u_3
β : Type u_4
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ 2 * extremalNumber n (completeBipartiteGraph α β) ≤ zarankiewicz n n s t

Tactic:
conv =>
    enter [1, 2, 1]
    rw [← Fintype.card_fin n]

Goal state after:
n s t : ℕ
α : Type u_3
β : Type u_4
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ 2 * extremalNumber (Fintype.card (Fin n)) (completeBipartiteGraph α β) ≤ zarankiewicz n n s t
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
w : ↑M.verts
hw : w ∈ h.toEdge ⁻¹' {⟨s(u, v), huv⟩}
⊢ w ∈ {⟨u, ⋯⟩, ⟨v, ⋯⟩}

Tactic:
grind [h.mem_coe_toEdge w.property]

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

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : MulZeroOneClass R
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
a : α
e : Sym2 α
inst✝ : Nontrivial R
⊢ incMatrix R G a e = 1 ↔ e ∈ G.incidenceSet a

Tactic:
convert! one_ne_zero.ite_eq_left_iff

Goal state after:
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
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)
h1_le_rε : 1 ≤ ↑r * ε
⊢ ↑n ≤ ↑G.minDegree

Tactic:
← div_le_iff₀' (by positivity),

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)
h1_le_rε : 1 / ↑r ≤ ε
⊢ ↑n ≤ ↑G.minDegree
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✝ : NonAssocRing R
v : V
vec : V → R
⊢ (degMatrix R G *ᵥ vec) v - (adjMatrix R G *ᵥ vec) v = ↑(G.degree v) * vec v - ∑ u ∈ G.neighborFinset v, vec u

Tactic:
degMatrix_mulVec_apply,

Goal state after:
V : Type u_1
R : Type u_2
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : NonAssocRing R
v : V
vec : V → R
⊢ ↑(G.degree v) * vec v - (adjMatrix R G *ᵥ vec) v = ↑(G.degree v) * vec v - ∑ u ∈ G.neighborFinset v, vec u
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hw' : w' ∈ p.support
⊢ False

Tactic:
exact hw'1 (hcyc.snd_of_mem_support_of_isPath_of_adj _ hww' hw' hp hw'2)

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

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G ≃g G'
x✝ : ↑G.edgeSet
⊢ f.symm.toCopy.lineGraph (f.toCopy.lineGraph x✝) = x✝

Tactic:
simp [Copy.lineGraph, Copy.toLineGraphEmbedding, Sym2.map_map]

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

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G ≃g G'
x✝ : ↑G'.edgeSet
⊢ f.toCopy.lineGraph (f.symm.toCopy.lineGraph x✝) = x✝

Tactic:
simp [Copy.lineGraph, Copy.toLineGraphEmbedding, Sym2.map_map]

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

Goal state before:
pp: V : Type u_1
r : V
⊢ (starGraph r).IsUniversal r

Tactic:
by
  intro _ _
  simpa

Goal state after:
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
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
⊢ y = w'

Tactic:
· obtain ⟨w'', hw''⟩ := hG'cyc.other_adj_of_adj hr.1
      by_contra! hc
      simp_all [show M.Adj v y ↔ ¬M.Adj v w' by simpa using hG' hc hr.1 hw'.2]

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

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

Tactic:
grw [hn, vertexCoverNum_le_card_sub_one]

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ ν : YoungDiagram
h : μ.transpose ≤ ν.transpose
⊢ μ ≤ ν

Tactic:
convert! YoungDiagram.le_of_transpose_le h
    simp

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
⊢ ack 0 n = n + 1

Tactic:
ack

Goal state after:
n : ℕ
⊢ n + 1 = n + 1
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m : ℕ
⊢ ack (m + 1) 0 = ack m 1

Tactic:
ack

Goal state after:
m : ℕ
⊢ ack m 1 = ack m 1
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
⊢ ack (m + 1) (n + 1) = ack m (ack (m + 1) n)

Tactic:
ack

Goal state after:
m n : ℕ
⊢ ack m (ack (m + 1) n) = ack m (ack (m + 1) n)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ
n : ℕ
IH : ack 1 n = n + 2
⊢ ack 1 (n + 1) = n + 1 + 2

Tactic:
simp [IH]

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b, a ≤ b ∧ f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
⊢ f x = 0

Tactic:
have x₀_pos := calc
    0 < 1 := by norm_num
    _ ≤ x₀ := le_of_max_le_right hx₀_ge

Goal state after:
f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b, a ≤ b ∧ f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
⊢ f x = 0
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
⊢ False

Tactic:
obtain ⟨x, y, hxy⟩ := (not_isClique_iff _).mp hK

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x y : ↑K.supp
hxy : x ≠ y ∧ ¬Gmax.deleteUniversalVerts.coe.Adj ↑x ↑y
⊢ False