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

Goal state before:
pp: case inr.inr.inl
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inl l' ∈ left
⊢ ((Sum.inr l).isLeft = true → (Sum.inl l').isLeft = true) ∧ ((Sum.inr l).isRight = true → (Sum.inl l').isRight = true)

Tactic:
solve | simp | simpa using h hl hr | simpa using h hl' hr

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

Goal state before:
pp: case inr.inr.inr
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inr l' ∈ left
⊢ ((Sum.inr l).isLeft = true → (Sum.inr l').isLeft = true) ∧ ((Sum.inr l).isRight = true → (Sum.inr l').isRight = true)

Tactic:
solve | simp | simpa using h hl hr | simpa using h hl' hr

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1) →
    ∃ i_1,
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length

Tactic:
by aesop

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
⊢ p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}

Tactic:
by
  have hadj1 := ((show i - 1 + 1 = i by lia) ▸
    p.toSubgraph_adj_getVert (by lia : (i - 1) < p.length)).symm
  ext v
  simp_all only [ne_eq, Subgraph.mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff,
    SimpleGraph.Walk.toSubgraph_adj_iff, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq,
    Prod.swap_prod_mk]
  refine ⟨?_, by aesop⟩
  rintro ⟨i', ⟨hl1, hl2⟩ | ⟨hr1, hr2⟩⟩
  · apply hpc.getVert_injOn' (by rw [Set.mem_ofPred_eq]; lia)
      (by rw [Set.mem_ofPred_eq]; lia) at hl1
    simp_all
  · apply hpc.getVert_injOn (by rw [Set.mem_ofPred_eq]; lia)
      (by rw [Set.mem_ofPred_eq]; lia) at hr2
    aesop

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
huv : u = v
⊢ (p.toSubgraph.neighborSet u).ncard = 2

Tactic:
hpc.neighborSet_toSubgraph_endpoint

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
huv : u = v
⊢ {p.snd, p.penultimate}.ncard = 2
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
hw : w ∈ p.support
⊢ v ∉ q.support

Tactic:
by
  obtain ⟨p₀, p₁, hp₀, hp₁, happend⟩ := hp.mem_support_iff_exists_append.mp hw
  rw [← Subtype.mk.inj <| hG.subsingleton_path u w |>.elim ⟨p₀, hp₀⟩ ⟨q, hq⟩]
  exact fun hxp => (happend ▸ hp).ne_of_mem_support_of_append hadj.symm.ne' hxp
    (p₁.end_mem_support) rfl

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
⊢ u ∈ {v}ᶜ

Tactic:
by aesop

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst✝ : Fintype ↑(G.neighborSet z)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun w ↦ G.Adj z w) y → y = u
w x : ↑{z}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath).support
pwz : G.Walk (↑w) z
pzx : G.Walk z ↑x
p_eq_pwzx : ↑(pwu.append pux).toPath = pwz.append pzx
this : 1 ≤ List.count (pwz.getVert (pwz.length - 1)) pwz.support
⊢ ↑w ≠ z

Tactic:
by aesop

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
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
l2 : (G.replaceVertex s t).degree u = G.degree u - 1
⊢ 0 < G.degree u

Tactic:
G.degree_pos_iff_exists_adj u

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
l2 : (G.replaceVertex s t).degree u = G.degree u - 1
⊢ ∃ w, G.Adj u w
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
K : Type u_3
C : TopEdgeLabeling V K
k : K
x y : V
⊢ (EdgeLabeling.labelGraph C k).Adj x y ↔ ∃ (H : x ≠ y), EdgeLabeling.get C x y H = k

Tactic:
by
  simp [EdgeLabeling.labelGraph_adj, EdgeLabeling.get_eq]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst✝ : Fintype ↑(G.neighborSet z)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun w ↦ G.Adj z w) y → y = u
w x : ↑{z}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath).support
pwz : G.Walk (↑w) z
pzx : G.Walk z ↑x
p_eq_pwzx : ↑(pwu.append pux).toPath = pwz.append pzx
this : 1 ≤ List.count u pwz.support
⊢ z ≠ ↑x

Tactic:
by aesop

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hconn : G.Connected
u z : V
inst✝ : Fintype ↑(G.neighborSet z)
hdeg : G.degree z = 1
adj_vu : G.Adj z u
hu : ∀ (y : V), (fun w ↦ G.Adj z w) y → y = u
w x : ↑{z}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
hz : z ∈ (↑(pwu.append pux).toPath).support
pwz : G.Walk (↑w) z
pzx : G.Walk z ↑x
p_eq_pwzx : ↑(pwu.append pux).toPath = pwz.append pzx
this✝ : 1 ≤ List.count u pwz.support
this : 1 ≤ List.count pzx.snd pzx.support.tail
⊢ z ≠ ↑x

Tactic:
by aesop

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
hadj : G.Adj v w
hreach : G.Reachable u v
⊢ G.dist u v ≠ G.dist u w

Tactic:
obtain ⟨p, hp, hp'⟩ := hreach.exists_path_of_dist
  obtain ⟨q, hq, hq'⟩ := hreach.trans hadj.reachable |>.exists_path_of_dist
  rw [← hp', ← hq']
  by_cases hw : w ∈ p.support
  · rw [hG.path_concat hq hp hadj.symm hw, q.length_concat]
    exact q.length.ne_add_one.symm
  · have hv : v ∈ q.support := hG.mem_support_of_ne_mem_support_of_adj_of_isPath hq hp
      hadj.symm hw
    rw [hG.path_concat hp hq hadj hv, p.length_concat]
    exact p.length.ne_add_one

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
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ G.CliqueFree (r + 1) → ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
rintro -

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ G.Preconnected ∧ univ.Nonempty ↔ G.Connected

Tactic:
connected_iff,

Goal state after:
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ G.Preconnected ∧ univ.Nonempty ↔ G.Preconnected ∧ Nonempty V
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
⊢ ⊥.center = Set.univ

Tactic:
by
  cases subsingleton_or_nontrivial α
  · exact center_eq_univ_of_subsingleton
  · rw [Set.eq_univ_iff_forall]
    intro u
    rw [mem_center_iff, eccent_bot, radius_bot]

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

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
h_bdd : BddBelow {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
⊢ Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop (𝓝 H.turanDensity)

Tactic:
have h_tto := Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici
    (antitoneOn_extremalNumber_div_choose_two H) h_bdd

Goal state after:
W : Type u_1
H : SimpleGraph W
h_bdd : BddBelow {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
h_tto :
  Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop
    (𝓝 (sInf ((fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) '' Set.Ici 2)))
⊢ Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop (𝓝 H.turanDensity)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
⊢ ∑ _x ∈ K.verts, (↑G.minDegree - ↑(#K.verts)) ≤ ↑(∑ v ∈ K.verts, (between (↑K.verts) (↑K.verts)ᶜ G).degree v)

Tactic:
Nat.cast_sum

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
⊢ ∑ _x ∈ K.verts, (↑G.minDegree - ↑(#K.verts)) ≤ ∑ x ∈ K.verts, ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree x)
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:
rw [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.Girth

Goal state before:
pp: α : Type u_1
h : 3 ≤ ENat.card α
s : Finset α
hcard : 3 = s.card
x y z : α
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
w : ⊤.Walk x x := Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
hw : w = Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
⊢ w.edges.Nodup

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
h : 3 ≤ ENat.card α
s : Finset α
hcard : 3 = s.card
x y z : α
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
w : ⊤.Walk x x := Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
hw : w = Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
⊢ w ≠ Walk.nil

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
h : 3 ≤ ENat.card α
s : Finset α
hcard : 3 = s.card
x y z : α
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
w : ⊤.Walk x x := Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
hw : w = Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
⊢ w.support.tail.Nodup

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard

Tactic:
by
  obtain hs | hs := s.infinite_or_finite
  · rw [hs.ncard]
    by_cases h : 1 = 0
    · simp [h]
    · exact finsum_mem_eq_zero_of_infinite (by simpa [Function.support_const h])
  · simp [finsum_mem_eq_finite_toFinset_sum _ hs, Set.ncard_eq_toFinset_card s hs]

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

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype ↑M.verts
h : ∀ v ∈ M.verts, M.degree v = 1
⊢ M.verts.toFinset.card = M.coe.edgeFinset.card + M.coe.edgeFinset.card

Tactic:
← two_mul,

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Fintype ↑M.verts
h : ∀ v ∈ M.verts, M.degree v = 1
⊢ M.verts.toFinset.card = 2 * M.coe.edgeFinset.card
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 - adjMatrix R G) *ᵥ vec) v = ↑(G.degree v) * vec v - ∑ u ∈ G.neighborFinset v, vec u

Tactic:
sub_mulVec,

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
⊢ (degMatrix R G *ᵥ vec - adjMatrix R G *ᵥ vec) v = ↑(G.degree v) * vec v - ∑ u ∈ G.neighborFinset v, vec u
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✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ x ⬝ᵥ (degMatrix R G - adjMatrix R G) *ᵥ x = (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Tactic:
sub_mulVec,

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✝¹ : Field R
inst✝ : CharZero R
x : V → R
⊢ x ⬝ᵥ (degMatrix R G *ᵥ x - adjMatrix R G *ᵥ x) = (∑ i, ∑ j, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
⊢ ?m.46 ∈ p.support

Tactic:
by aesop

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

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Partitionable n → G.Colorable n

Tactic:
rintro ⟨P, hf, hc⟩

Goal state after:
case mp
V : Type u
G : SimpleGraph V
n : ℕ
P : G.Partition
hf : P.parts.Finite
hc : hf.toFinset.card ≤ n
⊢ G.Colorable n
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)))
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
⊢ G.minDegree * (#W + (k + k)) ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w

Tactic:
← two_mul,

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)))
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
⊢ G.minDegree * (#W + 2 * k) ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
⊢ (p.toSubgraph.spanningCoe ⊔ edge x a).Adj a c

Tactic:
by aesop

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

Goal state before:
pp: μ : YoungDiagram
i : ℕ
hi : i ∈ List.range (μ.colLen 0)
⊢ 0 < μ.rowLen i

Tactic:
List.mem_range,

Goal state after:
μ : YoungDiagram
i : ℕ
hi : i < μ.colLen 0
⊢ 0 < μ.rowLen i
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
cycles : SimpleGraph V := ⋯
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
x' : V
hx' : x' ∈ {x, b}
hx'p : x' ∈ p'.support
htw : ∀ t ∈ {x, b}, t ∈ (p'.takeUntil x' hx'p).support → t = x'
⊢ ¬(p'.takeUntil x' hx'p).Nil

Tactic:
Walk.nil_takeUntil

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
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
x' : V
hx' : x' ∈ {x, b}
hx'p : x' ∈ p'.support
htw : ∀ t ∈ {x, b}, t ∈ (p'.takeUntil x' hx'p).support → t = x'
⊢ ¬a = x'
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
x : ℝ
hx₁ : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
hx₂ : ∀ (y : ℝ), b * id x ≤ y → f y = g y
hx₃ : f x = g x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)

Tactic:
hx₂ u hu.1,

Goal state after:
f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
x : ℝ
hx₁ : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
hx₂ : ∀ (y : ℝ), b * id x ≤ y → f y = g y
hx₃ : f x = g x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ g u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: ⊢ (fun n ↦ ↑n / log ↑n ^ 2) = fun n ↦ ↑n * (log ↑n ^ 2)⁻¹

Tactic:
by simp_rw [div_eq_mul_inv]

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
x₀_pos : 0 < x₀
hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0
⊢ 0 ≤ -logb 2 (x / x₀)

Tactic:
rw [neg_nonneg]

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₀
hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0
⊢ logb 2 (x / x₀) ≤ 0
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : 1 < n
hn' : ∀ (i : α), 0 < log (b i * ↑n)
h_log_pos : 0 < log ↑n
⊢ log ↑n ≠ 0

Tactic:
by aesop

Goal state after: