mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹ : t ≤ #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
s : Finset (Fin n)
hs✝ : s ∈ powersetCard t ({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
hs : s ⊆ {v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v} ∧ #s = t
hs' : s ∈ powersetCard t p
w : Fin n
hw✝ : w ∈ s
hw : w ∈ id p ∧ G.Adj w v ∧ (w ∈ ↑K.verts ∧ v ∈ (↑K.verts)ᶜ ∨ w ∈ (↑K.verts)ᶜ ∧ v ∈ ↑K.verts)
⊢ ?m.327 hs' w hw✝

Tactic:
]

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✝¹ : t ≤ #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
s : Finset (Fin n)
hs✝ : s ∈ powersetCard t ({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
hs : s ⊆ {v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v} ∧ #s = t
hs' : s ∈ powersetCard t p
w : Fin n
hw✝ : w ∈ s
hw : w ∈ id p ∧ G.Adj w v ∧ (w ∈ ↑K.verts ∧ v ∈ (↑K.verts)ᶜ ∨ w ∈ (↑K.verts)ᶜ ∧ v ∈ ↑K.verts)
⊢ ?m.327 hs' w hw✝
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
V : Type u_2
inst✝¹ : Fintype V
h_verts : Fintype.card V ≥ H.turanDensityConst ε
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ ↑(#(G.overFin ⋯).edgeFinset) ≥ (H.turanDensity + ε) * ↑((Fintype.card V).choose 2) → H ⊑ G.overFin ⋯

Tactic:
]

Goal state after:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
V : Type u_2
inst✝¹ : Fintype V
h_verts : Fintype.card V ≥ H.turanDensityConst ε
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ ↑(#(G.overFin ⋯).edgeFinset) ≥ (H.turanDensity + ε) * ↑((Fintype.card V).choose 2) → H ⊑ G.overFin ⋯
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'
⊢ ∑ x ∈ K.vertsᶜ, ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree x) = ↑(#(between (↑K.verts) (↑K.verts)ᶜ G).edgeFinset)

Tactic:
]

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'
⊢ ∑ x ∈ K.vertsᶜ, ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree x) = ↑(#(between (↑K.verts) (↑K.verts)ᶜ G).edgeFinset)
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a : α
w : G.Walk a a
hwc : w.IsCircuit
hlg : ↑w.length < G.egirth
w' : G.Walk a a := w.cycleBypass
hwc' : w'.IsCycle
⊢ ↑w.length < G.egirth

Tactic:
]

Goal state after:
α : Type u_1
G : SimpleGraph α
a : α
w : G.Walk a a
hwc : w.IsCircuit
hlg : ↑w.length < G.egirth
w' : G.Walk a a := w.cycleBypass
hwc' : w'.IsCycle
⊢ ↑w.length < G.egirth
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 ∈ K.vertsᶜ \ filter K t
⊢ ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) ≤ ↑(#K.verts - t') + ↑t

Tactic:
]

Goal state after:
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 ∈ K.vertsᶜ \ filter K t
⊢ ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) ≤ ↑(#K.verts - t') + ↑t
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: α : Type u_1
h : 3 ≤ ENat.card α
s : Finset α
hcard : 3 = s.card
x y z : α
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
w : ⊤.Walk x x := Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
hw : w = Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
this : w.IsCycle
⊢ ↑w.length ≤ 3

Tactic:
]

Goal state after:
α : Type u_1
h : 3 ≤ ENat.card α
s : Finset α
hcard : 3 = s.card
x y z : α
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
w : ⊤.Walk x x := Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
hw : w = Walk.cons hxy (Walk.cons hyz (Walk.cons ⋯ Walk.nil))
this : w.IsCycle
⊢ ↑w.length ≤ 3
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'
⊢ (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t)

Tactic:
]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
G : SimpleGraph α
G' : SimpleGraph β
h : G ⊑ G'
hacyc : ¬G.IsAcyclic
a : α
w : G.Walk a a
hw : w.IsCycle
hwl : G.egirth = ↑w.length
⊢ G'.egirth ≤ ↑(Walk.map (Nonempty.some h).toHom w).length

Tactic:
]

Goal state after:
case neg
α : Type u_1
β : Type u_2
G : SimpleGraph α
G' : SimpleGraph β
h : G ⊑ G'
hacyc : ¬G.IsAcyclic
a : α
w : G.Walk a a
hw : w.IsCycle
hwl : G.egirth = ↑w.length
⊢ G'.egirth ≤ ↑(Walk.map (Nonempty.some h).toHom w).length
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'
⊢ ∑ x ∈ K.vertsᶜ \ filter K t, (↑(#K.verts) - ↑t' + ↑t) + ∑ x ∈ filter K t, ↑(#K.verts) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t)

Tactic:
rw [sum_const, nsmul_eq_mul, card_sdiff_of_subset (filter_subset_compl_verts K),
          Nat.cast_sub (card_le_card (filter_subset_compl_verts K)), card_compl,
          Nat.cast_sub (card_le_univ K.verts), Fintype.card_fin, sum_const, nsmul_eq_mul, sub_mul,
          sub_add (#K.verts : ℝ) _ _, mul_sub (#(filter K t) : ℝ) _ _,
          ← sub_add, sub_add_eq_add_sub, sub_add_cancel]

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'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ ∑ x ∈ K.vertsᶜ \ filter K t, (↑(#K.verts) - ↑t' + ↑t) + ∑ x ∈ filter K t, ↑(#K.verts) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t)

Tactic:
by
        rw [sum_const, nsmul_eq_mul, card_sdiff_of_subset (filter_subset_compl_verts K),
          Nat.cast_sub (card_le_card (filter_subset_compl_verts K)), card_compl,
          Nat.cast_sub (card_le_univ K.verts), Fintype.card_fin, sum_const, nsmul_eq_mul, sub_mul,
          sub_add (#K.verts : ℝ) _ _, mul_sub (#(filter K t) : ℝ) _ _,
          ← sub_add, sub_add_eq_add_sub, sub_add_cancel]

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case inl
α : Type u_1
s : Set α
hs : s.Infinite
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = 0

Tactic:
]

Goal state after:
case inl
α : Type u_1
s : Set α
hs : s.Infinite
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = 0
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)
⊢ (↑N + ↑r * ↑t') * (↑t' - ↑t) - ↑r * ↑t' * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t) - ↑r * ↑t' * (↑t' - ↑t)

Tactic:
]

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)
⊢ (↑N + ↑r * ↑t') * (↑t' - ↑t) - ↑r * ↑t' * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t) - ↑r * ↑t' * (↑t' - ↑t)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ #↑s = #↑s

Tactic:
]

Goal state after:
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
B : SimpleGraph (Fin m ⊕ Fin n)
left✝ : B ≤ completeBipartiteGraph (Fin m) (Fin n)
h : (completeBipartiteGraph (Fin s) (Fin t)).Free B
⊢ #(SimpleGraph.map (⇑finSumFinEquiv) B).edgeFinset ≤
    extremalNumber (Fintype.card (Fin (m + n))) (completeBipartiteGraph α β)

Tactic:
]

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)
left✝ : B ≤ completeBipartiteGraph (Fin m) (Fin n)
h : (completeBipartiteGraph (Fin s) (Fin t)).Free B
⊢ #(SimpleGraph.map (⇑finSumFinEquiv) B).edgeFinset ≤
    extremalNumber (Fintype.card (Fin (m + n))) (completeBipartiteGraph α β)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case inr
α : Type u_1
s : Set α
hs : s.Finite
he : Even #hs.toFinset
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
]

Goal state after:
case inr
α : Type u_1
s : Set α
hs : s.Finite
he : Even #hs.toFinset
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case inr
α : Type u_1
s : Set α
hs : s.Finite
he : Even #hs.toFinset
t u : Finset α
hutu : t ∪ u = hs.toFinset
hdtu : Disjoint t u
hctu : #t = #u
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
use t, u

Goal state after:
case h
α : Type u_1
s : Set α
hs : s.Finite
he : Even #hs.toFinset
t u : Finset α
hutu : t ∪ u = hs.toFinset
hdtu : Disjoint t u
hctu : #t = #u
⊢ ↑t ∪ ↑u = s ∧ Disjoint ↑t ↑u ∧ #↑↑t = #↑↑u
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: n s t : ℕ
α : Type u_3
β : Type u_4
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ ∀ ⦃G : SimpleGraph (Fin n)⦄ [inst : DecidableRel G.Adj],
    (completeBipartiteGraph α β).Free G → ↑(#G.edgeFinset) ≤ ↑(zarankiewicz n n s t) / 2

Tactic:
]

Goal state after:
n s t : ℕ
α : Type u_3
β : Type u_4
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ ∀ ⦃G : SimpleGraph (Fin n)⦄ [inst : DecidableRel G.Adj],
    (completeBipartiteGraph α β).Free G → ↑(#G.edgeFinset) ≤ ↑(zarankiewicz n n s t) / 2
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case mpr.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : t.Finite ∧ u.Finite
⊢ Even (t ∪ u).ncard

Tactic:
]

Goal state after:
case mpr.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : t.Finite ∧ u.Finite
⊢ Even (t ∪ u).ncard
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case mpr.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : t.Finite ∧ u.Finite
hn : t.ncard = u.ncard
⊢ Even (u.ncard + u.ncard)

Tactic:
]

Goal state after:
case mpr.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : t.Finite ∧ u.Finite
hn : t.ncard = u.ncard
⊢ Even (u.ncard + u.ncard)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: n s t : ℕ
α : Type u_3
β : Type u_4
inst✝⁴ : Fintype α
inst✝³ : Fintype β
inst✝² : Nonempty α
inst✝¹ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
h : (completeBipartiteGraph α β).Free G
⊢ 2 * #G.edgeFinset ≤ zarankiewicz n n s t

Tactic:
]

Goal state after:
n s t : ℕ
α : Type u_3
β : Type u_4
inst✝⁴ : Fintype α
inst✝³ : Fintype β
inst✝² : Nonempty α
inst✝¹ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
h : (completeBipartiteGraph α β).Free G
⊢ 2 * #G.edgeFinset ≤ zarankiewicz n n s t
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : ∀ i ∈ t, (s i).Finite
h : t.PairwiseDisjoint s
⊢ ∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
hs : ∀ (i : ι), (s i).Finite
h : Pairwise (Disjoint on s)
⊢ (⋃ i, s i).ncard = (⋃ i ∈ univ, s i).ncard

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
hs : ∀ (i : ι), (s i).Finite
h : Pairwise (Disjoint on s)
⊢ (⋃ i, s i).ncard = (⋃ i ∈ univ, s i).ncard
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
h : ∀ i ∈ t, (s i).Finite
this : (⋃ i ∈ t, s i).Finite
⊢ ∑ᶠ (x : ι) (_ : x ∈ t), ↑(s x).ncard = ∑ᶠ (i : ι) (_ : i ∈ t), ↑(s i).ncard

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
i : ι
hi : i ∈ t
hn : (s i).Infinite
⊢ (⋃ i_1 ∈ insert i (t \ {i}), s i_1).encard = (s i).encard + ∑ᶠ (i_1 : ι) (_ : i_1 ∈ t \ {i}), (s i_1).encard

Tactic:
]

Goal state after:
case neg
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
i : ι
hi : i ∈ t
hn : (s i).Infinite
⊢ (⋃ i_1 ∈ insert i (t \ {i}), s i_1).encard = (s i).encard + ∑ᶠ (i_1 : ι) (_ : i_1 ∈ t \ {i}), (s i_1).encard
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
hs : Pairwise (Disjoint on s)
⊢ (⋃ i, s i).encard = (⋃ i ∈ univ, s i).encard

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
hs : Pairwise (Disjoint on s)
⊢ (⋃ i, s i).encard = (⋃ i ∈ univ, s i).encard
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'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
p : Finset (Fin n)
hp : p ∈ K.parts
⊢ t ≤ t'

Tactic:
]

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'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
p : Finset (Fin n)
hp : p ∈ K.parts
⊢ t ≤ t'
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
hvw : M.Adj v w
⊢ s(↑⟨v, ⋯⟩, w) = s(v, w)

Tactic:
]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
ha : M.Adj v w
⊢ s(w, v) = s(w, v)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
a b c : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
hs : G.IsNClique r (insert a s)
hc : c ∈ s
ha : a ∉ s
hd : ∀ w ∈ insert a s, w ≠ c → G.Adj w b
⊢ G.IsNClique r (insert b ((insert a s).erase c))

Tactic:
]

Goal state after:
α : Type u_1
a b c : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
hs : G.IsNClique r (insert a s)
hc : c ∈ s
ha : a ∉ s
hd : ∀ w ∈ insert a s, w ≠ c → G.Adj w b
⊢ G.IsNClique r (insert b ((insert a s).erase c))
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'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
this : Nonempty ↥(K.parts.pi fun x ↦ powersetCard t x)
⊢ t'.choose t ^ r * t ≤ t'.choose t ^ r * t

Tactic:
]

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
s : Finset ↑p₁
this : s.card ≤ (⋃ x ∈ ↑(Finset.image Subtype.val s), G.neighborSet x).ncard
⊢ s.card ≤ (s.biUnion fun x ↦ G.neighborFinset ↑x).card

Tactic:
]

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
s : Finset ↑p₁
this : s.card ≤ (⋃ x ∈ ↑(Finset.image Subtype.val s), G.neighborSet x).ncard
⊢ s.card ≤ (s.biUnion fun x ↦ G.neighborFinset ↑x).card
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
p2 : G.IsPathGraph3Compl v w₁ w₂
d1 : v ∉ s
d2 : v ∉ t
d3 : w₁ ∉ s
d4 : w₂ ∉ t
c1 : G.IsNClique (r + 1) (insert v s)
c2 : G.IsNClique (r + 1) (insert w₁ s)
c3 : G.IsNClique (r + 1) (insert v t)
c4 : G.IsNClique (r + 1) (insert w₂ t)
hk : #(s ∩ t) = k
⊢ #(s ∩ t) = k

Tactic:
]

Goal state after:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
p2 : G.IsPathGraph3Compl v w₁ w₂
d1 : v ∉ s
d2 : v ∉ t
d3 : w₁ ∉ s
d4 : w₂ ∉ t
c1 : G.IsNClique (r + 1) (insert v s)
c2 : G.IsNClique (r + 1) (insert w₁ s)
c3 : G.IsNClique (r + 1) (insert v t)
c4 : G.IsNClique (r + 1) (insert w₂ t)
hk : #(s ∩ t) = k
⊢ #(s ∩ t) = k
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'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
this : Nonempty ↥(K.parts.pi fun x ↦ powersetCard t x)
⊢ ↑(t'.choose t ^ r * t) * (↑t' - ↑t) ≤ ↑(#(filter K t)) * (↑t' - ↑t)

Tactic:
]

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'
ht_lt_t' : t < t'
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
hN : (↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) ≤ ↑n * (↑r * ↑t' * ε - ↑t)
this : Nonempty ↥(K.parts.pi fun x ↦ powersetCard t x)
⊢ ↑(t'.choose t ^ r * t) * (↑t' - ↑t) ≤ ↑(#(filter K t)) * (↑t' - ↑t)
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (⇑C) (insert w₁ ↑s) Set.univ
this : Set.SurjOn (⇑C) (insert w₂ ↑t) Set.univ
x : α
hx : x ∈ insert w₁ ↑s
hcx : C x = C v
y : α
hy : y ∈ insert w₂ ↑t
hcy : C y = C v
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (⇑C) (insert w₁ ↑s) Set.univ
this : Set.SurjOn (⇑C) (insert w₂ ↑t) Set.univ
x : α
hx : x ∈ insert w₁ ↑s
hcx : C x = C v
y : α
hy : y ∈ insert w₂ ↑t
hcy : C y = C v
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.inr
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd✝ : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : ∀ ⦃a : V⦄, a ∈ N.support → a ∉ N'.support
hmN : v ∈ N.verts
w : V
hw : (fun w ↦ N.Adj v w) w ∧ ∀ (y : V), (fun w ↦ N.Adj v w) y → y = w
y : V
h : N'.Adj v y
⊢ y = w

Tactic:
]

Goal state after:
case h.inr
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd✝ : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : ∀ ⦃a : V⦄, a ∈ N.support → a ∉ N'.support
hmN : v ∈ N.verts
w : V
hw : (fun w ↦ N.Adj v w) w ∧ ∀ (y : V), (fun w ↦ N.Adj v w) y → y = w
y : V
h : N'.Adj v y
⊢ y = w
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case inl
ε : ℝ
hε : 0 < ε
r t : ℕ
h0 : r + 1 ≤ 1 ∨ t = 0
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj],
      ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n → completeEquipartiteGraph (r + 1) t ⊑ G

Tactic:
]

Goal state after:
case inl
ε : ℝ
hε : 0 < ε
r t : ℕ
h0 : r + 1 ≤ 1 ∨ t = 0
⊢ ∀ᶠ (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.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case inl
ε : ℝ
hε : 0 < ε
r t : ℕ
h0 : r + 1 ≤ 1 ∨ t = 0
⊢ ∃ a,
    ∀ (b : ℕ),
      a ≤ b →
        ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
          ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑b → completeEquipartiteGraph (r + 1) t ⊑ G

Tactic:
]

Goal state after:
case inl
ε : ℝ
hε : 0 < ε
r t : ℕ
h0 : r + 1 ≤ 1 ∨ t = 0
⊢ ∃ a,
    ∀ (b : ℕ),
      a ≤ b →
        ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
          ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑b → completeEquipartiteGraph (r + 1) t ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
aux : ∀ {N N' : G.Subgraph}, N.IsMatching → Disjoint N.support N'.support → v ∈ N.verts → ∃! w, (N ⊔ N').Adj v w
hmM' : v ∈ M'.verts
⊢ ∃! w, (M' ⊔ M).Adj v w

Tactic:
]

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
aux : ∀ {N N' : G.Subgraph}, N.IsMatching → Disjoint N.support N'.support → v ∈ N.verts → ∃! w, (N ⊔ N').Adj v w
hmM' : v ∈ M'.verts
⊢ ∃! w, (M' ⊔ M).Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case inl
ε : ℝ
hε : 0 < ε
r t : ℕ
h0 : r + 1 ≤ 1 ∨ t = 0
n : ℕ
hn : (r + 1) * t ≤ n
G : SimpleGraph (Fin n)
x✝¹ : DecidableRel G.Adj
x✝ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
⊢ (r + 1) * t ≤ n

Tactic:
]

Goal state after:
case inl
ε : ℝ
hε : 0 < ε
r t : ℕ
h0 : r + 1 ≤ 1 ∨ t = 0
n : ℕ
hn : (r + 1) * t ≤ n
G : SimpleGraph (Fin n)
x✝¹ : DecidableRel G.Adj
x✝ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
⊢ (r + 1) * t ≤ n
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case inr
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
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

Tactic:
]

Goal state after:
case inr
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
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