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

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet w)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
⊢ G.neighborFinset w = {v ∈ s | G.Adj v w}

Tactic:
ext v
  rw [mem_neighborFinset, adj_comm, mem_filter, iff_and_self]
  exact h.mem_of_mem_adj' hw

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk✝ : k ≠ 0
h : G.IsEdgeReachable (k + 1) u v
e : Sym2 V
s : Set (Sym2 V)
hk : s.encard < ↑k
⊢ (s ∪ {e}).encard < ↑(k + 1)

Tactic:
grw [Set.encard_union_le, Set.encard_singleton]

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk✝ : k ≠ 0
h : G.IsEdgeReachable (k + 1) u v
e : Sym2 V
s : Set (Sym2 V)
hk : s.encard < ↑k
⊢ s.encard + 1 < ↑(k + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
⊢ (_root_.completeBipartiteGraph α β).Copy G

Tactic:
have : Nonempty (β ↪ right) := by
    rw [← card_coe] at card_right
    exact Function.Embedding.nonempty_of_card_le card_right.symm.le

Goal state after:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
⊢ (_root_.completeBipartiteGraph α β).Copy G
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.Connected ↔ H.Preconnected ∧ H.verts.Nonempty

Tactic:
rw [H.connected_iff', connected_iff, H.preconnected_iff, Set.nonempty_coe_sort]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Preconnected
hK : K.Preconnected
hn : (H ⊓ K).verts.Nonempty
⊢ (H ⊔ K).Connected

Tactic:
Subgraph.connected_iff',

Goal state after:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Preconnected
hK : K.Preconnected
hn : (H ⊓ K).verts.Nonempty
⊢ (H ⊔ K).coe.Connected
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inr
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isRight = true
hs₂ : s₂.isLeft = true
⊢ G.Adj (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) s₁) (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) s₂)

Tactic:
rw [← Sum.inr_getRight s₁ hs₁, ← Sum.inl_getLeft s₂ hs₂,
      Sum.elim_inl, Sum.elim_inr, adj_comm]
    exact h (by simp) (by simp)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ w.toSubgraph.IsInduced ↔ w.IsChordless

Tactic:
simp_rw [Subgraph.IsInduced, IsChordless, IsChord, Sym2.forall, Sym2.lift_mk, G.mem_edgeSet,
    mem_verts_toSubgraph, adj_toSubgraph_iff_mem_edges]
  grind only

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

Goal state before:
pp: case refine_4
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
w : V
hw : w ∈ G.commonNeighbors u v
⊢ G.edist u v ≤ 2

Tactic:
rw [mem_commonNeighbors] at hw

Goal state after:
case refine_4
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
w : V
hw : G.Adj u w ∧ G.Adj v w
⊢ G.edist u v ≤ 2
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ μ b * (f b * g a) ≤ μ (a ⊔ b) * (f (a ⊓ b) * g (a ⊔ b))

Tactic:
rw [sup_comm, inf_comm]

Goal state after:
case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ μ b * (f b * g a) ≤ μ (b ⊔ a) * (f (b ⊓ a) * g (b ⊔ a))
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
⊢ ∀ {a b : (V ⊕ W) ⊕ U},
    (G ⊕g (H ⊕g I)).Adj ((Equiv.sumAssoc V W U) a) ((Equiv.sumAssoc V W U) b) ↔ (G ⊕g H ⊕g I).Adj a b

Tactic:
by rintro ((u | u) | u) ((v | v) | v) <;> simp

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i : V
⊢ A.compl i i = 0

Tactic:
simp [compl]

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i j : V
⊢ A.compl i j = 0 ∨ A.compl i j = 1

Tactic:
simp [compl]

Goal state after:
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i j : V
⊢ (¬i = j → A i j = 0 → 1 = 0) ∨ (if i = j then 0 else if A i j = 0 then 1 else 0) = 1
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
inst✝¹ : Zero α
inst✝ : One α
A : Matrix V V α
hA : A.IsAdjMatrix
i✝ j✝ : V
⊢ A.compl.compl i✝ j✝ = A i✝ j✝

Tactic:
simp [compl]

Goal state after:
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
inst✝¹ : Zero α
inst✝ : One α
A : Matrix V V α
hA : A.IsAdjMatrix
i✝ j✝ : V
⊢ (if i✝ = j✝ then 0 else if ¬i✝ = j✝ → A i✝ j✝ = 0 → 1 = 0 then 1 else 0) = A i✝ j✝
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

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

Tactic:
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'

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

Goal state before:
pp: n r : ℕ
⊢ (∀ (x x_1 : Fin n), ↑x % r ≠ ↑x_1 % r ↔ x ≠ x_1) ↔ r = 0 ∨ n ≤ r

Tactic:
not_iff_not

Goal state after:
n r : ℕ
⊢ (∀ (x x_1 : Fin n), ↑x % r = ↑x_1 % r ↔ x = x_1) ↔ r = 0 ∨ n ≤ r
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∉ p.support
hv : v ∈ q.support
⊢ p.length ≠ q.length

Tactic:
rw [hG.path_concat hp hq hadj hv, p.length_concat]

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
hadj : G.Adj v w
hreach : G.Reachable u v
p : G.Walk u v
hp : p.IsPath
hp' : p.length = G.dist u v
q : G.Walk u w
hq : q.IsPath
hq' : q.length = G.dist u w
hw : w ∉ p.support
hv : v ∈ q.support
⊢ p.length ≠ p.length + 1
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u : α
⊢ 0 < G.eccent u ↔ Nontrivial α

Tactic:
pos_iff_ne_zero,

Goal state after:
α : Type u_1
G : SimpleGraph α
u : α
⊢ G.eccent u ≠ 0 ↔ Nontrivial α
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
u v : α
huv : ⊤.Adj u v
⊢ 0 < G.edist u v

Tactic:
pos_iff_ne_zero,

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
h : ∀ (u : α), G.eccent u = 1
u v : α
huv : ⊤.Adj u v
⊢ G.edist u v ≠ 0
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

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

Tactic:
rw [tsub_mul, ← Nat.sub_add_comm]

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

n r : ℕ
⊢ (n % r) ^ 2 * (r - 1) ≤ n ^ 2 * (r - 1)
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:
grw [w.length_cycleBypass_le_length]

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
⊢ ↑w.length < G.egirth
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Infinite
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
have := h.to_subtype

Goal state after:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case inl.inl
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v : α
t : Finset α
C : G.Coloring (Fin (r + 1))
x : α
hcx : C x = C v
y : α
hcy : C y = C v
h : Set.SurjOn (⇑C) (insert x ↑s) Set.univ
this : Set.SurjOn (⇑C) (insert y ↑t) Set.univ
hw : G.IsFiveWheelLike r k v x y s t
⊢ False

Tactic:
exact C.valid hw.isPathGraph3Compl.adj (hcy ▸ hcx)

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✝ : Subsingleton α
v : α
⊢ List.count v p.support = 1

Tactic:
nil_iff_support_eq.mp p.nil_of_subsingleton,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Subsingleton α
v : α
⊢ List.count v [a] = 1
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 α
h : e ∉ G.incidenceSet a
⊢ (G.incidenceSet a).indicator 1 e = 0

Tactic:
Set.indicator_of_notMem h

Goal state after:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : MulZeroOneClass R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
e : Sym2 α
h : e ∉ G.incidenceSet a
⊢ 0 = 0
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
i j : V
| if G.Adj i j then x i * x i - x i * x j else 0

Tactic:
rw [if_congr (adj_comm G i j) rfl rfl]

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
i j : V
| if G.Adj j i then x i * x i - x i * x j else 0
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hv : (p.toSubgraph.spanningCoe.neighborSet v).Nonempty
⊢ v ∈ p.support

Tactic:
obtain ⟨_, hw⟩ := hv

Goal state after:
V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v w✝ : V
hw : w✝ ∈ p.toSubgraph.spanningCoe.neighborSet v
⊢ v ∈ p.support
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
⊢ (fun i ↦ if G.connectedComponentMk i = c then 1 else 0) ∈ (toLin' (lapMatrix ℝ G)).ker

Tactic:
rw [LinearMap.mem_ker, toLin'_apply, lapMatrix_mulVec_eq_zero_iff_forall_reachable]

Goal state after:
V : Type u_1
inst✝³ : Fintype V
inst✝² : DecidableEq V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq G.ConnectedComponent
c : G.ConnectedComponent
⊢ ∀ (i j : V),
    G.Reachable i j → (if G.connectedComponentMk i = c then 1 else 0) = if G.connectedComponentMk j = c then 1 else 0
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
g : G.ConnectedComponent → ℝ
h0 : ↑(∑ i, g i • G.lapMatrix_ker_basis_aux i) = ↑0
i : V
⊢ (∑ i, ↑⟨g i • fun i_1 ↦ if G.connectedComponentMk i_1 = i then 1 else 0, ⋯⟩) i = g (G.connectedComponentMk i)

Tactic:
simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, mul_ite, mul_one, mul_zero, sum_ite_eq,
      mem_univ, ↓reduceIte]

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

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

Tactic:
rintro ⟨C⟩
    refine ⟨C.toPartition, C.colorClasses_finite, le_trans ?_ (Fintype.card_fin n).le⟩
    generalize_proofs h
    change Set.Finite (Coloring.colorClasses C) at h
    have : Fintype C.colorClasses := C.colorClasses_finite.fintype
    rw [h.card_toFinset]
    exact C.card_colorClasses_le

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

Goal state before:
pp: V : Type u_1
r x y : V
⊢ (starGraph r).Adj x y ↔ x ≠ y ∧ (x = r ∨ y = r)

Tactic:
by
  simp [starGraph, fromRel]

Goal state after:
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) - 1) + #Xᶜᶜ * (#(s ∩ t) - 0)
⊢ G.minDegree ≤ (2 * r + k) * ‖α‖ / (2 * r + k + 3)

Tactic:
compl_compl,

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) - 1) + #X * (#(s ∩ t) - 0)
⊢ G.minDegree ≤ (2 * r + k) * ‖α‖ / (2 * r + k + 3)
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: 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
⊢ (Subtype.val '' ?m.40).ncard ≤ (universalVerts ?m.39).ncard

Tactic:
simp only [IsTutteViolator, not_lt] at h
        rwa [Set.ncard_image_of_injective _ Subtype.val_injective, hrep.ncard_eq]

Goal state after:
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: m : ℕ
⊢ ppred 0 = some m ↔ m.succ = 0

Tactic:
by constructor <;> intro h <;> contradiction

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

Goal state before:
pp: n : ℕ
⊢ Nat.rec [] (fun n IH ↦ IH ++ [n]) n = List.range n

Tactic:
induction n

Goal state after:
case zero
⊢ Nat.rec [] (fun n IH ↦ IH ++ [n]) 0 = List.range 0

case succ
n✝ : ℕ
a✝ : Nat.rec [] (fun n IH ↦ IH ++ [n]) n✝ = List.range n✝
⊢ Nat.rec [] (fun n IH ↦ IH ++ [n]) (n✝ + 1) = List.range (n✝ + 1)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case comp
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Nat.Partrec ↑f✝
pg : Nat.Partrec ↑g✝
⊢ Nat.Partrec ↑fun n ↦ f✝ (g✝ n)

Tactic:
refine (pf.comp pg).of_eq_tot fun n => (by simp)

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case prec
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Nat.Partrec ↑f✝
pg : Nat.Partrec ↑g✝
⊢ Nat.Partrec ↑(unpaired fun z n ↦ Nat.rec (f✝ z) (fun y IH ↦ g✝ (Nat.pair z (Nat.pair y IH))) n)

Tactic:
| prec _ _ pf pg =>

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

Goal state before:
pp: β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b : β
i : ℕ
hi : i ≤ m b + 1
⊢ graph b i = List.map (fun x ↦ (x, f x)) (bindList b (m b + 1 - i))

Tactic:
have bindList_eq_nil : bindList b (m b + 1) = [] :=
        have bindList_m_lt (k : ℕ) : ∀ b' ∈ bindList b k, m b' < m b + 1 - k := by
          induction k with simp [bindList]
          | succ k ih =>
            grind
        List.eq_nil_iff_forall_not_mem.mpr
          (by intro b' ha'; by_contra; simpa using bindList_m_lt (m b + 1) b' ha')

Goal state after:
β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b : β
i : ℕ
hi : i ≤ m b + 1
bindList_eq_nil : bindList b (m b + 1) = []
⊢ graph b i = List.map (fun x ↦ (x, f x)) (bindList b (m b + 1 - i))
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝² : Primcodable α
inst✝¹ : Primcodable β
hf : PrimrecRel R
inst✝ : DecidableRel R
⊢ Primrec₂ fun L b ↦ filter (fun a ↦ decide (R a b)) L

Tactic:
simp only [← List.filterMap_eq_filter]

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝² : Primcodable α
inst✝¹ : Primcodable β
hf : PrimrecRel R
inst✝ : DecidableRel R
⊢ Primrec₂ fun L b ↦ filterMap (Option.guard fun a ↦ decide (R a b)) L
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case comp
f f✝ g✝ : ℕ → ℕ
hf : Nat.Primrec f✝
hg : Nat.Primrec g✝
IHf : ∃ m, ∀ (n : ℕ), f✝ n < ack m n
IHg : ∃ m, ∀ (n : ℕ), g✝ n < ack m n
⊢ ∃ m, ∀ (n : ℕ), (fun n ↦ f✝ (g✝ n)) n < ack m n

Tactic:
obtain ⟨a, ha⟩ := IHf; obtain ⟨b, hb⟩ := IHg
    exact
      ⟨max a b + 2, fun n =>
        (ha _).trans <| (ack_strictMono_right a <| hb n).trans <| ack_ack_lt_ack_max_add_two a b n⟩

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: this : Primrec fun t ↦ Nat.rec succ (fun x c ↦ pappAck.step c) t
n : ℕ
⊢ pappAck n = Nat.rec succ (fun x c ↦ pappAck.step c) n

Tactic:
induction n

Goal state after:
case zero
this : Primrec fun t ↦ Nat.rec succ (fun x c ↦ pappAck.step c) t
⊢ pappAck 0 = Nat.rec succ (fun x c ↦ pappAck.step c) 0

case succ
this : Primrec fun t ↦ Nat.rec succ (fun x c ↦ pappAck.step c) t
n✝ : ℕ
a✝ : pappAck n✝ = Nat.rec succ (fun x c ↦ pappAck.step c) n✝
⊢ pappAck (n✝ + 1) = Nat.rec succ (fun x c ↦ pappAck.step c) (n✝ + 1)
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
⊢ z ≤ 2 ^ (-↑k - 1) * x₀

Tactic:
have := hz.2
        simp only [neg_add, ← sub_eq_add_neg] at this
        exact this

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

Goal state before:
pp: c : ℝ
hc : c < 1
h₁ : Tendsto (fun x ↦ 1 - ε x) atTop (𝓝 1)
⊢ ∀ᶠ (x : ℝ) in atTop, c < 1 - ε x

Tactic:
rw [tendsto_order] at h₁

Goal state after:
c : ℝ
hc : c < 1
h₁ : (∀ a' < 1, ∀ᶠ (b : ℝ) in atTop, a' < 1 - ε b) ∧ ∀ a' > 1, ∀ᶠ (b : ℝ) in atTop, 1 - ε b < a'
⊢ ∀ᶠ (x : ℝ) in atTop, c < 1 - ε x
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x ↦ |f x|

Tactic:
| inl hf' =>

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

Goal state before:
pp: case inl
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun x ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x ↦ f x * g x

Tactic:
| inl hf' =>

Goal state after: