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

Goal state before:
pp: case h
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 ≤ #G.bipartiteDoubleCover.edgeFinset

Tactic:
·

Goal state after:
case h
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 ≤ #G.bipartiteDoubleCover.edgeFinset
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
h : ∃ i ∈ t, (s i).Infinite
⊢ (⋃ i ∈ t, s i).encard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard

Tactic:
·

Goal state after:
case neg
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
h : ∃ i ∈ t, (s i).Infinite
⊢ (⋃ i ∈ t, s i).encard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
v w : V
h✝ : v ∈ p
h : f ⟨v, h✝⟩ = w
⊢ G.Adj v w

pp: case pos
V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
v w : V
h✝¹ : v ∉ p
h✝ : w ∈ p
h : f ⟨w, h✝⟩ = v
⊢ G.Adj v w

Tactic:
·

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
v w : V
h✝ : v ∈ p
h : f ⟨v, h✝⟩ = w
⊢ G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
v w : V
h✝¹ : v ∉ p
h✝ : w ∈ p
h : f ⟨w, h✝⟩ = v
⊢ G.Adj v w

Tactic:
·

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
p : Set V
inst✝ : DecidablePred fun x ↦ x ∈ p
f : ↑p → V
h₁ : ∀ (x : ↑p), f x ∉ p
h₂ : ∀ (x : ↑p), G.Adj (↑x) (f x)
v w : V
h✝¹ : v ∉ p
h✝ : w ∈ p
h : f ⟨w, h✝⟩ = v
⊢ G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case inl
α : Type u_1
b✝ : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h2 : G.IsNClique r (insert b✝ s)
h3 : b✝ ∉ s
b : α
h1 : G.IsNClique r (insert b s)
ha : G.Adj b b✝
hb : b ∈ insert b s
⊢ G.Adj b✝ b

pp: case inr
α : Type u_1
a b✝ : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h1 : G.IsNClique r (insert a s)
h2 : G.IsNClique r (insert b✝ s)
h3 : b✝ ∉ s
ha : G.Adj a b✝
b : α
hb : b ∈ insert a s
h : b ∈ s
⊢ G.Adj b✝ b

Tactic:
·

Goal state after:
case inl
α : Type u_1
b✝ : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h2 : G.IsNClique r (insert b✝ s)
h3 : b✝ ∉ s
b : α
h1 : G.IsNClique r (insert b s)
ha : G.Adj b b✝
hb : b ∈ insert b s
⊢ G.Adj b✝ b
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case inr
α : Type u_1
a b✝ : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h1 : G.IsNClique r (insert a s)
h2 : G.IsNClique r (insert b✝ s)
h3 : b✝ ∉ s
ha : G.Adj a b✝
b : α
hb : b ∈ insert a s
h : b ∈ s
⊢ G.Adj b✝ b

Tactic:
·

Goal state after:
case inr
α : Type u_1
a b✝ : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h1 : G.IsNClique r (insert a s)
h2 : G.IsNClique r (insert b✝ s)
h3 : b✝ ∉ s
ha : G.Adj a b✝
b : α
hb : b ∈ insert a s
h : b ∈ s
⊢ G.Adj b✝ b
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
w : ↑M.verts
hw : w ∈ h.toEdge ⁻¹' {⟨s(u, v), huv⟩}
⊢ w ∈ {⟨u, ⋯⟩, ⟨v, ⋯⟩}

pp: case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
w : ↑M.verts
hw : w ∈ {⟨u, ⋯⟩, ⟨v, ⋯⟩}
⊢ w ∈ h.toEdge ⁻¹' {⟨s(u, v), huv⟩}

Tactic:
·

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
w : ↑M.verts
hw : w ∈ h.toEdge ⁻¹' {⟨s(u, v), huv⟩}
⊢ w ∈ {⟨u, ⋯⟩, ⟨v, ⋯⟩}
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
w : ↑M.verts
hw : w ∈ {⟨u, ⋯⟩, ⟨v, ⋯⟩}
⊢ w ∈ h.toEdge ⁻¹' {⟨s(u, v), huv⟩}

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
w : ↑M.verts
hw : w ∈ {⟨u, ⋯⟩, ⟨v, ⋯⟩}
⊢ w ∈ h.toEdge ⁻¹' {⟨s(u, v), huv⟩}
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case refine_2.inl
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
⊢ ⟨u, ⋯⟩ ∈ h.toEdge ⁻¹' {⟨s(u, v), huv⟩}

pp: case refine_2.inr
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
⊢ ⟨v, ⋯⟩ ∈ h.toEdge ⁻¹' {⟨s(u, v), huv⟩}

Tactic:
·

Goal state after:
case refine_2.inl
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
⊢ ⟨u, ⋯⟩ ∈ h.toEdge ⁻¹' {⟨s(u, v), huv⟩}
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case refine_2.inr
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
⊢ ⟨v, ⋯⟩ ∈ h.toEdge ⁻¹' {⟨s(u, v), huv⟩}

Tactic:
·

Goal state after:
case refine_2.inr
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
⊢ ⟨v, ⋯⟩ ∈ h.toEdge ⁻¹' {⟨s(u, v), huv⟩}
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: case h.inl
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : ↑p₁ → V
hf₁ : Injective f
hf₂ : ∀ (x : ↑p₁), f x ∈ G.neighborFinset ↑x
this : ∀ (x : ↑p₁), f x ∉ p₁
v : V
h' : v ∈ p₁
⊢ ∃! w, if h : v ∈ p₁ then f ⟨v, h⟩ = w else if h : w ∈ p₁ then f ⟨w, h⟩ = v else False

pp: case h.inr
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : ↑p₁ → V
hf₁ : Injective f
hf₂ : ∀ (x : ↑p₁), f x ∈ G.neighborFinset ↑x
this : ∀ (x : ↑p₁), f x ∉ p₁
v x : V
hx₁ : x ∈ p₁
hx₂ : f ⟨x, hx₁⟩ = v
⊢ ∃! w, if h : v ∈ p₁ then f ⟨v, h⟩ = w else if h : w ∈ p₁ then f ⟨w, h⟩ = v else False

Tactic:
·

Goal state after:
case h.inl
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : ↑p₁ → V
hf₁ : Injective f
hf₂ : ∀ (x : ↑p₁), f x ∈ G.neighborFinset ↑x
this : ∀ (x : ↑p₁), f x ∉ p₁
v : V
h' : v ∈ p₁
⊢ ∃! w, if h : v ∈ p₁ then f ⟨v, h⟩ = w else if h : w ∈ p₁ then f ⟨w, h⟩ = v else False
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: case h.inr
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : ↑p₁ → V
hf₁ : Injective f
hf₂ : ∀ (x : ↑p₁), f x ∈ G.neighborFinset ↑x
this : ∀ (x : ↑p₁), f x ∉ p₁
v x : V
hx₁ : x ∈ p₁
hx₂ : f ⟨x, hx₁⟩ = v
⊢ ∃! w, if h : v ∈ p₁ then f ⟨v, h⟩ = w else if h : w ∈ p₁ then f ⟨w, h⟩ = v else False

Tactic:
·

Goal state after:
case h.inr
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : ↑p₁ → V
hf₁ : Injective f
hf₂ : ∀ (x : ↑p₁), f x ∈ G.neighborFinset ↑x
this : ∀ (x : ↑p₁), f x ∉ p₁
v x : V
hx₁ : x ∈ p₁
hx₂ : f ⟨x, hx₁⟩ = v
⊢ ∃! w, if h : v ∈ p₁ then f ⟨v, h⟩ = w else if h : w ∈ p₁ then f ⟨w, h⟩ = v else False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

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

pp: case inr
ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : r ≠ 0
ht_pos : 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 = 0 ∨ 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.Hall

Goal state before:
pp: case refine_1
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
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ Injective f'

pp: case refine_2
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
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ Injective g'

pp: case refine_3
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
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ ∀ (a : ↑p₁), G.Adj ↑a ↑(f' a)

pp: case refine_4
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
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ ∀ (b : ↑p₂), G.Adj ↑(g' b) ↑b

Tactic:
·

Goal state after:
case refine_1
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
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ Injective f'
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: case refine_2
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
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ Injective g'

pp: case refine_3
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
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ ∀ (a : ↑p₁), G.Adj ↑a ↑(f' a)

pp: case refine_4
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
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ ∀ (b : ↑p₂), G.Adj ↑(g' b) ↑b

Tactic:
·

Goal state after:
case refine_2
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
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ Injective g'
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: case refine_3
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
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ ∀ (a : ↑p₁), G.Adj ↑a ↑(f' a)

pp: case refine_4
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
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ ∀ (b : ↑p₂), G.Adj ↑(g' b) ↑b

Tactic:
·

Goal state after:
case refine_3
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
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ ∀ (a : ↑p₁), G.Adj ↑a ↑(f' a)
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: case refine_4
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
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ ∀ (b : ↑p₂), G.Adj ↑(g' b) ↑b

Tactic:
·

Goal state after:
case refine_4
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
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this✝¹ : ∀ x ∈ p₁, f x ∉ p₁
this✝ : ∀ x ∈ p₂, f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : ↑p₁ → ↑p₂ := fun x ↦ ⟨f ↑x, ⋯⟩
g' : ↑p₂ → ↑p₁ := fun x ↦ ⟨f ↑x, ⋯⟩
⊢ ∀ (b : ↑p₂), G.Adj ↑(g' b) ↑b
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

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

Goal state before:
pp: case pos
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'
⊢ y = w

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'
⊢ y = w

Tactic:
·

Goal state after:
case pos
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'
⊢ y = w
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: case h.isTrue
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₁
⊢ ∃! w, ↑(b ⟨v, ⋯⟩) = w

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₁
⊢ ∃! w, ∃ (h : w ∈ p₁), ↑(b ⟨w, ⋯⟩) = v

Tactic:
·

Goal state after:
case h.isTrue
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₁
⊢ ∃! w, ↑(b ⟨v, ⋯⟩) = w
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'
⊢ y = w

Tactic:
·

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'
⊢ y = w
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₁
⊢ ∃! w, ∃ (h : w ∈ p₁), ↑(b ⟨w, ⋯⟩) = v

Tactic:
·

Goal state after:
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₁
⊢ ∃! w, ∃ (h : w ∈ p₁), ↑(b ⟨w, ⋯⟩) = v
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
h : IsEmpty α
⊢ p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
h : Nonempty α
⊢ p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
h : IsEmpty α
⊢ p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.refine_1
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) y → y = w
⊢ (fun w ↦ (Subgraph.coeSubgraph M).Adj v✝ w) ↑w

pp: case h.refine_2
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) y → y = w
y : V
hy : (fun w ↦ (Subgraph.coeSubgraph M).Adj v✝ w) y
⊢ y = ↑w

Tactic:
·

Goal state after:
case h.refine_1
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) y → y = w
⊢ (fun w ↦ (Subgraph.coeSubgraph M).Adj v✝ w) ↑w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h.refine_2
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) y → y = w
y : V
hy : (fun w ↦ (Subgraph.coeSubgraph M).Adj v✝ w) y
⊢ y = ↑w

Tactic:
·

Goal state after:
case h.refine_2
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v✝ : V
hv : v✝ ∈ (Subgraph.coeSubgraph M).verts
w : ↑G'.verts
hw : (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) w ∧ ∀ (y : ↑G'.verts), (fun w ↦ M.Adj ⟨v✝, ⋯⟩ w) y → y = w
y : V
hy : (fun w ↦ (Subgraph.coeSubgraph M).Adj v✝ w) y
⊢ y = ↑w
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
β : Type u_2
inst✝ : DecidableEq β
H : SimpleGraph β
a : α
f : G →g H
hf : Bijective ⇑f
x : α
hp : nil.IsHamiltonianCycle
__IsCycle✝ : (Walk.map f nil).IsCycle := IsCycle.map (Bijective.injective hf) (isCycle hp)
⊢ List.count (f x) (Walk.map f nil).tail.support = 1

pp: case cons
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
β : Type u_2
inst✝ : DecidableEq β
H : SimpleGraph β
a : α
f : G →g H
hf : Bijective ⇑f
x v✝ : α
y : G.Adj a v✝
p : G.Walk v✝ a
hp : (cons y p).IsHamiltonianCycle
__IsCycle✝ : (Walk.map f (cons y p)).IsCycle := IsCycle.map (Bijective.injective hf) (isCycle hp)
⊢ List.count (f x) (Walk.map f (cons y p)).tail.support = 1

Tactic:
·

Goal state after:
case nil
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
β : Type u_2
inst✝ : DecidableEq β
H : SimpleGraph β
a : α
f : G →g H
hf : Bijective ⇑f
x : α
hp : nil.IsHamiltonianCycle
__IsCycle✝ : (Walk.map f nil).IsCycle := IsCycle.map (Bijective.injective hf) (isCycle hp)
⊢ List.count (f x) (Walk.map f nil).tail.support = 1