mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ a ∈ s ∧ b ∈ t ∧ a ≠ v ∧ b ≠ v ∧ a ≠ w₂ ∧ b ≠ w₁

Tactic:
by grind

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
⊢ insert w₁ s ⊆ W ∧ insert w₂ t ⊆ W

Tactic:
by grind

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
⊢ G.IsPathGraph3Compl v w₁ w₂

Tactic:
by grind

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
⊢ v ∉ insert x (s.erase a)

Tactic:
by grind

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
⊢ v ∉ insert x (t.erase b)

Tactic:
by grind

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
⊢ w₁ ∉ insert x (s.erase a)

Tactic:
by grind

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
⊢ w₂ ∉ insert x (t.erase b)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst✝² : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
x w✝ : α
hz : w✝ ∈ insert w₁ s ∧ ¬G.Adj x w✝
⊢ w✝ ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))

Tactic:
by grind

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ s(v, w') = s(u, x)

Tactic:
by grind

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
⊢ s(v, w) = s(u, x)

Tactic:
by grind

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

Goal state before:
pp: case neg.inr.inl
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
⊢ G'.Adj u x ↔ ¬G'.Adj v w'

Tactic:
simp only [hnadj, false_iff, not_not]

Goal state after:
case neg.inr.inl
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
⊢ G'.Adj v w'
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
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
⊢ y = w

Tactic:
have ⟨w', hw'⟩ := hG'cyc.other_adj_of_adj hr.1

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
y : V
hr : G'.Adj v y ∧ ¬M.Adj v y
w' : V
hw' : y ≠ w' ∧ G'.Adj v w'
⊢ y = w
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
⊢ #X * (#W - 3) + #Xᶜ * (#W - 1) + 2 * (#X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)) =
    #X * (#W - 3 + 2 * k) + #Xᶜ * (#W - 1 + 2 * (k - 1))

Tactic:
by grind

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ (G.incidenceFinset x).val = Multiset.filter (fun e ↦ x ∈ e) ↑p.edges

Tactic:
convert_to! _ = (ht.isTrail.edgesFinset.filter (x ∈ ·)).val

Goal state after:
case convert_2
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ (G.incidenceFinset x).val = {x_1 ∈ ⋯.edgesFinset | x ∈ x_1}.val
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u : V
p : G.Walk u u
ht : p.IsEulerian
⊢ {x | ¬u = u ∧ (¬x = u → x = u)} = ∅ ∨ {x | ¬u = u ∧ (¬x = u → x = u)}.card = 2

pp: case inr
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ {x | ¬u = v ∧ (¬x = u → x = v)} = ∅ ∨ {x | ¬u = v ∧ (¬x = u → x = v)}.card = 2

Tactic:
· simp

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ {x | ¬u = v ∧ (¬x = u → x = v)} = ∅ ∨ {x | ¬u = v ∧ (¬x = u → x = v)}.card = 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case refine_4
ε : ℝ
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₂✝ : Finset (Fin n)
v₁ v₂ : Fin n
hv₂ : v₂ ∈ ↑p₂✝
p₁ : Finset (Fin n)
hp₁ : p₁ ∈ K.parts
hne : y p₁ ⋯ ≠ p₂✝
hv₁ : v₁ ∈ ↑(y p₁ ⋯)
hyp₁ : y p₁ ⋯ = p₁✝
hy₁' : y p₁ hp₁ ⊆ p₁ ∧ #(y p₁ hp₁) = t
p₂ : Finset (Fin n)
hp₂ : p₂ ∈ K.parts
hyp₂ : y p₂ ⋯ = p₂✝
⊢ G.Adj v₁ v₂

Tactic:
← hyp₂

Goal state after:
case refine_4
ε : ℝ
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₂✝ : Finset (Fin n)
v₁ v₂ : Fin n
p₁ : Finset (Fin n)
hp₁ : p₁ ∈ K.parts
hv₁ : v₁ ∈ ↑(y p₁ ⋯)
hyp₁ : y p₁ ⋯ = p₁✝
hy₁' : y p₁ hp₁ ⊆ p₁ ∧ #(y p₁ hp₁) = t
p₂ : Finset (Fin n)
hp₂ : p₂ ∈ K.parts
hne : y p₁ ⋯ ≠ y p₂ ⋯
hv₂ : v₂ ∈ ↑(y p₂ ⋯)
hyp₂ : y p₂ ⋯ = p₂✝
⊢ G.Adj v₁ v₂
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: case refine_1
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₁ : PlacedTile ps
⊢ pt₁.index = pt₁.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₁.index)).subtype (↑ps pt₁.index).symmetries)) ⁻¹'
        {pt₁.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₁.index)).subtype (↑ps pt₁.index).symmetries)) ⁻¹'
        {pt₁.groupElts}

Tactic:
simp only [and_self]

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

Goal state before:
pp: case nil
c : ℕ × ℕ
⊢ c ∈ ∅ ↔ ∃ (h : c.1 < [].length), c.2 < [][c.1]

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:
· simp

Goal state after:
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]
Module: Mathlib.Computability.Primrec.Basic

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

Tactic:
| succ n =>

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

Goal state before:
pp: 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))

pp: 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))

Tactic:
· simp

Goal state after:
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.List

Goal state before:
pp: case hz
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := ⋯
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n : ℕ
⊢ encode
      (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
        (ofNat (List ℕ) 0)) =
    encode (decode 0)

pp: case hi
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := ⋯
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ m ≤ n,
        encode
            (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
              (ofNat (List ℕ) m)) =
          encode (decode m)) →
      encode
          (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) (n + 1))) =
        encode (decode (n + 1))

Tactic:
· simp

Goal state after:
case hi
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := ⋯
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ m ≤ n,
        encode
            (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
              (ofNat (List ℕ) m)) =
          encode (decode m)) →
      encode
          (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) (n + 1))) =
        encode (decode (n + 1))
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 : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
a : ∀ k_1 ≤ k, false ∈ p k_1
⊢ n ≤ k + 1 + m

Tactic:
rw [Nat.add_right_comm]; exact kn

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
⊢ (rfindOpt f).Dom

Tactic:
have h' : ∃ n, (f n).isSome := h.imp fun n => Option.isSome_iff_exists.2
    have s := Nat.find_spec h'
    have fd : (rfind fun n => (f n).isSome).Dom :=
      ⟨Nat.find h', by simpa using s.symm, fun _ _ => trivial⟩
    refine ⟨fd, ?_⟩
    have := rfind_spec (get_mem fd)
    simpa using this

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case none
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
e : decode n = Option.none
⊢ (((↑Option.none).bind fun a ↦ Part.map encode (↑f a)).bind fun n_1 ↦
      Nat.rec ((↑Option.none).bind fun a ↦ Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode ((fun p ↦ h p.1 p.2) a))
        n_1) =
    (↑Option.none).bind fun a ↦
      Part.map encode ((fun a ↦ Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) (f a)) a)

pp: case some
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
⊢ (((↑(Option.some a)).bind fun a ↦ Part.map encode (↑f a)).bind fun n_1 ↦
      Nat.rec ((↑(Option.some a)).bind fun a ↦ Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode ((fun p ↦ h p.1 p.2) a))
        n_1) =
    (↑(Option.some a)).bind fun a ↦
      Part.map encode ((fun a ↦ Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) (f a)) a)

Tactic:
· simp

Goal state after:
case some
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
⊢ (((↑(Option.some a)).bind fun a ↦ Part.map encode (↑f a)).bind fun n_1 ↦
      Nat.rec ((↑(Option.some a)).bind fun a ↦ Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode ((fun p ↦ h p.1 p.2) a))
        n_1) =
    (↑(Option.some a)).bind fun a ↦
      Part.map encode ((fun a ↦ Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) (f a)) a)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case zero
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
⊢ Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun i ↦ h a (0 - 1)) 0 =
    Nat.rec (Part.some (g a)) (fun n n_ih ↦ h a n) 0

pp: case succ
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
⊢ Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun i ↦ h a (n + 1 - 1)) (n + 1) =
    Nat.rec (Part.some (g a)) (fun n n_ih ↦ h a n) (n + 1)

Tactic:
· simp

Goal state after:
case succ
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
⊢ Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun i ↦ h a (n + 1 - 1)) (n + 1) =
    Nat.rec (Part.some (g a)) (fun n n_ih ↦ h a n) (n + 1)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case zero
m : ℕ
⊢ ack m (0 + 1) ≤ ack (m + 1) 0

pp: case succ
m n : ℕ
⊢ ack m (n + 1 + 1) ≤ ack (m + 1) (n + 1)

Tactic:
· simp

Goal state after:
case succ
m n : ℕ
⊢ ack m (n + 1 + 1) ≤ ack (m + 1) (n + 1)
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case H
⊢ ∀ (n : ℕ × ℕ), ack n.1 n.2 ∈ (pappAck n.1).eval n.2

Tactic:
· simp

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

Tactic:
by
  filter_upwards [R.dist_r_b'] with n hn i
  calc r i n = b i * n + (r i n - b i * n) := by ring
             _ ≤ b i * n + ‖r i n - b i * n‖ := by gcongr; exact Real.le_norm_self _
             _ ≤ b i * n + n / log n ^ 2 := by gcongr; exact hn i

Goal state after: