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

Goal state before:
pp: case intro.refine_1
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this✝ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
v : V
⊢ W

Tactic:
exact
      (u (Opposite.op (singletonFinsubgraph v))).toFun
        ⟨v, by
          unfold singletonFinsubgraph
          simp⟩

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

Goal state before:
pp: case intro.refine_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this✝ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
⊢ ∀ {a b : V},
    G.Adj a b →
      F.Adj ((u (Opposite.op (singletonFinsubgraph a))).toFun ⟨a, ⋯⟩)
        ((u (Opposite.op (singletonFinsubgraph b))).toFun ⟨b, ⋯⟩)

Tactic:
·

Goal state after:
case intro.refine_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this✝ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
⊢ ∀ {a b : V},
    G.Adj a b →
      F.Adj ((u (Opposite.op (singletonFinsubgraph a))).toFun ⟨a, ⋯⟩)
        ((u (Opposite.op (singletonFinsubgraph b))).toFun ⟨b, ⋯⟩)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_2
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
G : SimpleGraph (Fin m ⊕ Fin n)
h_le : G ≤ completeBipartiteGraph (Fin m) (Fin n)
h_free : (completeBipartiteGraph (Fin s) (Fin t)).Free G
⊢ K.Free (SimpleGraph.map (⇑e₁.toEmbedding) G)

Tactic:
·

Goal state after:
case refine_2
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
G : SimpleGraph (Fin m ⊕ Fin n)
h_le : G ≤ completeBipartiteGraph (Fin m) (Fin n)
h_free : (completeBipartiteGraph (Fin s) (Fin t)).Free G
⊢ K.Free (SimpleGraph.map (⇑e₁.toEmbedding) G)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: case refine_1
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
⊢ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}.Nonempty

pp: case refine_2
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
m : ℕ
hm : m ∈ Set.Ici 2
hx : ↑(extremalNumber m H) / ↑(m.choose 2) = x
⊢ H.turanDensity + ε ≤ x

Tactic:
·

Goal state after:
case refine_1
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
⊢ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}.Nonempty
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'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
⊢ ∑ x ∈ K.parts \ {p}, #({v_1 ∈ id x | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v}) ≤ #K.verts - t'

pp: case h₂
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
⊢ #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v}) < t

Tactic:
·

Goal state after:
case h₁
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
⊢ ∑ x ∈ K.parts \ {p}, #({v_1 ∈ id x | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v}) ≤ #K.verts - t'
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
m : ℕ
hm : m ∈ Set.Ici 2
hx : ↑(extremalNumber m H) / ↑(m.choose 2) = x
n : ℕ
hn : m ≤ n
G : SimpleGraph (Fin n)
w✝ : DecidableRel G.Adj
hcard_edges : ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(n.choose 2)
h_free : H.Free G
⊢ H.turanDensity + ε ≤ ↑(extremalNumber n H) / ↑(n.choose 2)

pp: W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
m : ℕ
hm : m ∈ Set.Ici 2
hx : ↑(extremalNumber m H) / ↑(m.choose 2) = x
n : ℕ
hn : m ≤ n
G : SimpleGraph (Fin n)
w✝ : DecidableRel G.Adj
hcard_edges : ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(n.choose 2)
h_free : H.Free G
⊢ ↑(extremalNumber n H) / ↑(n.choose 2) ≤ ↑(extremalNumber m H) / ↑(m.choose 2)

Tactic:
·

Goal state after:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
m : ℕ
hm : m ∈ Set.Ici 2
hx : ↑(extremalNumber m H) / ↑(m.choose 2) = x
n : ℕ
hn : m ≤ n
G : SimpleGraph (Fin n)
w✝ : DecidableRel G.Adj
hcard_edges : ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(n.choose 2)
h_free : H.Free G
⊢ H.turanDensity + ε ≤ ↑(extremalNumber n H) / ↑(n.choose 2)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_1
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
G : SimpleGraph (V ⊕ W)
h_le : G ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free G
x✝¹ x✝ : V ⊕ W
hadj : G.Adj x✝¹ x✝
⊢ (SimpleGraph.comap (⇑e₁.toEmbedding) (completeBipartiteGraph (Fin m) (Fin n))).Adj x✝¹ x✝

pp: case refine_2
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
G : SimpleGraph (V ⊕ W)
h_le : G ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free G
⊢ K.Free (SimpleGraph.map (⇑e₁.toEmbedding) G)

Tactic:
·

Goal state after:
case refine_1
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
G : SimpleGraph (V ⊕ W)
h_le : G ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free G
x✝¹ x✝ : V ⊕ W
hadj : G.Adj x✝¹ x✝
⊢ (SimpleGraph.comap (⇑e₁.toEmbedding) (completeBipartiteGraph (Fin m) (Fin n))).Adj x✝¹ x✝
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'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
⊢ #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v}) < t

Tactic:
·

Goal state after:
case h₂
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs : ∀ (x : Finset (Fin n)), x ∉ powersetCard t p ∨ ∃ x_1 ∈ x, ¬G.Adj v x_1
⊢ #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v}) < t
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_2
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
G : SimpleGraph (V ⊕ W)
h_le : G ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free G
⊢ K.Free (SimpleGraph.map (⇑e₁.toEmbedding) G)

Tactic:
·

Goal state after:
case refine_2
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
G : SimpleGraph (V ⊕ W)
h_le : G ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free G
⊢ K.Free (SimpleGraph.map (⇑e₁.toEmbedding) G)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
m : ℕ
hm : m ∈ Set.Ici 2
hx : ↑(extremalNumber m H) / ↑(m.choose 2) = x
n : ℕ
hn : m ≤ n
G : SimpleGraph (Fin n)
w✝ : DecidableRel G.Adj
hcard_edges : ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(n.choose 2)
h_free : H.Free G
⊢ ↑(extremalNumber n H) / ↑(n.choose 2) ≤ ↑(extremalNumber m H) / ↑(m.choose 2)

Tactic:
·

Goal state after:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
m : ℕ
hm : m ∈ Set.Ici 2
hx : ↑(extremalNumber m H) / ↑(m.choose 2) = x
n : ℕ
hn : m ≤ n
G : SimpleGraph (Fin n)
w✝ : DecidableRel G.Adj
hcard_edges : ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(n.choose 2)
h_free : H.Free G
⊢ ↑(extremalNumber n H) / ↑(n.choose 2) ≤ ↑(extremalNumber m H) / ↑(m.choose 2)
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ (∃ a w, w.IsCycle ∧ G.egirth = ↑w.length) ↔ ¬G.IsAcyclic

Tactic:
refine ⟨?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
⊢ (∃ a w, w.IsCycle ∧ G.egirth = ↑w.length) → ¬G.IsAcyclic

case refine_2
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
⊢ ∃ a w, w.IsCycle ∧ G.egirth = ↑w.length
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
⊢ (∃ a w, w.IsCycle ∧ G.egirth = ↑w.length) → ¬G.IsAcyclic

pp: case refine_2
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
⊢ ∃ a w, w.IsCycle ∧ G.egirth = ↑w.length

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
⊢ (∃ a w, w.IsCycle ∧ G.egirth = ↑w.length) → ¬G.IsAcyclic
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
⊢ ∃ a w, w.IsCycle ∧ G.egirth = ↑w.length

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
⊢ ∃ a w, w.IsCycle ∧ G.egirth = ↑w.length
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

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 ∈ filter K t
⊢ ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) ≤ ↑(#K.verts)

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.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 ∈ filter K t
⊢ ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree v) ≤ ↑(#K.verts)

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
G : SimpleGraph α
G' : SimpleGraph β
h : G ⊑ G'
hacyc : G.IsAcyclic
⊢ G'.egirth ≤ G.egirth

pp: case neg
α : Type u_1
β : Type u_2
G : SimpleGraph α
G' : SimpleGraph β
h : G ⊑ G'
hacyc : ¬G.IsAcyclic
⊢ G'.egirth ≤ G.egirth

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
G : SimpleGraph α
G' : SimpleGraph β
h : G ⊑ G'
hacyc : G.IsAcyclic
⊢ G'.egirth ≤ G.egirth
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.girth = 0
⊢ ¬3 ≤ G.girth

Tactic:
by lia

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 = s.ncard

pp: case inr
α : Type u_1
s : Set α
hs : s.Finite
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard

Tactic:
·

Goal state after:
case inl
α : Type u_1
s : Set α
hs : s.Infinite
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard
Module: Mathlib.Data.Set.Card.Arithmetic

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

pp: case neg
α : Type u_1
s : Set α
hs : s.Infinite
h : ¬1 = 0
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
s : Set α
hs : s.Infinite
h : 1 = 0
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = 0
Module: Mathlib.Data.Set.Card.Arithmetic

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

Tactic:
·

Goal state after:
case neg
α : Type u_1
s : Set α
hs : s.Infinite
h : ¬1 = 0
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = 0
Module: Mathlib.Data.Set.Card.Arithmetic

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

Tactic:
·

Goal state after:
case inr
α : Type u_1
s : Set α
hs : s.Finite
⊢ ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ Subtype.val '' ⇑f ⁻¹' range Sum.inl ∪ Subtype.val '' ⇑f ⁻¹' range Sum.inr = s

pp: case refine_2
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ Disjoint (Subtype.val '' ⇑f ⁻¹' range Sum.inl) (Subtype.val '' ⇑f ⁻¹' range Sum.inr)

pp: case refine_3
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ #↑(Subtype.val '' ⇑f ⁻¹' range Sum.inl) = #↑(Subtype.val '' ⇑f ⁻¹' range Sum.inr)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ Subtype.val '' ⇑f ⁻¹' range Sum.inl ∪ Subtype.val '' ⇑f ⁻¹' range Sum.inr = s
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ Disjoint (Subtype.val '' ⇑f ⁻¹' range Sum.inl) (Subtype.val '' ⇑f ⁻¹' range Sum.inr)

pp: case refine_3
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ #↑(Subtype.val '' ⇑f ⁻¹' range Sum.inl) = #↑(Subtype.val '' ⇑f ⁻¹' range Sum.inr)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ Disjoint (Subtype.val '' ⇑f ⁻¹' range Sum.inl) (Subtype.val '' ⇑f ⁻¹' range Sum.inr)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case refine_3
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ #↑(Subtype.val '' ⇑f ⁻¹' range Sum.inl) = #↑(Subtype.val '' ⇑f ⁻¹' range Sum.inr)

Tactic:
·

Goal state after:
case refine_3
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ #↑(Subtype.val '' ⇑f ⁻¹' range Sum.inl) = #↑(Subtype.val '' ⇑f ⁻¹' range Sum.inr)
Module: Mathlib.Data.Set.Card.Arithmetic

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

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

Tactic:
·

Goal state after:
case inl
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Infinite
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u
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 ∪ u).Finite
⊢ Even (t ∪ u).ncard

pp: case mpr.inr
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hnfin : (t ∪ u).Infinite
⊢ 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 ∪ u).Finite
⊢ Even (t ∪ u).ncard
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case mpr.inr
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hnfin : (t ∪ u).Infinite
⊢ Even (t ∪ u).ncard

Tactic:
·

Goal state after:
case mpr.inr
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hnfin : (t ∪ u).Infinite
⊢ Even (t ∪ u).ncard
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case hb
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
⊢ G.bipartiteDoubleCover ∈
    {G | G ≤ completeBipartiteGraph (Fin n) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}

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 hb
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
⊢ G.bipartiteDoubleCover ∈
    {G | G ≤ completeBipartiteGraph (Fin n) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}
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
⊢ (⋃ i ∈ t, s i).encard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard

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 pos
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
h : ∀ i ∈ t, (s i).Finite
⊢ (⋃ i ∈ t, s i).encard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard