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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ 2 < G.edist u v ↔ u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ lt_of_le_of_ne ?_ (Ne.symm ?_)⟩
  · have hn : u ≠ v := fun hc ↦ by simp [hc] at h
    have : ¬ G.Adj u v := fun hc ↦ by simp +decide [edist_eq_one_iff_adj.mpr hc] at h
    use hn, this
    by_contra! hc
    simp [edist_eq_two_iff.mpr ⟨hn, this, hc⟩] at h
  · rw [← one_add_one_eq_two]
    refine Order.add_one_le_of_lt <| lt_of_le_of_ne ?_ ?_
    <;> grind [Order.one_le_iff_pos, pos_iff_ne_zero, edist_eq_zero_iff, edist_eq_one_iff_adj]
  · simp_all [edist_eq_two_iff]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : V
⊢ G.ball c ⊤ = (G.connectedComponentMk c).supp

Tactic:
by
  simp [Set.ext_iff, lt_top_iff_ne_top, edist_ne_top_iff_reachable]

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

Goal state before:
pp: ⊢ cycleGraph 2 = ⊤

Tactic:
simp only [SimpleGraph.ext_iff, funext_iff]
  decide

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

Goal state before:
pp: ⊢ cycleGraph 3 = ⊤

Tactic:
simp only [SimpleGraph.ext_iff, funext_iff]
  decide

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

Goal state before:
pp: n : ℕ
⊢ cycleGraph (n + 1) = circulantGraph {1}

Tactic:
cases n
  · exact edgeFinset_inj.mp rfl
  · aesop

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ #G.edgeFinset ≤ extremalNumber (Fintype.card V) H

Tactic:
by
  rw [extremalNumber_of_fintypeCard_eq rfl]
  convert! @le_sup _ _ _ _ {G | H.Free G} (#·.edgeFinset) G (by simpa using h)

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✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (fun i ↦ adjMatrix α G i v) = adjMatrix α G v

Tactic:
ext x

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 v x
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
this : ¬Maximal (fun F ↦ F ≤ G ∧ F.IsAcyclic) F
H : SimpleGraph V
hFH : F < H
hHG : H ≤ G
hH : H.IsAcyclic
e : Sym2 V
heH : e ∈ H.edgeSet
heF : e ∉ F.edgeSet
⊢ False

Tactic:
have h_bridge : (F ⊔ fromEdgeSet {e}).IsBridge e := by
    refine isAcyclic_iff_forall_isBridge.mp ?_ <| by simp [H.not_isDiag_of_mem_edgeSet heH]
    exact hH.anti <| sup_le_iff.mpr ⟨hFH.le, H.fromEdgeSet_le.mpr <| by grind⟩

Goal state after:
V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
this : ¬Maximal (fun F ↦ F ≤ G ∧ F.IsAcyclic) F
H : SimpleGraph V
hFH : F < H
hHG : H ≤ G
hH : H.IsAcyclic
e : Sym2 V
heH : e ∈ H.edgeSet
heF : e ∉ F.edgeSet
h_bridge : (F ⊔ fromEdgeSet {e}).IsBridge e
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n : ℕ
h : Even 1
u v : Fin 1
hadj : (cycleGraph 1).Adj u v
⊢ decide (↑u % 2 = 0) ≠ decide (↑v % 2 = 0)

Tactic:
simp at h

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

Goal state before:
pp: case refine_1
V : Type u_1
G T : SimpleGraph V
hG : G.Connected
hT : T ≤ G
this : Nonempty V
h : Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) T
u v : V
⊢ T.Reachable u v

Tactic:
exact G.reachable_eq_of_maximal_isAcyclic T h ▸ hG.preconnected u v

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

Goal state before:
pp: n : ℕ
h : 2 ≤ 1
u v : Fin 1
hadj : (cycleGraph 1).Adj u v
⊢ (if ↑u = 1 - 1 then 2 else ⟨↑u % 2, ⋯⟩) ≠ if ↑v = 1 - 1 then 2 else ⟨↑v % 2, ⋯⟩

Tactic:
simp at h

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

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

Tactic:
split_ifs with hu hv

Goal state after:
case pos
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hadj : u - v = 1 ∨ v - u = 1
hu : ↑u = n + 2 - 1
hv : ↑v = n + 2 - 1
⊢ 2 ≠ 2

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

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

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
k : K
⊢ C.labelGraph k ≤ G

Tactic:
by
  intro x y
  grind [labelGraph_adj]

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
β : Type u_1
H : SimpleGraph β
f : H ↪g G
⊢ G.IsCompleteMultipartite → H.IsCompleteMultipartite

Tactic:
intro h; contrapose h
  exact not_isCompleteMultipartite_of_pathGraph3ComplEmbedding
          <| f.comp (pathGraph3ComplEmbeddingOf h)

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.diam = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α

Tactic:
rw [diam, ENat.toNat_eq_zero, or_comm, ediam_eq_zero_iff_subsingleton]

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

Goal state before:
pp: case inl
α : Type u_1
G : SimpleGraph α
h✝ : IsEmpty α
⊢ G.ediam ≤ 2 * G.radius

Tactic:
rw [radius_eq_top_of_isEmpty]
    exact le_top

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Subsingleton α
u : α
⊢ G.eccent u = G.radius

Tactic:
eccent_eq_zero_of_subsingleton u,

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Subsingleton α
u : α
⊢ 0 = G.radius
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✝²
h₁ : ∃ y, map { toFun := fun j ↦ f (y, j), inj' := ⋯ } univ = x✝³
h₂ : ∃ y, map { toFun := fun j ↦ f (y, j), inj' := ⋯ } univ = x✝²
⊢ G.Adj x✝¹ x✝

Tactic:
replace ⟨_, h₁⟩ := 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✝¹ : V
h₁' : x✝¹ ∈ ↑x✝³
x✝ : V
h₂' : x✝ ∈ ↑x✝²
h₂ : ∃ y, map { toFun := fun j ↦ f (y, 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.Ends.Properties

Goal state before:
pp: V : Type
G : SimpleGraph V
e : ↑G.end
K : (Finset V)ᵒᵖ
⊢ (ComponentCompl.supp (↑e K)).Infinite

Tactic:
refine (e.val K).infinite_iff_in_all_ranges.mpr (fun L h => ?_)

Goal state after:
V : Type
G : SimpleGraph V
e : ↑G.end
K : (Finset V)ᵒᵖ
L : Finset V
h : Opposite.unop K ⊆ L
⊢ ∃ D, ComponentCompl.hom h D = ↑e K
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
⊢ Disjoint K ↑C

Tactic:
Set.disjoint_iff

Goal state after:
V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
⊢ K ∩ ↑C ⊆ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
C D : G.ComponentCompl K
ne : C ≠ D
⊢ Disjoint ↑C ↑D

Tactic:
Set.disjoint_iff

Goal state after:
V : Type u
G : SimpleGraph V
K : Set V
C D : G.ComponentCompl K
ne : C ≠ D
⊢ ↑C ∩ ↑D ⊆ ∅
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_2.refine_2
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 ⋯) = r + 1 ∨ t = 0

Tactic:
rw [Finset.card_cons, K.card_parts.resolve_right ht]

Goal state after:
case neg.refine_2.refine_2
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
⊢ r + 1 = r + 1 ∨ t = 0
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
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
D : G.ComponentCompl ↑(K ∪ Cfin.toFinset)
e : hom ⋯ D = C
v : V
vD : v ∈ ↑D
Ddis : Disjoint ↑K ↑D ∧ Disjoint C.supp ↑D
⊢ False

Tactic:
Set.disjoint_iff

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
D : G.ComponentCompl ↑(K ∪ Cfin.toFinset)
e : hom ⋯ D = C
v : V
vD : v ∈ ↑D
Ddis : ↑K ∩ ↑D ⊆ ∅ ∧ C.supp ∩ ↑D ⊆ ∅
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
B : SimpleGraph (Fin m ⊕ Fin n)
left✝ : B ≤ completeBipartiteGraph (Fin m) (Fin n)
h : (completeBipartiteGraph (Fin s) (Fin t)).Free B
⊢ #B.edgeFinset ≤ extremalNumber (Fintype.card (Fin (m + n))) (completeBipartiteGraph α β)

Tactic:
rw [(Iso.map finSumFinEquiv B).card_edgeFinset_eq]

Goal state after:
m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
B : SimpleGraph (Fin m ⊕ Fin n)
left✝ : B ≤ completeBipartiteGraph (Fin m) (Fin n)
h : (completeBipartiteGraph (Fin s) (Fin t)).Free B
⊢ #(SimpleGraph.map (⇑finSumFinEquiv) B).edgeFinset ≤
    extremalNumber (Fintype.card (Fin (m + n))) (completeBipartiteGraph α β)
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (r + 2)) G
hnc : ¬G.IsCompleteMultipartite
v w₁ w₂ : α
p3 : G.IsPathGraph3Compl v w₁ w₂
s : Finset α
h1 : v ∉ s
h2 : w₁ ∉ s
h3 : G.IsNClique (r + 1) (insert v s)
h4 : G.IsNClique (r + 1) (insert w₁ s)
t : Finset α
h5 : v ∉ t
h6 : w₂ ∉ t
h7 : G.IsNClique (r + 1) (insert v t)
h8 : G.IsNClique (r + 1) (insert w₂ t)
⊢ ∃ v w₁ w₂ s t, G.IsFiveWheelLike r (#(s ∩ t)) v w₁ w₂ s t

Tactic:
exact ⟨_, _, _, _, _, p3, h1, h5, h2, h6, h3, h4, h7, h8, rfl⟩

Goal state after:
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 : r ≤ k
hs : s ∩ t = s
this : s ∩ t = t
⊢ ¬G.CliqueFree (r + 2)

Tactic:
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 b : α
p : G.Walk a b
inst✝ : Fintype α
hp : p.IsHamiltonian
⊢ p.support.length = Fintype.card α

Tactic:
by
  have : Inhabited α := ⟨a⟩
  grind [Fintype.card_ne_zero, length_eq]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
x 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
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
⊢ c = a ∧ d = b

Tactic:
by
    by_contra! hf
    apply h2.not_gt <| two_lt_card_iff.2 _
    by_cases h : a = c
    · exact ⟨a, b, d, by grind⟩
    · exact ⟨a, b, c, by grind⟩

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

Goal state before:
pp: V✝ V : Type u_1
v w : V
hadj : v ≠ w ∧ (v = v ∨ w = v)
⊢ ((starGraph v).deleteEdges {s(v, w)}).neighborSet w = ∅

Tactic:
ext x

Goal state after:
V✝ V : Type u_1
v w : V
hadj : v ≠ w ∧ (v = v ∨ w = v)
x : V
⊢ x ∈ ((starGraph v).deleteEdges {s(v, w)}).neighborSet w ↔ x ∈ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: case inr.convert_2
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ {x | ¬u = v ∧ (¬x = u → x = v)} = {u, v}

Tactic:
ext x

Goal state after:
case inr.convert_2
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
x : V
⊢ x ∈ {x | ¬u = v ∧ (¬x = u → x = v)} ↔ x ∈ {u, v}
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ {x | ¬u = v ∧ (¬x = u → x = v)} = ∅ ∨ {x | ¬u = v ∧ (¬x = u → x = v)}.card = 2

Tactic:
right
    convert_to _ = ({u, v} : Finset V).card
    · simp [hn]
    · congr
      ext x
      simp [hn, imp_iff_not_or]

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

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h✝ : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
v : V
hv : v ∈ Set.univ \ G.universalVerts
h : v ∈ M1.verts
⊢ v ∈ M1.verts ∪ M2.verts

pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h✝ : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
v : V
hv : v ∈ Set.univ \ G.universalVerts
h : v ∉ M1.verts
⊢ v ∈ M1.verts ∪ M2.verts

Tactic:
· exact M1.verts.mem_union_left _ h

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h✝ : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
v : V
hv : v ∈ Set.univ \ G.universalVerts
h : v ∉ M1.verts
⊢ v ∈ M1.verts ∪ M2.verts
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
⊢ μ.transpose.transpose = μ

Tactic:
ext x

Goal state after:
μ : YoungDiagram
x : ℕ × ℕ
⊢ x ∈ μ.transpose.transpose.cells ↔ x ∈ μ.cells
Module: Mathlib.Computability.Partrec

Goal state before:
pp: x✝² x✝¹ : ℕ
x✝ : x✝¹ ∈ Nat.rfind fun n ↦ (fun m ↦ decide (m = 0)) <$> (↑fun x ↦ 1) (Nat.pair x✝² n)
h : (Nat.rfind fun n ↦ (fun m ↦ decide (m = 0)) <$> (↑fun x ↦ 1) (Nat.pair x✝² n)).Dom
h✝ : (Nat.rfind fun n ↦ (fun m ↦ decide (m = 0)) <$> (↑fun x ↦ 1) (Nat.pair x✝² n)).get h = x✝¹
⊢ False

Tactic:
simp at h

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
⊢ Nat.rec (↑g a) (fun y IH ↦ IH.bind fun i ↦ ↑(h a) (y, i)) (f a) =
    (↑fun a ↦ Nat.rec (g a) (fun y IH ↦ h a (y, IH)) (f a)) a

Tactic:
by simp; induction f a <;> simp [*]

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

Goal state before:
pp: case comp
n : ℕ
f : List.Vector ℕ n → ℕ
m✝ n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
g✝ : Fin n✝ → List.Vector ℕ m✝ → ℕ
a✝¹ : Primrec' f✝
a✝ : ∀ (i : Fin n✝), Primrec' (g✝ i)
hf : Primrec f✝
hg : ∀ (i : Fin n✝), Primrec (g✝ i)
⊢ Primrec fun a ↦ f✝ (ofFn fun i ↦ g✝ i a)

Tactic:
| comp _ _ _ hf hg =>

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * (2 ^ (n + 3) - 3) + 3 = 2 ^ (n + 3).succ - 3

Tactic:
Nat.pow_succ 2 (n + 3),

Goal state after:
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * (2 ^ (n + 3) - 3) + 3 = 2 ^ (n + 3) * 2 - 3
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
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / log ↑n ^ 2

Tactic:
by
  rw [Filter.eventually_all]
  intro i
  simpa using IsLittleO.eventuallyLE (R.dist_r_b i)

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_pos : 0 < x
x₀ : ℝ
hx₀_ge : max x 1 ≤ x₀
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
ih : f (2 ^ (-↑k - 1) * x₀) = 0
z : ℝ
hxz : x ≤ z
hz : z ∈ Set.Icc (2 ^ (-(↑k + 1) - 1) * x₀) (2 ^ (-(↑k + 1)) * x₀)
hx' : x ≤ 2 ^ (-↑k - 1) * x₀
hx : z ∈ Set.Icc (1 / 2 * (2 ^ (-↑k - 1) * x₀)) (2 ^ (-↑k - 1) * x₀) → f z = 0
⊢ 1 / 2 * (2 ^ (-↑k - 1) * x₀) ≤ z

Tactic:
rw [one_div, ← zpow_neg_one, ← mul_assoc, ← zpow_add₀ (by norm_num)]
        have h₁ : (-1 : ℤ) + (-k - 1) = -k - 2 := by ring
        have h₂ : -(k + (1 : ℤ)) - 1 = -k - 2 := by ring
        rw [h₁]
        rw [h₂] at hz
        exact hz.1

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly✝ : GrowsPolynomially fun x ↦ ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
hb' : ∀ (i : α), b' ≤ b i
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
hq_poly :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b' * x) x,
      (fun x ↦ ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x ↦ ‖deriv q x‖) x) (c₂ * (fun x ↦ ‖deriv q x‖) x)
h_tendsto : Tendsto (fun x ↦ b' * x) atTop atTop
n : ℕ
hn : ∀ u ∈ Set.Icc (b' * ↑n) ↑n, ‖deriv q u‖ ∈ Set.Icc (c₁ * ‖deriv q ↑n‖) (c₂ * ‖deriv q ↑n‖)
h_bi_le_r : ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
h_ge_n₀ : R.n₀ ≤ n
h_n_pos : 0 < n
h_bn : 1 < b' * ↑n
⊢ b i * ↑n ∈ Set.Icc (b' * ↑n) ↑n

Tactic:
refine ⟨by gcongr; exact hb' i, ?_⟩
    calc b i * n ≤ 1 * n := by gcongr; exact le_of_lt <| R.b_lt_one i
                 _ = n := by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
⊢ (fun n ↦ ↑n ^ (p a b - 1) * (↑n / log ↑n ^ 2)) =ᶠ[atTop] fun n ↦ ↑n ^ p a b / log ↑n ^ 2

Tactic:
filter_upwards [eventually_ne_atTop 0] with n hn

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 - ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (p a b - 1) * (↑n / log ↑n ^ 2) = ↑n ^ p a b / log ↑n ^ 2
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 : α
⊢ (fun n ↦ (log ↑n - log (b i * ↑n)) / (log (b i * ↑n) * log ↑n)) =ᶠ[atTop] fun n ↦
    (log ↑n - log (b i) - log ↑n) / ((log (b i) + log ↑n) * log ↑n)

Tactic:
filter_upwards [eventually_ne_atTop 0] with n hn

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
n : ℕ
hn : n ≠ 0
⊢ (log ↑n - log (b i * ↑n)) / (log (b i * ↑n) * log ↑n) =
    (log ↑n - log (b i) - log ↑n) / ((log (b i) + log ↑n) * log ↑n)
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
⊢ (fun n ↦ ↑n ^ (p a b - 1) * (↑n / log ↑n ^ 2)) =ᶠ[atTop] fun n ↦ ↑n ^ p a b / log ↑n ^ 2

Tactic:
filter_upwards [eventually_ne_atTop 0] with n hn

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
q : ℝ → ℝ := fun x ↦ x ^ p a b * (1 + ε x)
h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)
h_deriv_q : deriv q =O[atTop] fun x ↦ x ^ (p a b - 1)
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (p a b - 1) * (↑n / log ↑n ^ 2) = ↑n ^ p a b / log ↑n ^ 2
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l : Language α
⊢ l∗ = {x | ∃ S, x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []}

Tactic:
ext x

Goal state after:
α : Type u_1
l : Language α
x : List α
⊢ x ∈ l∗ ↔ x ∈ {x | ∃ S, x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []}
Module: Mathlib.Computability.Language

Goal state before:
pp: α : Type u_1
l : Language α
⊢ l∗ = ⨆ i, l ^ i

Tactic:
ext x

Goal state after:
α : Type u_1
l : Language α
x : List α
⊢ x ∈ l∗ ↔ x ∈ ⨆ i, l ^ i