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

Goal state before:
pp: m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ zarankiewicz m n s t ≤ extremalNumber (Fintype.card (Fin (m + n))) (completeBipartiteGraph α β)

Tactic:
simp_rw [zarankiewicz, Finset.sup_le_iff, mem_filter, mem_univ, true_and]

Goal state after:
m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ ∀ (b : SimpleGraph (Fin m ⊕ Fin n)),
    b ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free b →
      #b.edgeFinset ≤ extremalNumber (Fintype.card (Fin (m + n))) (completeBipartiteGraph α β)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
⊢ (⋃ i, s i).encard ≤ ∑ᶠ (i : ι), (s i).encard

Tactic:
simpa using finite_univ.encard_biUnion_le s

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 : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
s : Finset V
⊢ s.card ≤ (s.biUnion fun x ↦ G.neighborFinset x).card

Tactic:
have := h₂ s
    simpa [← Set.ncard_coe_finset, neighborFinset_def]

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

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun i j ↦ Disjoint (f i).support (f j).support
v : V
hv : v ∈ (⨆ i, f i).verts
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun w ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun w ↦ (f i).Adj v w) y → y = w
y : V
hy : (⨆ i, f i).Adj v y
i' : ι
hi' : (f i').Adj v y
heq : ¬i = i'
this : (fun i j ↦ Disjoint (f i).support (f j).support) i i'
⊢ y = w

Tactic:
simp only [Set.disjoint_left] at this

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun i j ↦ Disjoint (f i).support (f j).support
v : V
hv : v ∈ (⨆ i, f i).verts
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun w ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun w ↦ (f i).Adj v w) y → y = w
y : V
hy : (⨆ i, f i).Adj v y
i' : ι
hi' : (f i').Adj v y
heq : ¬i = i'
this : ∀ ⦃a : V⦄, a ∈ (f i).support → a ∉ (f i').support
⊢ y = w
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
h : Fintype.card α = 2
hG : G.IsHamiltonian
v : α
p : G.Walk v v
hp : p.IsHamiltonianCycle
⊢ False

Tactic:
grind [hp.three_le_length, hp.length_eq]

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
w' : V
hw' : (fun w ↦ M'.Adj v w) w' ∧ ∀ (y : V), (fun w ↦ M'.Adj v w) y → y = w'
⊢ (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
    ∃ x y, ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}

Tactic:
by_cases hww' : w = w'

Goal state after:
case pos
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
w' : V
hw' : (fun w ↦ M'.Adj v w) w' ∧ ∀ (y : V), (fun w ↦ M'.Adj v w) y → y = w'
hww' : w = w'
⊢ (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
    ∃ x y, ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}

case neg
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
hw : (fun w ↦ M.Adj v w) w ∧ ∀ (y : V), (fun w ↦ M.Adj v w) y → y = w
w' : V
hw' : (fun w ↦ M'.Adj v w) w' ∧ ∀ (y : V), (fun w ↦ M'.Adj v w) y → y = w'
hww' : ¬w = w'
⊢ (∀ (x : V), (¬M.Adj v x ∨ M'.Adj v x) ∧ (¬M'.Adj v x ∨ M.Adj v x)) ∨
    ∃ x y, ¬x = y ∧ (M.spanningCoe \ M'.spanningCoe ⊔ M'.spanningCoe \ M.spanningCoe).neighborSet v = {x, y}
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 : G.ConnectedComponent), g i = 0

Tactic:
have h : ∑ c, g c • lapMatrix_ker_basis_aux G c = fun i ↦ g (connectedComponentMk G i) := by
    simp only [lapMatrix_ker_basis_aux, SetLike.mk_smul_mk]
    repeat rw [AddSubmonoid.coe_finsetSum]
    ext i
    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:
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
h : ↑(∑ c, g c • G.lapMatrix_ker_basis_aux c) = fun i ↦ g (G.connectedComponentMk i)
⊢ ∀ (i : G.ConnectedComponent), g i = 0
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
by_cases hww' : w = w'

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : w = w'
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : w = w'
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
subst hww'
    have : (G \ p.toSubgraph.spanningCoe).Adj w v := by
      simp only [sdiff_adj, Subgraph.spanningCoe_adj]
      exact ⟨hw'2.symm, fun h ↦ hnpvw' h.symm⟩
    exact this.reachable

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 ∩ t.erase b).erase a)) = k + 1

Tactic:
inter_erase,

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 ∩ t).erase b).erase a)) = k + 1
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
⊢ H.spanningCoe.IsAlternating G'

Tactic:
intro v w w' hww' hvw hvv'
  simp only [Subgraph.spanningCoe_adj] at hvw hvv'
  exact halt hww' hvw.adj_sub hvv'.adj_sub

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' * ε
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'
⊢ completeEquipartiteGraph (r + 1) t ⊑ G

Tactic:
replace ih : completeEquipartiteGraph r t' ⊑ G := by
      rcases eq_or_ne r 1 with hr_eq_1 | hr_ne_1
      -- if `r = 1` then `completeEquipartiteGraph r t' = ⊥`
      · have h0 : r ≤ 1 ∨ t' = 0 := Or.inl hr_eq_1.le
        rw [completeEquipartiteGraph_eq_bot_iff.mpr h0, bot_isContained_iff_card_le,
          card_prod, Fintype.card_fin, Fintype.card_fin, hr_eq_1, one_mul, Fintype.card_fin]
        apply hn.trans'
        exact_mod_cast calc (t' : ℝ)
          _ ≤ r * t' := le_mul_of_one_le_left (by positivity) (mod_cast hr_pos)
          _ ≤ t'.choose t ^ r * t + r * t' := le_add_of_nonneg_left (by positivity)
          _ ≤ (t'.choose t ^ r * t + r * t') * (t' - t) / (r * t' * ε - t) := by
            rw [mul_div_assoc, le_mul_iff_one_le_right (by positivity),
              one_le_div (sub_pos.mpr ht_lt_rt'ε), sub_le_sub_iff_right,
              mul_comm (r : ℝ) (t' : ℝ),  mul_assoc, mul_le_iff_le_one_right (by positivity)]
            exact hrε_lt_1.le
          _ ≤ ⌈(t'.choose t ^ r * t + r * t') * (t' - t) / (r * t' * ε - t)⌉₊ := Nat.le_ceil _
          _ ≤ N := Nat.cast_le.mpr (le_max_right _ _)
      -- if `r > 1` then `G` satisfies the inductive hypothesis
      · have hδ' := calc (G.minDegree : ℝ)
          _ ≥ (1 - 1 / (r - 1) + (1 / (r - 1) - 1 / r) + ε) * n := by
              rwa [← sub_add_sub_cancel _ (1 / (r - 1) : ℝ) _] at hδ
          _ = (1 - 1 / ↑(r - 1) + ε') * n := by
              rw [← one_div_mul_sub_mul_one_div_eq_one_div_add_one_div
                (sub_ne_zero_of_ne (mod_cast hr_ne_1)) (mod_cast hr_pos.ne'),
                sub_sub_cancel, mul_one, one_div_mul_one_div_rev, mul_comm (r : ℝ) _,
                ← Nat.cast_pred hr_pos, add_assoc]
        rw [← Nat.succ_pred_eq_of_pos hr_pos]
        exact ih n (hn.trans' (le_max_of_le_left (le_max_right 1 N'))) hδ'

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' : ℕ
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
⊢ completeEquipartiteGraph (r + 1) t ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
⊢ Fintype.card ↑(Gᶜ.commonNeighbors v w) = n - (2 * k - μ) - 2

Tactic:
simp only [← Set.toFinset_card, commonNeighbors, Set.toFinset_inter, neighborSet_compl,
    Set.toFinset_sdiff, Set.toFinset_singleton, Set.toFinset_compl, ← neighborFinset_def]

Goal state after:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : Gᶜ.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - μ) - 2
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ Fintype.card V - (2 * k - μ) - (1 + 1) = n - (2 * k - μ) - 2

Tactic:
← h.card

Goal state after:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ Fintype.card V - (2 * k - μ) - (1 + 1) = Fintype.card V - (2 * k - μ) - 2
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : ¬Gᶜ.Adj v w
⊢ Fintype.card ↑(Gᶜ.commonNeighbors v w) = n - (2 * k - ℓ)

Tactic:
simp only [← Set.toFinset_card, commonNeighbors, Set.toFinset_inter, neighborSet_compl,
    Set.toFinset_sdiff, Set.toFinset_singleton, Set.toFinset_compl, ← neighborFinset_def]

Goal state after:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : ¬Gᶜ.Adj v w
⊢ #((G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w})) = n - (2 * k - ℓ)
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
h2' : G.Adj v w
⊢ Fintype.card V - (2 * k - ℓ) = n - (2 * k - ℓ)

pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
h2' : G.Adj v w
⊢ G.Adj v w

Tactic:
← h.card

Goal state after:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
h2' : G.Adj v w
⊢ Fintype.card V - (2 * k - ℓ) = Fintype.card V - (2 * k - ℓ)

V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
hn : v ≠ w
hna : v ≠ w → G.Adj v w
h2' : G.Adj v w
⊢ G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.UniversalVerts

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
⊢ ∃ t ⊆ G.universalVerts, ∃ M, M.verts = s ∪ t ∧ M.IsMatching

Tactic:
by
  obtain ⟨t, ht⟩ := Set.exists_subset_card_eq hc
  refine ⟨t, ht.1, ?_⟩
  obtain ⟨f⟩ : Nonempty (s ≃ t) := by
    rw [← Cardinal.eq, ← t.cast_ncard t.toFinite, ← s.cast_ncard s.toFinite, ht.2]
  let hd := Set.disjoint_of_subset_left ht.1 h
  have hadj (v : s) : G.Adj v (f v) := ht.1 (f v).2 (hd.ne_of_mem (f v).2 v.2) |>.symm
  exact Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv hd.symm f hadj

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
⊢ 1 + 1 ≤ (Set.univ \ t).encard

Tactic:
Set.encard_sdiff (by simp) (Set.finite_of_encard_eq_coe ht₁),

Goal state after:
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
⊢ 1 + 1 ≤ Set.univ.encard - t.encard
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: 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
h : M1.Adj a c
⊢ False

Tactic:
simpa [hnGac, edge_adj, hnac, hxa.ne, hnbc.symm, hab.ne]
    using h.adj_sub

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

Goal state before:
pp: case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens tail✝ ↔ ∃ (h : c.1 < tail✝.length), c.2 < tail✝[c.1]
c : ℕ × ℕ
⊢ c ∈
      {0} ×ˢ Finset.range head✝ ∪
        Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens tail✝) ↔
    ∃ (h : c.1 < (head✝ :: tail✝).length), c.2 < (head✝ :: tail✝)[c.1]

Tactic:
rcases c with ⟨⟨_, _⟩, _⟩ <;> simp_all

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
l : List α
⊢ (List.casesOn (id l) none fun b l_1 ↦ some (l, b, l_1).2.1) = l.head?

Tactic:
cases l <;> rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
l : List α
⊢ (List.casesOn (id l) [] fun b l_1 ↦ (l, b, l_1).2.2) = l.tail

Tactic:
cases l <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
g : β → α → α
hg : Primrec₂ g
l : List α
b : β
⊢ (List.casesOn (l, b).1 [] fun b_1 l_1 ↦ g ((l, b), b_1, l_1).1.2 ((l, b), b_1, l_1).2.1 :: ((l, b), b_1, l_1).2.2) =
    List.modifyHead (g b) l

Tactic:
cases l <;> rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
n : ℕ
x✝ : List.Vector α n
l : List α
h : l.length = n
⊢ (List.Vector.toList ⟨l, h⟩).tail = (List.Vector.tail ⟨l, h⟩).toList

Tactic:
cases l <;> rfl

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack (m + 1) (n₁ + 1) < ack (m + 1) (n₂ + 1)

Tactic:
by
    rw [ack_succ_succ, ack_succ_succ]
    apply ack_strictMono_right _ (ack_strictMono_right _ _)
    rwa [add_lt_add_iff_right] at h

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
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, ‖↑(r i x) - b i * ↑x‖ ≤ ↑x / log ↑x ^ 2

Tactic:
intro i

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ ∀ᶠ (x : ℕ) in atTop, ‖↑(r i x) - b i * ↑x‖ ≤ ↑x / log ↑x ^ 2
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
h_max_bi_lt_one : 0 < 1 - b (max_bi b)
hc_pos : 0 < c
h₁ : 0 < (1 - b (max_bi b)) / 2
hc_lt_one : c < 1
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑x‖
n : ℕ
hn : ‖↑n / log ↑n ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑n‖
hn' : ∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2
⊢ ∀ (i : α), ↑(r i n) ≤ c * ↑n

Tactic:
intro i

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2
h_max_bi_pos : 0 < b (max_bi b)
h_max_bi_lt_one : 0 < 1 - b (max_bi b)
hc_pos : 0 < c
h₁ : 0 < (1 - b (max_bi b)) / 2
hc_lt_one : c < 1
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑x‖
n : ℕ
hn : ‖↑n / log ↑n ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑n‖
hn' : ∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2
i : α
⊢ ↑(r i n) ≤ c * ↑n
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < log (b i * ↑x)

Tactic:
intro i

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ ∀ᶠ (x : ℕ) in atTop, 0 < log (b i * ↑x)
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 : α), ∀ᶠ (x : ℕ) in atTop, ↑(r i x) ^ p a b * (1 - ε ↑(r i x)) ≤ b i ^ p a b * ↑x ^ p a b * (1 - ε ↑x)

Tactic:
intro i

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ ∀ᶠ (x : ℕ) in atTop, ↑(r i x) ^ p a b * (1 - ε ↑(r i x)) ≤ b i ^ p a b * ↑x ^ p a b * (1 - ε ↑x)
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)
x✝ : ℝ
⊢ x✝ ^ (p a b - 1) * 1 = x✝ ^ (p a b - 1)

Tactic:
rw [mul_one]

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 ↦ x ^ (p a b - 1) * 1) = fun x ↦ x ^ (p a b - 1)

Tactic:
by ext; rw [mul_one]

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
i : α
this : -log (b i) ≠ 0
⊢ (fun n ↦ -log (b i) * (1 / log ↑n ^ 2)) =Θ[atTop] fun n ↦ 1 / log ↑n ^ 2

Tactic:
rw [← isTheta_const_mul_right this]

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 : α), ∀ᶠ (x : ℕ) in atTop, b i ^ p a b * ↑x ^ p a b * (1 + ε ↑x) ≤ ↑(r i x) ^ p a b * (1 + ε ↑(r i x))

Tactic:
intro i

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ ∀ᶠ (x : ℕ) in atTop, b i ^ p a b * ↑x ^ p a b * (1 + ε ↑x) ≤ ↑(r i x) ^ p a b * (1 + ε ↑(r i x))