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

Goal state before:
pp: case e_a.e_a
n r : ℕ
⊢ (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = #(range r) * (r - 1)

Tactic:
← smul_eq_mul,

Goal state after:
case e_a.e_a
n r : ℕ
⊢ (∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) = #(range r) • (r - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
u : α
hu : u ∈ Set.univ
⊢ G.eccent u = G.radius

Tactic:
h u

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
u : α
hu : u ∈ Set.univ
⊢ e = G.radius
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

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

Tactic:
simp_rw [h_bot (r + 1), ht, Finset.card_eq_zero, exists_eq_left, IsCompleteBetween, mem_coe,
      notMem_empty, IsEmpty.forall_iff, implies_true, exists_true_iff_nonempty]

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
this : ∀ (r' : ℕ), IsEmpty (Fin r' × Fin t)
h_bot : ∀ (r' : ℕ), completeEquipartiteGraph r' t = ⊥
⊢ ⊥ ⊑ G ↔ Nonempty (G.CompleteEquipartiteSubgraph r t)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_1
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
K : G.CompleteEquipartiteSubgraph r t :=
  { parts := parts, card_parts := ⋯, card_mem_parts := ⋯, isCompleteBetween := ⋯ }
s : Finset V
nhs_mem : s ∉ K.parts
hs : insert s K.parts = K'.parts
⊢ ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s

Tactic:
have hs_mem : s ∈ K'.parts := by simp [← hs]

Goal state after:
case neg.refine_1
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
K : G.CompleteEquipartiteSubgraph r t :=
  { parts := parts, card_parts := ⋯, card_mem_parts := ⋯, isCompleteBetween := ⋯ }
s : Finset V
nhs_mem : s ∉ K.parts
hs : insert s K.parts = K'.parts
hs_mem : s ∈ K'.parts
⊢ ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: case hn
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
e : Sym2 (Fin (n + 1))
he : e ∈ G.edgeFinset
⊢ n - 1 ≤ ↑(#(bipartiteBelow (fun v e ↦ v ∉ e) univ e))

Tactic:
← Sym2.mem_toFinset,

Goal state after:
case hn
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
e : Sym2 (Fin (n + 1))
he : e ∈ G.edgeFinset
⊢ n - 1 ≤ ↑(#(bipartiteBelow (fun v e ↦ v ∉ e.toFinset) univ e))
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
| #(K.parts \ {p}) * t'

Tactic:
← smul_eq_mul,

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
| #(K.parts \ {p}) • t'
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 b : α
e : Sym2 α
⊢ incMatrix R G a e * incMatrix R G b e = (G.incidenceSet a ∩ G.incidenceSet b).indicator 1 e

Tactic:
by
  simp [incMatrix_apply', Set.indicator_apply, ← ite_and, and_comm]

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
v : V
⊢ v ∈ (Subgraph.map (Hom.ofLE h) x).verts

Tactic:
simp only [Subgraph.map_verts, Hom.coe_ofLE, id_eq, Set.image_id']

Goal state after:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
v : V
⊢ v ∈ x.verts
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
hr_eq_1 : r = 1
h0 : r ≤ 1 ∨ t' = 0
⊢ ↑(t'.choose t) ^ r * ↑t + ↑r * ↑t' ≤ (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)

Tactic:
mul_div_assoc,

Goal state after:
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
ih :
  ∀ (b : ℕ),
    N' ≤ b →
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        ↑G.minDegree ≥ (1 - 1 / ↑(r - 1) + ε') * ↑b → completeEquipartiteGraph (r - 1 + 1) t' ⊑ G
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
hr_eq_1 : r = 1
h0 : r ≤ 1 ∨ t' = 0
⊢ ↑(t'.choose t) ^ r * ↑t + ↑r * ↑t' ≤ (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * ((↑t' - ↑t) / (↑r * ↑t' * ε - ↑t))
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
⊢ Fintype.card G.ConnectedComponent = finrank ℝ ↥(toLin' (lapMatrix ℝ G)).ker

Tactic:
rw [Module.finrank_eq_card_basis G.lapMatrix_ker_basis]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
⊢ P.partOfVertex v ≠ P.partOfVertex w

Tactic:
intro hn

Goal state after:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
hn : P.partOfVertex v = P.partOfVertex w
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Partition

Goal state before:
pp: V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
hn : P.partOfVertex v = P.partOfVertex w
hw : w ∈ P.partOfVertex w
⊢ False

Tactic:
rw [← hn] at hw

Goal state after:
V : Type u
G : SimpleGraph V
P : G.Partition
v w : V
h : G.Adj v w
hn : P.partOfVertex v = P.partOfVertex w
hw : w ∈ P.partOfVertex v
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
inst✝ : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
⊢ (G.deleteEdges {s(v, w)}).Reachable v w

Tactic:
by
  have : fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe := by
    simp only [Walk.toSubgraph, singletonSubgraph_le_iff, subgraphOfAdj_verts, Set.mem_insert_iff,
      Set.mem_singleton_iff, or_true, sup_of_le_left]
    exact (Subgraph.spanningCoe_subgraphOfAdj hadj).symm
  rw [show G.deleteEdges {s(v, w)} = G \ fromEdgeSet {s(v, w)} by rfl]
  exact this ▸ (hcyc.reachable_sdiff_toSubgraph_spanningCoe hadj.toWalk
    (Walk.IsPath.of_adj hadj)).symm

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
c' : G.ConnectedComponent
hc' : p.toSubgraph.verts = c'.supp
⊢ v ∈ p.support

Tactic:
exact hvp

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

Goal state before:
pp: V : Type u_1
a✝ : Nontrivial V
n : ℕ
hn : ↑n ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < ↑n
this✝ : ↑n - 1 ≤ ENat.card V
t : Set V
ht₁ : t.encard = ↑(n - 1)
ht₂ : (completeGraph V).IsVertexCover t
this : 1 < (Set.univ \ t).encard
a b : V
left✝¹ : a ∈ Set.univ \ t
left✝ : b ∈ Set.univ \ t
hne : a ≠ b
⊢ (completeGraph V).Adj a b

Tactic:
simp [hne]

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
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
⊢ G.CompleteEquipartiteSubgraph r t

Tactic:
by
      refine ⟨univ.map ⟨fun p : K.parts ↦ y p.val p.prop, fun p₁ p₂ (heq : y p₁ _ = y p₂ _) ↦ ?_⟩,
        ?_, fun {p} hp ↦ ?_, fun p₁ hp₁ p₂ hp₂ hne v₁ hv₁ v₂ hv₂ ↦ ?_⟩
      · have hy₁' := mem_powersetCard.mp (hy p₁.val p₁.prop)
        have hy₂' := mem_powersetCard.mp (hy p₂.val p₂.prop)
        rw [← heq] at hy₂'
        obtain ⟨v, hv⟩ : (y p₁ _).Nonempty := by
          rw [← Finset.card_pos, hy₁'.right]
          exact ht_pos
        by_contra! hne
        absurd K.isCompleteBetween p₁.prop p₂.prop
          (Subtype.ext_iff.ne.mp hne) (hy₁'.left hv) (hy₂'.left hv)
        exact G.loopless.irrefl v
      · simp_rw [card_map, card_univ, card_coe]
        exact .inl (K.card_parts.resolve_right ht'_pos.ne')
      · simp_rw [univ_eq_attach, Finset.mem_map, mem_attach,
          Function.Embedding.coeFn_mk, true_and, Subtype.exists] at hp
        replace ⟨p, hp, hyp⟩ := hp
        rw [← hyp]
        have hy' := mem_powersetCard.mp (hy p hp)
        exact hy'.right
      · simp_rw [univ_eq_attach, coe_map, Function.Embedding.coeFn_mk,
          Set.mem_image, mem_coe, mem_attach, true_and, Subtype.exists] at hp₁ hp₂
        replace ⟨p₁, hp₁, hyp₁⟩ := hp₁
        rw [← hyp₁] at hv₁ hne
        have hy₁' := mem_powersetCard.mp (hy p₁ hp₁)
        replace ⟨p₂, hp₂, hyp₂⟩ := hp₂
        rw [← hyp₂] at hv₂ hne
        have hy₂' := mem_powersetCard.mp (hy p₂ hp₂)
        refine K.isCompleteBetween hp₁ hp₂ ?_ (hy₁'.left hv₁) (hy₂'.left hv₂)
        by_contra! heq
        simp [← heq] at hne

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
M : G.Subgraph
hM : M.IsPerfectMatching
u : Set V
f : ↑(⊤.deleteVerts u).coe.oddComponents → V
hf : ∀ (c : ↑(⊤.deleteVerts u).coe.oddComponents), f c ∈ u
g : ↑(⊤.deleteVerts u).coe.oddComponents → ↑(⊤.deleteVerts u).verts
hgf : ∀ (c : ↑(⊤.deleteVerts u).coe.oddComponents), M.Adj (↑(g c)) (f c)
hg : ∀ (c : ↑(⊤.deleteVerts u).coe.oddComponents), g c ∈ (↑c).supp
c d : ↑(⊤.deleteVerts u).coe.oddComponents
hcd : f c = f d
⊢ c = d

Tactic:
replace hcd : g c = g d := Subtype.val_injective <| hM.1.eq_of_adj_right (hgf c) (hcd ▸ hgf d)

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
M : G.Subgraph
hM : M.IsPerfectMatching
u : Set V
f : ↑(⊤.deleteVerts u).coe.oddComponents → V
hf : ∀ (c : ↑(⊤.deleteVerts u).coe.oddComponents), f c ∈ u
g : ↑(⊤.deleteVerts u).coe.oddComponents → ↑(⊤.deleteVerts u).verts
hgf : ∀ (c : ↑(⊤.deleteVerts u).coe.oddComponents), M.Adj (↑(g c)) (f c)
hg : ∀ (c : ↑(⊤.deleteVerts u).coe.oddComponents), g c ∈ (↑c).supp
c d : ↑(⊤.deleteVerts u).coe.oddComponents
hcd : g c = g d
⊢ c = d
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: m n : ℕ
⊢ m.psub' n = m.psub n

Tactic:
by
  rw [psub']
  split_ifs with h
  · exact (psub_eq_sub h).symm
  · exact (psub_eq_none.2 (not_le.1 h)).symm

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case false
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
pm : (p m).Dom
e : (p m).get pm = false
⊢ { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }

pp: case true
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
pm : (p m).Dom
e : (p m).get pm = true
⊢ { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }

Tactic:
· suffices ∀ᵉ k ≤ m, false ∈ p k from IH _ ⟨rfl, this⟩ fun n h => this _ (le_of_lt_succ h)
        intro n h
        rcases h.lt_or_eq_dec with h | h
        · exact al _ h
        · rw [h]
          exact ⟨_, e⟩

Goal state after:
case true
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
pm : (p m).Dom
e : (p m).get pm = true
⊢ { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
⊢ ack 3 n = 2 ^ (n + 3) - 3

Tactic:
by
  induction n with
  | zero => simp
  | succ n IH =>
    rw [ack_succ_succ, IH, ack_two, Nat.succ_add, Nat.pow_succ 2 (n + 3), mul_comm _ 2,
        Nat.mul_sub_left_distrib, ← Nat.sub_add_comm, two_mul 3, Nat.add_sub_add_right]
    calc 2 * 3
      _ ≤ 2 * 2 ^ 3 := by simp
      _ ≤ 2 * 2 ^ (n + 3) := by gcongr <;> lia

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: c : Code
⊢ ofNatCode c.encodeCode = c

Tactic:
induction c <;> simp [encodeCode, ofNatCode, Nat.div2_val, *]

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

Goal state before:
pp: case neg.inr
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ 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' : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
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 x'
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x' x
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ {x'_1 : V}, x'_1 ∈ {x, x'} → ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x'_1 → M2.Adj c' x'_1
⊢ ∃ G', G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x' x ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c

Tactic:
exact tutte_exists_isAlternating_isCycles p hp hcalt (hnM2 _ hnbc) hpac hnpxb hM2ac
      hab.symm hnbc hxa.ne.symm hle (aux (by simp))

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: ⊢ ¬Primrec fun n ↦ ack n n

Tactic:
by
  rw [Primrec.nat_iff]
  exact not_nat_primrec_ack_self

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc✝ : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x✝ y : ↑K.supp
hxy : x✝ ≠ y ∧ ¬Gmax.deleteUniversalVerts.coe.Adj ↑x✝ ↑y
p : K.toSimpleGraph.Walk x✝ y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x✝ y
x a b : ↥K
hnxb : x ≠ b
hxa : Gmax.Adj ↑↑x ↑↑a
hxb : Gmax.Adj ↑↑a ↑↑b
hnadjxb : ¬Gmax.Adj ↑↑x ↑↑b
c : V
hc : ↑↑a ≠ c ∧ ¬Gmax.Adj (↑↑a) c
hbnec : ↑↑b ≠ c
w✝ : (Gmax ⊔ edge ↑↑x ↑↑b).Subgraph
hG1 : w✝.IsPerfectMatching
⊢ ¬?m.343 ≤ Gmax

Tactic:
edge_le_iff (v := a.1.1) (w := c),

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val✝ : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ M, M.IsPerfectMatching
hc✝ : ¬Fintype.card ↑Gmax.universalVerts < Fintype.card ↑(⊤.deleteVerts Gmax.universalVerts).coe.oddComponents
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x✝ y : ↑K.supp
hxy : x✝ ≠ y ∧ ¬Gmax.deleteUniversalVerts.coe.Adj ↑x✝ ↑y
p : K.toSimpleGraph.Walk x✝ y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x✝ y
x a b : ↥K
hnxb : x ≠ b
hxa : Gmax.Adj ↑↑x ↑↑a
hxb : Gmax.Adj ↑↑a ↑↑b
hnadjxb : ¬Gmax.Adj ↑↑x ↑↑b
c : V
hc : ↑↑a ≠ c ∧ ¬Gmax.Adj (↑↑a) c
hbnec : ↑↑b ≠ c
w✝ : (Gmax ⊔ edge ↑↑x ↑↑b).Subgraph
hG1 : w✝.IsPerfectMatching
⊢ ¬(↑↑a = c ∨ Gmax.Adj (↑↑a) c)
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)
⊢ (fun x ↦ deriv (fun z ↦ z ^ p a b) x * (1 - ε x) + x ^ p a b * deriv (fun z ↦ 1 - ε z) x) =O[atTop] fun x ↦
    x ^ (p a b - 1)

Tactic:
refine IsBigO.add ?left ?right

Goal state after:
case left
α : 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)
⊢ (fun x ↦ deriv (fun z ↦ z ^ p a b) x * (1 - ε x)) =O[atTop] fun x ↦ x ^ (p a b - 1)

case right
α : 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)
⊢ (fun x ↦ x ^ p a b * deriv (fun z ↦ 1 - ε z) x) =O[atTop] fun x ↦ x ^ (p a b - 1)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
⊢ 0 ≤ f x

Tactic:
have hu := hx (3 / 4 * x) h'

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ 0 ≤ f x
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
⊢ f x ≤ 0

Tactic:
have hu := hx (3 / 4 * x) h'

Goal state after:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ f x ≤ 0
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)
⊢ (fun x ↦ deriv (fun z ↦ z ^ p a b) x * (1 + ε x) + x ^ p a b * deriv (fun z ↦ 1 + ε z) x) =O[atTop] fun x ↦
    x ^ (p a b - 1)

Tactic:
refine IsBigO.add ?left ?right

Goal state after:
case left
α : 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)
⊢ (fun x ↦ deriv (fun z ↦ z ^ p a b) x * (1 + ε x)) =O[atTop] fun x ↦ x ^ (p a b - 1)

case right
α : 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)
⊢ (fun x ↦ x ^ p a b * deriv (fun z ↦ 1 + ε z) x) =O[atTop] fun x ↦ x ^ (p a b - 1)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

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

Tactic:
rwa [iff_eventuallyEq hmain]

Goal state after: