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

Goal state before:
pp: α : Type u_1
β : Type u_2
V : Type u_3
inst✝ : DecidableEq V
G : SimpleGraph V
u v : V
w : G.Walk u v
hw : w.IsPath
⊢ ∀ {a b : Fin (w.length + 1)},
    w.toSubgraph.coe.Adj
        ({ toFun := ⇑w.pathGraphHomToSubgraph, invFun := fun v_1 ↦ ⟨List.idxOf (↑v_1) w.support, ⋯⟩, left_inv := ⋯,
            right_inv := ⋯ }
          a)
        ({ toFun := ⇑w.pathGraphHomToSubgraph, invFun := fun v_1 ↦ ⟨List.idxOf (↑v_1) w.support, ⋯⟩, left_inv := ⋯,
            right_inv := ⋯ }
          b) ↔
      (pathGraph (w.length + 1)).Adj a b

Tactic:
refine ⟨fun hadj ↦ ?_, w.pathGraphHomToSubgraph.map_rel'⟩
    grind [w.toSubgraph_adj_iff.mp hadj, pathGraph_adj, getVert_eq_getD_support,
      pathGraphHomToSubgraph, RelHom.coeFn_mk, hw.support_nodup.getElem_inj_iff]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
v : V
p : G.Walk v v
hp : p.IsCycle
this✝ : 3 ≤ p.length
this : p.support.tail.length ≤ 2
⊢ False

Tactic:
List.length_tail,

Goal state after:
V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
v : V
p : G.Walk v v
hp : p.IsCycle
this✝ : 3 ≤ p.length
this : p.support.length - 1 ≤ 2
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
⊢ (adjMatrix α G).diag = 0

Tactic:
by
  simp

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

Goal state before:
pp: V : Type u_1
G F : SimpleGraph V
h : Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
x✝ : G.Reachable u v
p : G.Walk u v
this✝² : ¬F.Reachable u v
s : F.ConnectedComponent := Quot.mk F.Reachable u
this✝¹ : v ∉ s
u' v' : V
huv : G.Adj (u', v').1 (u', v').2
left✝ : { fst := u', snd := v', adj := huv } ∈ p.darts
hu : { fst := u', snd := v', adj := huv }.toProd.1 ∈ s
hv : { fst := u', snd := v', adj := huv }.toProd.2 ∉ s
this✝ : ¬F.Reachable v' u'
this : F ⊔ edge v' u' ≤ F
⊢ False

Tactic:
grind [Adj.reachable, sup_le_iff, le_iff_adj]

Goal state after:
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
i✝ j✝ : K
h : i✝ ≠ j✝
⊢ Disjoint (C.labelGraph i✝) (C.labelGraph j✝)

Tactic:
rw [disjoint_left]

Goal state after:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
i✝ j✝ : K
h : i✝ ≠ j✝
⊢ ∀ (x y : V), (C.labelGraph i✝).Adj x y → ¬(C.labelGraph j✝).Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd #{x | Odd x.supp.ncard} ↔ Odd (∑ x, x.supp.ncard)

Tactic:
exact (Finset.odd_sum_iff_odd_card_odd (fun x : G.ConnectedComponent ↦ x.supp.ncard)).symm

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

Goal state before:
pp: r t : ℕ
⊢ r * t * (r - 1) * t = r * (r - 1) * t ^ 2

Tactic:
mul_comm r _,

Goal state after:
r t : ℕ
⊢ t * r * (r - 1) * t = r * (r - 1) * t ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
u : α
⊢ G.eccent u ≠ 0

Tactic:
obtain ⟨v, huv⟩ := exists_ne ‹_›
  contrapose huv
  simp only [eccent, ENat.iSup_eq_zero, edist_eq_zero_iff] at huv
  exact (huv v).symm

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

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
h✝ : Nonempty α
hdiam : ¬G.ediam = ⊤
w : α
hw : G.eccent w = G.radius
w✝¹ w✝ : α
h : G.edist w✝¹ w✝ = G.ediam
⊢ G.edist w✝¹ w + G.edist w w✝ ≤ 2 * G.radius

Tactic:
two_mul

Goal state after:
case neg
α : Type u_1
G : SimpleGraph α
h✝ : Nonempty α
hdiam : ¬G.ediam = ⊤
w : α
hw : G.eccent w = G.radius
w✝¹ w✝ : α
h : G.edist w✝¹ w✝ = G.ediam
⊢ G.edist w✝¹ w + G.edist w w✝ ≤ G.radius + G.radius
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
sec : s ∈ G.end
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : v ∉ Opposite.unop L
hs : s L = G.componentComplMk vnL
⊢ s K = G.componentComplMk ⋯

Tactic:
rw [← sec h, hs]

Goal state after:
V : Type u
G : SimpleGraph V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
sec : s ∈ G.end
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : v ∉ Opposite.unop L
hs : s L = G.componentComplMk vnL
⊢ (ConcreteCategory.hom (G.componentComplFunctor.map h)) (G.componentComplMk vnL) = G.componentComplMk ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
ι : Sort u_1
f : ι → G.Finsubgraph
⊢ ⨅ G_1 ∈ range fun i ↦ f i, ↑G_1 = ⨅ i, ↑(f i)

Tactic:
iInf_range

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
ι : Sort u_1
f : ι → G.Finsubgraph
⊢ ⨅ i, ↑(f i) = ⨅ i, ↑(f i)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case h₂
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
v : Fin n
hv : v ∈ filter K t
⊢ ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) ≤ ↑(#K.verts)

Tactic:
· exact_mod_cast isBipartiteWith_degree_le'
            (between_verts_isBipartiteWith K) (filter_subset_compl_verts K hv)

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 ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : ↑p₁ → V
hf₁ : Injective f
hf₂ : ∀ (x : ↑p₁), f x ∈ G.neighborFinset ↑x
⊢ ∃ M, p₁ ⊆ M.verts ∧ M.IsMatching

Tactic:
have (x : p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ x.2 <| Set.mem_toFinset.mp <| hf₂ x

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : ↑p₁ → V
hf₁ : Injective f
hf₂ : ∀ (x : ↑p₁), f x ∈ G.neighborFinset ↑x
this : ∀ (x : ↑p₁), f x ∉ p₁
⊢ ∃ M, p₁ ⊆ M.verts ∧ M.IsMatching
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 ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
⊢ ∃ M, p₁ ⊆ M.verts ∧ M.IsMatching

Tactic:
obtain ⟨f, hf₁, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun (x : p₁) ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ (s.image Subtype.val) (by simp)
    rw [Set.ncard_coe_finset, Finset.card_image_of_injective _ Subtype.val_injective] at this
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  have (x : p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ x.2 <| Set.mem_toFinset.mp <| hf₂ x
  use hall_subgraph f this (fun v ↦ G.mem_neighborFinset _ _ |>.mp <| hf₂ v)
  refine ⟨by simp, fun v hv ↦ ?_⟩
  simp only [Set.mem_union, Set.mem_range, Subtype.exists] at hv ⊢
  rcases hv with h' | ⟨x, hx₁, hx₂⟩
  · exact ⟨f ⟨v, h'⟩, by simp_all⟩
  · use x
    have := hx₂ ▸ this ⟨x, hx₁⟩
    simp only [this, ↓reduceDIte, hx₁, hx₂, dite_else_false, forall_exists_index, true_and]
    exact fun _ _ k ↦ Subtype.ext_iff.mp <| hf₁ (hx₂ ▸ k)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
⊢ M.IsPerfectMatching ↔ ∀ (v : V), ∃! w, M.Adj v w

Tactic:
refine ⟨?_, fun hm => ⟨fun v _ => hm v, fun v => ?_⟩⟩
  · rintro ⟨hm, hs⟩ v
    exact hm (hs v)
  · obtain ⟨w, hw, -⟩ := hm v
    exact M.edge_vert hw

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

Goal state before:
pp: case refine_2
α : 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 : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
⊢ w₁ ≠ x

pp: case refine_3
α : 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 : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
⊢ w₂ ≠ x

Tactic:
· by_cases hax : x = a <;> rintro rfl
      · grind
      · exact haj <| hw.isNClique_fst_left.1 (mem_insert_self ..) (mem_insert_of_mem has) hax

Goal state after:
case refine_3
α : 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 : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
⊢ w₂ ≠ x
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
⊢ ¬x.IsPerfectMatching

Tactic:
by_contra! hc

Goal state after:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Star

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
r : V
⊢ (starGraph r).degree r = Fintype.card V - 1

Tactic:
by
  simp

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

Goal state before:
pp: case h
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
this : p.toSubgraph.verts = c.supp
⊢ (p.rotate v hvp).IsCycle ∧ (p.rotate v hvp).toSubgraph.verts = p.toSubgraph.verts

Tactic:
exact ⟨hp.1.rotate _, by simp⟩

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)
⊢ G.minDegree ≤ (2 * r + k) * ‖α‖ / (2 * r + k + 3)

Tactic:
let X : Finset α := {x | ∀ ⦃y⦄, y ∈ s ∩ t → G.Adj x y}

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}
⊢ G.minDegree ≤ (2 * r + k) * ‖α‖ / (2 * r + k + 3)
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case a
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
u v : V
⊢ G.edist u v ≤ 2

Tactic:
by_contra! hc

Goal state after:
case a
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : Nontrivial V
h : G.IsSRGWith n k ℓ μ
ht : G ≠ ⊤
hm : μ ≠ 0
u v : V
hc : 2 < G.edist u v
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.inr
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
w'' : V
hw'' : y ≠ w'' ∧ G'.Adj v w''
⊢ y = w'

Tactic:
by_contra! hc

Goal state after:
case h.inr
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
h : G'.Adj v w
w' : V
hw' : w ≠ w' ∧ G'.Adj v w'
hmadj : M.Adj v w ↔ ¬M.Adj v w'
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
w'' : V
hw'' : y ≠ w'' ∧ G'.Adj v w''
hc : y ≠ w'
⊢ False
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₂ ⋯
⊢ p₁ = p₂

Tactic:
have hy₁' := mem_powersetCard.mp (hy p₁.val p₁.prop)

Goal state after:
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
⊢ p₁ = p₂
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
x : ℕ
hx : x ∈ μ.rowLens
⊢ 0 < x

Tactic:
rw [rowLens, List.mem_map] at hx

Goal state after:
μ : YoungDiagram
x : ℕ
hx : ∃ a ∈ List.range (μ.colLen 0), μ.rowLen a = x
⊢ 0 < x
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: case h
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
i✝ : ιₚ
gx✝ : G
⊢ ↑(g • { index := i✝, groupElts := ↑gx✝ }) = g • ↑{ index := i✝, groupElts := ↑gx✝ }

Tactic:
simp [coeSet, mul_smul]

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

Goal state before:
pp: μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
⊢ T i j1 ≤ T i j2

Tactic:
by
  rcases eq_or_lt_of_le hj with h | h
  · rw [h]
  · exact T.row_weak h cell

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × α
o : Option α
a : α
⊢ (Option.casesOn ((fun a x ↦ a) (o, a).1 (o, a).2) ((fun x b ↦ b) (o, a).1 (o, a).2) fun b ↦ b) =
    (o, a).1.getD (o, a).2

Tactic:
by
    cases o <;> rfl

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 : β
graph_eq_map_bindList : ∀ i ≤ m b + 1, graph b i = List.map (fun x ↦ (x, f x)) (bindList b (m b + 1 - i))
⊢ Option.map Prod.snd (graph b (m b + 1))[0]? = some (f b)

Tactic:
simp [graph_eq_map_bindList (m b + 1) (Nat.le_refl _), bindList]

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

Goal state before:
pp: case intro
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
⊢ Gmax.IsTutteViolator Gmax.universalVerts

Tactic:
by_contra! hc

Goal state after:
case intro
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 : ¬Gmax.IsTutteViolator Gmax.universalVerts
⊢ False
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
⊢ 0 < n → 1 < b' * ↑n → ‖q ↑(r i n) - q (b i * ↑n)‖ ≤ c₂ * ‖deriv q ↑n * (↑(r i n) - b i * ↑n)‖

Tactic:
h_n_pos

Goal state after:
α : 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
⊢ 1 < b' * ↑n → ‖q ↑(r i n) - q (b i * ↑n)‖ ≤ c₂ * ‖deriv q ↑n * (↑(r i n) - b i * ↑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)
⊢ (fun x ↦ x ^ p a b * deriv (fun z ↦ 1 - ε z) x) =O[atTop] fun x ↦ x ^ (p a b - 1)

Tactic:
calc (fun x => x ^ (p a b) * deriv (fun z => 1 - ε z) x)
        _ =O[atTop] (fun x => x ^ (p a b) * x⁻¹) :=
          IsBigO.mul (isBigO_refl _ _) isLittleO_deriv_one_sub_smoothingFn.isBigO
        _ =ᶠ[atTop] fun x => x ^ ((p a b) - 1) := by
          filter_upwards [eventually_gt_atTop 0] with x hx
          rw [← Real.rpow_neg_one, ← Real.rpow_add hx, ← sub_eq_add_neg]

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)
⊢ (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
        case left =>
          calc (fun x => deriv (fun z => z ^ (p a b)) x * (1 + ε x))
            _ =O[atTop] fun x => x ^ ((p a b) - 1) * (1 + ε x) :=
              IsBigO.mul (isBigO_deriv_rpow_const_atTop (p a b)) (isBigO_refl _ _)
            _ =O[atTop] fun x => x ^ ((p a b) - 1) * 1 :=
              IsBigO.mul (isBigO_refl _ _) isEquivalent_one_add_smoothingFn_one.isBigO
            _ = fun x => x ^ ((p a b) - 1) := by ext; rw [mul_one]
        case right =>
          calc (fun x => x ^ (p a b) * deriv (fun z => 1 + ε z) x)
            _ =O[atTop] (fun x => x ^ (p a b) * x⁻¹) :=
              IsBigO.mul (isBigO_refl _ _) isLittleO_deriv_one_add_smoothingFn.isBigO
            _ =ᶠ[atTop] fun x => x ^ ((p a b) - 1) := by
              filter_upwards [eventually_gt_atTop 0] with x hx
              rw [← Real.rpow_neg_one, ← Real.rpow_add hx, ← sub_eq_add_neg]

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
⊢ ↑n ^ p a b * ↑n * (c₂ * g ↑n / (c₁ * ↑n) ^ (p a b + 1)) = c₂ * g ↑n * ↑n ^ (p a b + 1) / (c₁ * ↑n) ^ (p a b + 1)

Tactic:
rw [← Real.rpow_add_one (by positivity) (p a b)]; ring

Goal state after: