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

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
⊢ Nonempty (G →g F)

Tactic:
by
  -- Obtain a `Fintype` instance for `W`.
  cases nonempty_fintype W
  -- Establish the required interface instances.
  have : ∀ G' : G.Finsubgraphᵒᵖ, Nonempty ((finsubgraphHomFunctor G F).obj G') := fun G' =>
    ⟨h G'.unop G'.unop.property⟩
  have : ∀ G' : G.Finsubgraphᵒᵖ, Fintype ((finsubgraphHomFunctor G F).obj G') := by
    intro G'
    haveI : Fintype (G'.unop.val.verts : Type u) := G'.unop.property.fintype
    haveI : Fintype (↥G'.unop.val.verts → W) := by classical exact Pi.instFintype
    exact Fintype.ofInjective (fun f => f.toFun) RelHom.coe_fn_injective
  -- Use compactness to obtain a section.
  obtain ⟨u, hu⟩ := nonempty_sections_of_finite_inverse_system (finsubgraphHomFunctor G F)
  refine ⟨⟨fun v => ?_, ?_⟩⟩
  · -- Map each vertex using the homomorphism provided for its singleton subgraph.
    exact
      (u (Opposite.op (singletonFinsubgraph v))).toFun
        ⟨v, by
          unfold singletonFinsubgraph
          simp⟩
  · -- Prove that the above mapping preserves adjacency.
    intro v v' e
    simp only
    /- The homomorphism for each edge's singleton subgraph agrees with those for its source and
        target vertices. -/
    have hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v) :=
      Quiver.Hom.op (CategoryTheory.homOfLE singletonFinsubgraph_le_adj_left)
    have hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v') :=
      Quiver.Hom.op (CategoryTheory.homOfLE singletonFinsubgraph_le_adj_right)
    rw [← hu hv, ← hu hv']
    -- Porting note: was `apply Hom.map_adj`
    apply Hom.map_adj (u _) ?_
    -- `v` and `v'` are definitionally adjacent in `finsubgraphOfAdj e`
    simp [finsubgraphOfAdj]

Goal state after:
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 - 1) * t'

Tactic:
← card_singleton p,

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.Extremal.ErdosStoneSimonovits

Goal state before:
pp: 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'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
| ↑(#K.verts) * ((1 - 1 / ↑r + ε) * ↑n - ↑(#K.verts)) + -(↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t))

Tactic:
neg_sub,

Goal state after:
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'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
N : ℕ
hN : (↑N + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
| ↑(#K.verts) * ((1 - 1 / ↑r + ε) * ↑n - ↑(#K.verts)) + (↑(#K.verts) - ↑n) * (↑(#K.verts) - (↑t' - ↑t))
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: case h.isFalse
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
b : ↑p₁ → ↑p₂
hb₁ : Bijective b
hb₂ : ∀ (a : ↑p₁), G.Adj ↑a ↑(b a)
this : (p₁ ∪ Set.range fun v ↦ ↑(b v)) = Set.univ
v : V
x✝ : v ∈ (hall_subgraph (fun v ↦ ↑(b v)) ⋯ hb₂).verts
h✝¹ : v ∉ p₁
x : ↑p₁
h✝ : (fun a ↦ b a = ⟨v, ⋯⟩) x ∧ ∀ (y : ↑p₁), (fun a ↦ b a = ⟨v, ⋯⟩) y → y = x
⊢ ∃! w, ∃ (h : w ∈ p₁), ↑(b ⟨w, ⋯⟩) = v

Tactic:
exact ⟨x, by grind⟩

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

Goal state before:
pp: case inr
ε : ℝ
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' * ε
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj],
      ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n → completeEquipartiteGraph (r + 1) t ⊑ G

Tactic:
have ht'_pos : 0 < t' := by positivity

Goal state after:
case inr
ε : ℝ
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 : ℕ) in atTop,
    ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj],
      ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n → completeEquipartiteGraph (r + 1) t ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : (v : V) → Fintype ↑(M.neighborSet v)
⊢ M.IsMatching ↔ ∀ v ∈ M.verts, M.degree v = 1

Tactic:
simp only [degree_eq_one_iff_existsUnique_adj, IsMatching]

Goal state after:
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✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
⊢ (lapMatrix R G).PosSemidef

Tactic:
refine .of_dotProduct_mulVec_nonneg ?_ (fun x ↦ ?_)

Goal state after:
case refine_1
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✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
⊢ (lapMatrix R G).IsHermitian

case refine_2
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✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
x : V → R
⊢ 0 ≤ star x ⬝ᵥ lapMatrix R G *ᵥ x
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
⊢ ∃ w', w ≠ w' ∧ G.Adj v w'

Tactic:
by
  simp_rw [← SimpleGraph.mem_neighborSet] at hadj ⊢
  have := h ⟨w, hadj⟩
  obtain ⟨w', hww'⟩ := (G.neighborSet v).exists_ne_of_one_lt_ncard (by lia) w
  exact ⟨w', ⟨hww'.2.symm, hww'.1⟩⟩

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 : α
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₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
w✝ : α
hz : w✝ ∈ W
⊢ w✝ ≠ a → w✝ ≠ b → G.Adj w✝ x

Tactic:
haz

Goal state after:
α : 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₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
w✝ : α
hz : w✝ ∈ W
haz : w✝ ≠ a
⊢ w✝ ≠ b → G.Adj w✝ x
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: case h
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : Nonempty V
⊢ (fun x ↦ 1) ≠ 0

Tactic:
rw [← Function.support_nonempty_iff]

Goal state after:
case h
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : Nonempty V
⊢ (Function.support fun x ↦ 1).Nonempty
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 → ℝ), ∑ i, g i • G.lapMatrix_ker_basis_aux i = 0 → ∀ (i : G.ConnectedComponent), g i = 0

Tactic:
intro g h0

Goal state after:
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 : G.ConnectedComponent), g i = 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
x : ↥(toLin' (lapMatrix ℝ G)).ker
a✝ : x ∈ ⊤
⊢ ∀ (a b : V), G.Reachable a b → ↑x a = ↑x b

Tactic:
by rw [← lapMatrix_mulVec_eq_zero_iff_forall_reachable,
    ← toLin'_apply, LinearMap.map_coe_ker]

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
⊢ SimpleGraph.map (⇑(subtype fun x ↦ x ∈ G.edgeSet)) G.lineGraph ≤
    SimpleGraph.map (⇑(subtype fun x ↦ x ∈ G'.edgeSet)) G'.lineGraph

Tactic:
rintro _ _ ⟨hne', ⟨⟨⟩, h₁⟩, ⟨⟨⟩, h₂⟩, ⟨hne, hinter⟩, rfl, rfl⟩
  exact ⟨hne', ⟨⟨_, h h₁⟩, ⟨_, h h₂⟩, ⟨(hne <| Subtype.ext <| Subtype.mk.inj ·), hinter⟩, rfl, rfl⟩⟩

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 : α
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₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ #(insert x (s.erase a) ∩ insert x (t.erase b)) = k + 1

Tactic:
← insert_inter_distrib,

Goal state after:
α : 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₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ #(insert x (s.erase a ∩ t.erase b)) = k + 1
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) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
⊢ G.minDegree * (2 * r + (3 + k)) ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w

Tactic:
← add_assoc,

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) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
⊢ G.minDegree * (2 * r + 3 + k) ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w
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
p₁ p₂ : ↥K.parts
heq : y ↑p₁ ⋯ = y ↑p₂ ⋯
hy₁' : y ↑p₁ ⋯ ⊆ ↑p₁ ∧ #(y ↑p₁ ⋯) = t
hy₂' : y ↑p₁ ⋯ ⊆ ↑p₂ ∧ #(y ↑p₁ ⋯) = t
⊢ 0 < t

Tactic:
exact ht_pos

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : Set V
⊢ G.IsIndepSet cᶜ ↔ G.IsVertexCover c

Tactic:
by
  refine ⟨fun hi v w hadj ↦ ?_, by grind [IsVertexCover, Set.Pairwise]⟩
  by_contra! hh
  exact hi hh.1 hh.2 (Adj.ne hadj) hadj

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
n : ℕ
h₁ : G.vertexCoverNum ≤ ↑n
h₂ : ↑n ≤ ENat.card V
⊢ ∃ s, s.encard = ↑n ∧ G.IsVertexCover s

Tactic:
obtain ⟨s, hs₁, hs₂⟩ := vertexCoverNum_exists G

Goal state after:
V : Type u_1
G : SimpleGraph V
n : ℕ
h₁ : G.vertexCoverNum ≤ ↑n
h₂ : ↑n ≤ ENat.card V
s : Set V
hs₁ : s.encard = G.vertexCoverNum
hs₂ : G.IsVertexCover s
⊢ ∃ s, s.encard = ↑n ∧ G.IsVertexCover s
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case some
m n val✝ : ℕ
s : m.psub n = some val✝
⊢ some val✝ = none ↔ m < n

Tactic:
· grind [psub_eq_some]

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

Goal state before:
pp: α : Type u_1
h : Primcodable α
n : ℕ
⊢ (Nat.casesOn n 1 fun n ↦ Nat.casesOn (encode (decode n)) 0 fun n ↦ n.succ.succ) = encode (decode n)

Tactic:
cases n with

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

Goal state before:
pp: α : Type ?u.4
β : Type ?u.6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ (Nat.pair n_1 n).succ) (encode (decode (Nat.unpair n).2)))
      (encode (decode (Nat.unpair n).1)) =
    encode ((decode (Nat.unpair n).1).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))

Tactic:
cases @decode α _ n.unpair.1

Goal state after:
case none
α : Type ?u.4
β : Type ?u.6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ (Nat.pair n_1 n).succ) (encode (decode (Nat.unpair n).2)))
      (encode none) =
    encode (none.bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))

case some
α : Type ?u.4
β : Type ?u.6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ (Nat.pair n_1 n).succ) (encode (decode (Nat.unpair n).2)))
      (encode (some val✝)) =
    encode ((some val✝).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ n_1.succ) (encode (decode (Nat.unpair n).2)))
      (encode (decode (Nat.unpair n).1)) =
    encode
      (Option.map Prod.fst ((decode (Nat.unpair n).1).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))

Tactic:
cases @decode α _ n.unpair.1

Goal state after:
case none
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ n_1.succ) (encode (decode (Nat.unpair n).2))) (encode none) =
    encode (Option.map Prod.fst (none.bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))

case some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ n_1.succ) (encode (decode (Nat.unpair n).2))) (encode (some val✝)) =
    encode (Option.map Prod.fst ((some val✝).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ n.succ) (encode (decode (Nat.unpair n).2)))
      (encode (decode (Nat.unpair n).1)) =
    encode
      (Option.map Prod.snd ((decode (Nat.unpair n).1).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))

Tactic:
cases @decode α _ n.unpair.1

Goal state after:
case none
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ n.succ) (encode (decode (Nat.unpair n).2))) (encode none) =
    encode (Option.map Prod.snd (none.bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))

case some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ n.succ) (encode (decode (Nat.unpair n).2))) (encode (some val✝)) =
    encode (Option.map Prod.snd ((some val✝).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
x' : V
hx' : x' ∈ {x, b}
hx'p : x' ∈ p'.support
htw : ∀ t ∈ {x, b}, t ∈ (p'.takeUntil x' hx'p).support → t = x'
h : (p'.takeUntil x' hx'p).toSubgraph.Adj x b
⊢ False

Tactic:
simp [htw _ (by simp) (Walk.mem_support_of_adj_toSubgraph h.symm),
        htw _ (by simp) (Walk.mem_support_of_adj_toSubgraph h)] at hnxb

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

Goal state before:
pp: ⊢ Primrec₂ fun x1 x2 ↦ x1 / x2

Tactic:
refine of_graph ⟨_, fst, fun p => Nat.div_le_self _ _⟩ ?_
  have : PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) => (a.2 = 0 ∧ b = 0) ∨
      (0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2) :=
    PrimrecPred.or
      (.and (const 0 |> Primrec.eq.comp (fst |> snd.comp)) (const 0 |> Primrec.eq.comp snd))
      (.and (nat_lt.comp (const 0) (fst |> snd.comp)) <|
          .and (nat_le.comp (nat_mul.comp snd (fst |> snd.comp)) (fst |> fst.comp))
          (nat_lt.comp (fst.comp fst) (nat_mul.comp (Primrec.succ.comp snd) (snd.comp fst))))
  refine this.of_eq ?_
  rintro ⟨a, k⟩ q
  if H : k = 0 then simp [H, eq_comm]
  else
    have : q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k := by
      rw [le_antisymm_iff, ← (@Nat.lt_succ_iff _ q), Nat.le_div_iff_mul_le (Nat.pos_of_ne_zero H),
          Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero H)]
    simpa [H, zero_lt_iff, eq_comm (b := q)]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m k : ℕ
kn : n ≤ k + m
⊢ Acc (lbp p) k

Tactic:
induction m generalizing k with

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

Goal state before:
pp: v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec v.tail.head (fun y IH ↦ (y ::ᵥ IH ::ᵥ v.tail).tail.head.succ) v.head = v.head + v.tail.head

Tactic:
by
    simp; induction v.head <;> simp [*, Nat.succ_add]

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

Goal state before:
pp: this : Primrec' fun v ↦ (fun a b ↦ b - a) v.head v.tail.head
⊢ Primrec' fun v ↦ v.head - v.tail.head

Tactic:
simpa using comp₂ (fun a b => b - a) this (tail head) head

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

Goal state before:
pp: case pair
n : ℕ
f✝¹ : List.Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
hf : Primrec' fun v ↦ f✝ v.head
hg : Primrec' fun v ↦ g✝ v.head
⊢ Primrec' fun v ↦ (fun n ↦ pair (f✝ n) (g✝ n)) v.head

Tactic:
exact natPair.comp₂ _ hf hg

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
⊢ m + n + 2 = (m + 1 + n).succ

Tactic:
by rw [succ_eq_add_one]; ring_nf

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun z ↦ p * z ^ (p - 1) * (1 + ε z)) ~[atTop] fun z ↦ p * z ^ (p - 1)

Tactic:
calc
        (fun z => p * z ^ (p - 1) * (1 + ε z)) ~[atTop] fun z => p * z ^ (p - 1) * 1 :=
              IsEquivalent.mul IsEquivalent.refl isEquivalent_one_add_smoothingFn_one
        _ = fun z => p * z ^ (p - 1) := by ext; ring

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
h₁ : ∑ x, 0 = 0
i : α
x✝ : i ∈ univ
⊢ Tendsto (fun p ↦ a i * b i ^ p) atTop (𝓝 0)

Tactic:
rw [← mul_zero (a i)]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
h₁ : ∑ x, 0 = 0
i : α
x✝ : i ∈ univ
⊢ Tendsto (fun p ↦ a i * b i ^ p) atTop (𝓝 (a i * 0))