mathlib-initiative/mathlib-tactics huggingface dataset:
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 α
d : ℕ
a : α
hd : G.IsRegularOfDegree d
v : V
⊢ (adjMatrix α G *ᵥ Function.const V a) v = ↑d * a

Tactic:
by
  simp [hd v]

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

Goal state before:
pp: 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)
⊢ Odd n

Tactic:
exact hOdd

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
hnil : ¬p.Nil
w : V
hadj : (fun w ↦ G.Adj u w) w
this : ¬(cons ⋯ p).IsPath
⊢ w ∈ p.support

Tactic:
grind [hp.cons]

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
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
⊢ (induce {v}ᶜ G).Reachable w x

Tactic:
Reachable,

Goal state after:
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
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
⊢ Nonempty ((induce {v}ᶜ G).Walk w x)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case map_rel_iff'.inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
c : Fintype.card V < r
lc : ∀ (x : V), ↑(zm ⟨x, ⋯⟩) < Fintype.card V
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % min (Fintype.card V) r = ↑(zm ⟨b, ⋯⟩) % min (Fintype.card V) r

Tactic:
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)]

Goal state after:
case map_rel_iff'.inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
c : Fintype.card V < r
lc : ∀ (x : V), ↑(zm ⟨x, ⋯⟩) < Fintype.card V
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r
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
⊢ Disjoint s c.supp

Tactic:
Set.disjoint_left

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⦄, a ∈ s → a ∉ c.supp
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h : G.ediam = 1
⊢ G = ⊤

Tactic:
eq_top_iff_forall_eccent_eq_one

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h : G.ediam = 1
⊢ ∀ (u : α), G.eccent u = 1
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_2
α : 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
i₁ i₂ : Fin r
h :
  (fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ) i₁ =
    (fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ) i₂
⊢ i₁ = i₂

Tactic:
simp_rw [Finset.ext_iff] at h
      have : NeZero t := ⟨ht⟩
      obtain ⟨_, heq⟩ : ∃ j, f (i₁, j) = f (i₂, 0) := by simpa using h <| f (i₂, 0)
      apply f.injective at heq
      rw [Prod.mk.injEq] at heq
      exact heq.left

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

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
⊢ (∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C) → C.supp.Infinite

Tactic:
· rintro h Cfin
      obtain ⟨D, e⟩ := h (K ∪ Cfin.toFinset) Finset.subset_union_left
      obtain ⟨v, vD⟩ := D.nonempty
      let Ddis := D.disjoint_right
      simp_rw [Finset.coe_union, Set.Finite.coe_toFinset, Set.disjoint_union_left,
        Set.disjoint_iff] at Ddis
      exact Ddis.right ⟨(ComponentCompl.hom_eq_iff_le _ _ _).mp e vD, vD⟩

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

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
K L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
⊢ Finite (induce (↑∅)ᶜ G).ConnectedComponent

Tactic:
Finset.coe_empty,

Goal state after:
case inl
V : Type u
G : SimpleGraph V
K L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
⊢ Finite (induce ∅ᶜ G).ConnectedComponent
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
hwc' : w'.IsCycle
⊢ ↑w.length < G.egirth

Tactic:
exact hlg

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).ncard ≤ ∑ i, (s i).ncard

Tactic:
simpa using Finset.univ.set_ncard_biUnion_le s

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
s : Finset V
⊢ s.card ≤ (s.biUnion fun x ↦ G.neighborFinset x).card

Tactic:
have := h₂ s

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
s : Finset V
this : (↑s).ncard ≤ (⋃ x ∈ ↑s, G.neighborSet x).ncard
⊢ s.card ≤ (s.biUnion fun x ↦ G.neighborFinset x).card
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 : 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:
Set.disjoint_left

Goal state after:
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
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
h : G.CliqueFree (r + 2)
⊢ k < r

Tactic:
contrapose! h
  -- If `r ≤ k` then `s = t` and so `s ∪ {w₁, w₂}` is an `r + 2`-clique, a contradiction.
  have hs := eq_of_subset_of_card_le inter_subset_left (hw.card_inter ▸ hw.card_left ▸ h)
  have := eq_of_subset_of_card_le inter_subset_right (hw.card_inter ▸ hw.card_right ▸ h)
  exact (hw.isNClique_fst_left.insert_insert (hs ▸ this.symm ▸ hw.isNClique_snd_right)
    hw.snd_notMem_left hw.isPathGraph3Compl.adj).not_cliqueFree

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst✝ : Fintype α
hp : p.IsHamiltonianCycle
⊢ 1 ≤ Fintype.card α

Tactic:
rw [Nat.succ_le_iff, Fintype.card_pos_iff]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst✝ : Fintype α
hp : p.IsHamiltonianCycle
⊢ Nonempty α
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
⊢ ∃ i, ∃ (_ : i ∈ M.edgeSet), v ∈ ↑i

Tactic:
have ⟨u, he, _⟩ := h hv
    exact ⟨s(v, u), he, Sym2.mem_mk_left ..⟩

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

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
⊢ ∀ (y : V), (fun w' ↦ w ≠ w' ∧ G.Adj v w') y → y = w'

Tactic:
intro y ⟨hwy, hwy'⟩

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
w' : V
hww : w ≠ w'
hww' : G.Adj v w'
y : V
hwy : w ≠ y
hwy' : G.Adj v y
⊢ y = w'
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: case cons
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) (cons huv p).edges) ↔ u✝ ≠ w✝ → x ≠ u✝ ∧ x ≠ w✝

Tactic:
simp only [List.countP_cons, Ne, edges_cons, Sym2.mem_iff]

Goal state after:
case cons
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges + if decide (x = u✝ ∨ x = v✝) = true then 1 else 0) ↔
    ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case refine_1
ε : ℝ
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₁ p₂ : ↥K.parts
heq : y ↑p₁ ⋯ = y ↑p₂ ⋯
hy₁' : y ↑p₁ ⋯ ⊆ ↑p₁ ∧ #(y ↑p₁ ⋯) = t
hy₂' : y ↑p₁ ⋯ ⊆ ↑p₂ ∧ #(y ↑p₁ ⋯) = t
v : Fin n
hv : v ∈ y ↑p₁ ⋯
hne : p₁ ≠ p₂
⊢ ¬G.Adj v v

Tactic:
exact G.loopless.irrefl v

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

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

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

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

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

Tactic:
rwa [List.mem_range, ← mem_iff_lt_colLen, mem_iff_lt_rowLen] at hi

Goal state after:
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
⊢ Primrec Subtype.val

Tactic:
let := Primcodable.subtype hp
  refine (Primcodable.prim (Subtype p)).of_eq fun n => ?_
  rcases @decode (Subtype p) _ n with (_ | ⟨a, h⟩) <;> rfl

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

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
a b c : V
M2 : (G ⊔ edge a c).Subgraph
hab : G.Adj a b
hnGac : ¬G.Adj a c
hnac : a ≠ c
hnbc : b ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x'✝ x' c' : V
hc : c' ≠ a
w : V
M1 : (G ⊔ edge x' b).Subgraph
hxa : G.Adj x' a
hnGxb : ¬G.Adj x' b
hnxb : x' ≠ b
hnxc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x' b
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
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
hx' : x'✝ ∈ {x', b}
p : cycles.Walk a x'✝
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x' b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
hadj : p.toSubgraph.Adj c' x'
hl : (M1.spanningCoe \ M2.spanningCoe).Adj c' x'
hw : ∀ (y : V), (fun w ↦ M1.Adj x' w) y → y = w
⊢ p.toSubgraph.Adj x' b

Tactic:
rw [hw _ hM1xb, ← hw _ hl.1.symm]

Goal state after:
case inl
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
a b c : V
M2 : (G ⊔ edge a c).Subgraph
hab : G.Adj a b
hnGac : ¬G.Adj a c
hnac : a ≠ c
hnbc : b ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x'✝ x' c' : V
hc : c' ≠ a
w : V
M1 : (G ⊔ edge x' b).Subgraph
hxa : G.Adj x' a
hnGxb : ¬G.Adj x' b
hnxb : x' ≠ b
hnxc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x' b
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
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
hx' : x'✝ ∈ {x', b}
p : cycles.Walk a x'✝
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x' b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
hadj : p.toSubgraph.Adj c' x'
hl : (M1.spanningCoe \ M2.spanningCoe).Adj c' x'
hw : ∀ (y : V), (fun w ↦ M1.Adj x' w) y → y = w
⊢ p.toSubgraph.Adj x' c'
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case zero
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_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hx : ∀ u ∈ Set.Icc (1 / 2 * x₀) x₀, f u = 0
⊢ ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-1) * x₀) x₀ → f z = 0

Tactic:
refine fun z _ hz => hx _ ?_

Goal state after:
case zero
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_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hx : ∀ u ∈ Set.Icc (1 / 2 * x₀) x₀, f u = 0
z : ℝ
x✝ : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-1) * x₀) x₀
⊢ z ∈ Set.Icc (1 / 2 * x₀) x₀
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ -(z ^ (p - 1) / log z ^ 2)) =o[atTop] fun z ↦ z ^ (p - 1) / 1

Tactic:
by
            simp_rw [isLittleO_neg_left, div_eq_mul_inv]
            refine IsBigO.mul_isLittleO (isBigO_refl _ _)
              (IsLittleO.inv_rev ?_ (by simp))
            rw [isLittleO_const_left]
            refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
            exact Tendsto.comp (g := fun z => z ^ 2)
              (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop

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

Goal state before:
pp: x : ℝ
hx : rexp 1 ≤ x
⊢ 1 + ε x ≤ 2

Tactic:
by
  simp only [smoothingFn, ← one_add_one_eq_two]
  gcongr
  have : 1 < x := by
    calc 1 = exp 0 := by simp
         _ < exp 1 := by simp
         _ ≤ x := hx
  rw [div_le_one (log_pos this)]
  calc 1 = log (exp 1) := by simp
       _ ≤ log x := log_le_log (exp_pos _) hx

Goal state after:
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
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
⊢ c₂ / c₁ ^ (p a b + 1) * g ↑n ≤ max c₂ (c₂ / c₁ ^ (p a b + 1)) * g ↑n

Tactic:
by gcongr; exact le_max_right _ _

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

Goal state before:
pp: case h₂
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
hfg₃ : ‖g u‖ ≤ 1 / 2 * f u
⊢ -|g u| ≤ g u

Tactic:
exact neg_abs_le _

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case comp
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h : ∃ a, evaln (k + 1) a✝ n = some a ∧ evaln (k + 1) a✝¹ a = some x
⊢ ∃ a ∈ a✝.eval n, x ∈ a✝¹.eval a

pp: case prec
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h :
  Nat.rec (evaln (k + 1) a✝¹ (unpair n).1)
      (fun n_1 n_ih ↦
        (evaln k (a✝¹.prec a✝) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
          evaln (k + 1) a✝ (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2 =
    some x
⊢ x ∈
    Nat.rec (a✝¹.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ a✝.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
      (unpair n).2

pp: case rfind'
k : ℕ
a✝ : Code
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h :
  ∃ a,
    evaln (k + 1) a✝ n = some a ∧
      (if a = 0 then some (unpair n).2 else evaln k a✝.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
⊢ ∃ a,
    (0 ∈ a✝.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
        ∀ {m : ℕ}, m < a → ∃ a ∈ a✝.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
      a + (unpair n).2 = x

Tactic:
case comp cf cg hf hg _ =>
      rcases h with ⟨y, eg, ef⟩
      exact ⟨_, hg _ _ eg, hf _ _ ef⟩

Goal state after:
case prec
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h :
  Nat.rec (evaln (k + 1) a✝¹ (unpair n).1)
      (fun n_1 n_ih ↦
        (evaln k (a✝¹.prec a✝) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
          evaln (k + 1) a✝ (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2 =
    some x
⊢ x ∈
    Nat.rec (a✝¹.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ a✝.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
      (unpair n).2

case rfind'
k : ℕ
a✝ : Code
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h :
  ∃ a,
    evaln (k + 1) a✝ n = some a ∧
      (if a = 0 then some (unpair n).2 else evaln k a✝.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
⊢ ∃ a,
    (0 ∈ a✝.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
        ∀ {m : ℕ}, m < a → ∃ a ∈ a✝.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
      a + (unpair n).2 = x
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case prec
cf cg : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ}, x ∈ cg.eval n → ∃ k, x ∈ evaln (k + 1) cg n
n x : ℕ
h :
  x ∈
    Nat.rec (cf.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
      (unpair n).2
⊢ ∃ k,
    n ≤ k ∧
      Nat.rec (evaln (k + 1) cf (unpair n).1)
          (fun n_1 n_ih ↦
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          (unpair n).2 =
        some x

Tactic:
revert h
    generalize n.unpair.1 = n₁; generalize n.unpair.2 = n₂
    induction n₂ generalizing x n with simp [Option.bind_eq_some_iff]
    | zero =>
      intro h
      rcases hf h with ⟨k, hk⟩
      exact ⟨_, le_max_left _ _, evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk⟩
    | succ m IH =>
      intro y hy hx
      rcases IH hy with ⟨k₁, nk₁, hk₁⟩
      rcases hg hx with ⟨k₂, hk₂⟩
      refine
        ⟨(max k₁ k₂).succ,
          Nat.le_succ_of_le <| le_max_of_le_left <|
            le_trans (le_max_left _ (Nat.pair n₁ m)) nk₁, y,
          evaln_mono (Nat.succ_le_succ <| le_max_left _ _) ?_,
          evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_right _ _) hk₂⟩
      simp only [evaln.eq_8, bind, unpaired, unpair_pair, Option.mem_def, Option.bind_eq_some_iff,
        Option.guard_eq_some', exists_and_left, exists_const]
      exact ⟨le_trans (le_max_right _ _) nk₁, hk₁⟩

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

Goal state before:
pp: case h₂
f g : ℝ → ℝ
hf✝ : GrowsPolynomially f
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ -|g u| ≤ g u

Tactic:
exact neg_abs_le _

Goal state after: