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

Goal state before:
pp: case mp
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
⊢ G ⊴ H → ∃ H' _e, H'.IsInduced

pp: case mpr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
⊢ (∃ H' _e, H'.IsInduced) → G ⊴ H

Tactic:
·

Goal state after:
case mp
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
⊢ G ⊴ H → ∃ H' _e, H'.IsInduced
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case mpr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
⊢ (∃ H' _e, H'.IsInduced) → G ⊴ H

Tactic:
·

Goal state after:
case mpr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
⊢ (∃ H' _e, H'.IsInduced) → G ⊴ H
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case refine_4
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
v w : W
⊢ (Subgraph.map f H).Adj v w → H'.Adj v w

Tactic:
·

Goal state after:
case refine_4
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
v w : W
⊢ (Subgraph.map f H).Adj v w → H'.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
B : Finset α
hB : B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts
h₁ : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ #(B \ {A ∈ (equitabilise ⋯).parts | A ⊆ B}.biUnion id) ≤ m

pp: case neg
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
B : Finset α
hB : B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts
h₁ : ¬#U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ #(B \ {A ∈ (equitabilise ⋯).parts | A ⊆ B}.biUnion id) ≤ m

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
B : Finset α
hB : B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts
h₁ : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ #(B \ {A ∈ (equitabilise ⋯).parts | A ⊆ B}.biUnion id) ≤ m
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
B : Finset α
hB : B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts
h₁ : ¬#U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ #(B \ {A ∈ (equitabilise ⋯).parts | A ⊆ B}.biUnion id) ≤ m

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
B : Finset α
hB : B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts
h₁ : ¬#U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
⊢ #(B \ {A ∈ (equitabilise ⋯).parts | A ⊆ B}.biUnion id) ≤ m
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case inl
V : Type u_1
W : Type u_2
G : SimpleGraph V
hHG : ⊥.Free G
⊢ G.killCopies ⊥ = G

pp: case inr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hHG : H.Free G
hH : H ≠ ⊥
⊢ G.killCopies H = G

Tactic:
·

Goal state after:
case inl
V : Type u_1
W : Type u_2
G : SimpleGraph V
hHG : ⊥.Free G
⊢ G.killCopies ⊥ = G
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case inr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hHG : H.Free G
hH : H ≠ ⊥
⊢ G.killCopies H = G

Tactic:
·

Goal state after:
case inr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hHG : H.Free G
hH : H ≠ ⊥
⊢ G.killCopies H = G
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case refine_1
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Function.Injective fun H ↦
    { verts := ↑(↑H).1, Adj := fun a b ↦ (↑H).2 a b = true, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }

pp: case refine_2
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
H : G.Subgraph
⊢ ∃ a, (fun H ↦ { verts := ↑(↑H).1, Adj := fun a b ↦ (↑H).2 a b = true, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }) a = H

Tactic:
·

Goal state after:
case refine_1
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Function.Injective fun H ↦
    { verts := ↑(↑H).1, Adj := fun a b ↦ (↑H).2 a b = true, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case refine_2
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
H : G.Subgraph
⊢ ∃ a, (fun H ↦ { verts := ↑(↑H).1, Adj := fun a b ↦ (↑H).2 a b = true, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }) a = H

Tactic:
·

Goal state after:
case refine_2
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
H : G.Subgraph
⊢ ∃ a, (fun H ↦ { verts := ↑(↑H).1, Adj := fun a b ↦ (↑H).2 a b = true, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }) a = H
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ 0 < ε

pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ 2 ^ #P.parts * ↑m / ↑(#U) ≤ ε * (ε / 10)

Tactic:
·

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ 0 < ε
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case inl
V : Type u_1
W : Type u_2
G : SimpleGraph V
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
⊢ #G.edgeFinset - G.copyCount ⊥ ≤ #(G.killCopies ⊥).edgeFinset

pp: case inr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
⊢ #G.edgeFinset - G.copyCount H ≤ #(G.killCopies H).edgeFinset

Tactic:
·

Goal state after:
case inl
V : Type u_1
W : Type u_2
G : SimpleGraph V
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
⊢ #G.edgeFinset - G.copyCount ⊥ ≤ #(G.killCopies ⊥).edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case inr.calc_1
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
⊢ #G.edgeFinset - G.copyCount H = #G.edgeFinset - Fintype.card { G' // Nonempty (H ≃g G'.coe) }

pp: case inr.calc_2
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
⊢ #(G.edgeFinset \ (Set.range f).toFinset) = #(G.killCopies H).edgeFinset

Tactic:
·

Goal state after:
case inr.calc_1
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
⊢ #G.edgeFinset - G.copyCount H = #G.edgeFinset - Fintype.card { G' // Nonempty (H ≃g G'.coe) }
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
hG : G'.verts.Subsingleton
hv : v ∈ G'.verts
⊢ G'.degree v = 0

pp: case neg
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
hG : G'.verts.Subsingleton
hv : v ∉ G'.verts
⊢ G'.degree v = 0

Tactic:
·

Goal state after:
case pos
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
hG : G'.verts.Subsingleton
hv : v ∈ G'.verts
⊢ G'.degree v = 0
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
hG : G'.verts.Subsingleton
hv : v ∉ G'.verts
⊢ G'.degree v = 0

Tactic:
·

Goal state after:
case neg
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝ : Fintype ↑(G'.neighborSet v)
hG : G'.verts.Subsingleton
hv : v ∉ G'.verts
⊢ G'.degree v = 0
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case left
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ (G.singletonSubgraph v).verts ⊆ H.verts

pp: case right
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ ∀ ⦃v_1 w : V⦄, (G.singletonSubgraph v).Adj v_1 w → H.Adj v_1 w

Tactic:
·

Goal state after:
case left
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ (G.singletonSubgraph v).verts ⊆ H.verts
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ ∀ ⦃v_1 w : V⦄, (G.singletonSubgraph v).Adj v_1 w → H.Adj v_1 w

Tactic:
·

Goal state after:
case right
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ ∀ ⦃v_1 w : V⦄, (G.singletonSubgraph v).Adj v_1 w → H.Adj v_1 w
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝ : V
⊢ x✝ ∈ H.verts ↔ x✝ ∈ (G.singletonSubgraph v).verts

pp: case Adj
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ H.Adj x✝¹ x✝ ↔ (G.singletonSubgraph v).Adj x✝¹ x✝

Tactic:
·

Goal state after:
case verts
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝ : V
⊢ x✝ ∈ H.verts ↔ x✝ ∈ (G.singletonSubgraph v).verts
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ H.Adj x✝¹ x✝ ↔ (G.singletonSubgraph v).Adj x✝¹ x✝

Tactic:
·

Goal state after:
case Adj
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ H.Adj x✝¹ x✝ ↔ (G.singletonSubgraph v).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case left
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ (G.subgraphOfAdj ⋯).verts ⊆ H.verts

pp: case right
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ ∀ ⦃v_1 w_1 : V⦄, (G.subgraphOfAdj ⋯).Adj v_1 w_1 → H.Adj v_1 w_1

Tactic:
·

Goal state after:
case left
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ (G.subgraphOfAdj ⋯).verts ⊆ H.verts
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ ∀ ⦃v_1 w_1 : V⦄, (G.subgraphOfAdj ⋯).Adj v_1 w_1 → H.Adj v_1 w_1

Tactic:
·

Goal state after:
case right
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ ∀ ⦃v_1 w_1 : V⦄, (G.subgraphOfAdj ⋯).Adj v_1 w_1 → H.Adj v_1 w_1
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).neighborSet v = {w}

Tactic:
ext u
  suffices w = u ↔ u = w by simpa [hvw.ne.symm] using this
  rw [eq_comm]

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

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x✝ : ↑G'.verts
⊢ x✝ ∈ (Subgraph.restrict (Subgraph.coeSubgraph G'')).verts ↔ x✝ ∈ G''.verts

pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x✝¹ x✝ : ↑G'.verts
⊢ (Subgraph.restrict (Subgraph.coeSubgraph G'')).Adj x✝¹ x✝ ↔ G''.Adj x✝¹ x✝

Tactic:
·

Goal state after:
case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x✝ : ↑G'.verts
⊢ x✝ ∈ (Subgraph.restrict (Subgraph.coeSubgraph G'')).verts ↔ x✝ ∈ G''.verts
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x✝¹ x✝ : ↑G'.verts
⊢ (Subgraph.restrict (Subgraph.coeSubgraph G'')).Adj x✝¹ x✝ ↔ G''.Adj x✝¹ x✝

Tactic:
·

Goal state after:
case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x✝¹ x✝ : ↑G'.verts
⊢ (Subgraph.restrict (Subgraph.coeSubgraph G'')).Adj x✝¹ x✝ ↔ G''.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case left
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
⊢ (Subgraph.coeSubgraph H').verts ⊆ H.verts

pp: case right
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
⊢ ∀ ⦃v w : V⦄, (Subgraph.coeSubgraph H').Adj v w → H.Adj v w

Tactic:
·

Goal state after:
case left
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
⊢ (Subgraph.coeSubgraph H').verts ⊆ H.verts
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
⊢ ∀ ⦃v w : V⦄, (Subgraph.coeSubgraph H').Adj v w → H.Adj v w

Tactic:
·

Goal state after:
case right
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
⊢ ∀ ⦃v w : V⦄, (Subgraph.coeSubgraph H').Adj v w → H.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝ : V
⊢ x✝ ∈ (Subgraph.coeSubgraph (Subgraph.restrict H')).verts ↔ x✝ ∈ (H ⊓ H').verts

pp: case Adj
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝¹ x✝ : V
⊢ (Subgraph.coeSubgraph (Subgraph.restrict H')).Adj x✝¹ x✝ ↔ (H ⊓ H').Adj x✝¹ x✝

Tactic:
·

Goal state after:
case verts
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝ : V
⊢ x✝ ∈ (Subgraph.coeSubgraph (Subgraph.restrict H')).verts ↔ x✝ ∈ (H ⊓ H').verts
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝¹ x✝ : V
⊢ (Subgraph.coeSubgraph (Subgraph.restrict H')).Adj x✝¹ x✝ ↔ (H ⊓ H').Adj x✝¹ x✝

Tactic:
·

Goal state after:
case Adj
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝¹ x✝ : V
⊢ (Subgraph.coeSubgraph (Subgraph.restrict H')).Adj x✝¹ x✝ ↔ (H ⊓ H').Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
v w : V
h : v = w
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w

pp: case inr
V : Type u_1
G : SimpleGraph V
v w : V
h : v ≠ w
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w

Tactic:
·

Goal state after:
case inl
V : Type u_1
G : SimpleGraph V
v w : V
h : v = w
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
v w : V
h : v ≠ w
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w

Tactic:
·

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
v w : V
h : v ≠ w
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
u : V
⊢ Disjoint G (edge u u) ↔ ¬G.Adj u u

pp: case inr
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v
⊢ Disjoint G (edge u v) ↔ ¬G.Adj u v

Tactic:
·

Goal state after:
case inl
V : Type u_1
G : SimpleGraph V
u : V
⊢ Disjoint G (edge u u) ↔ ¬G.Adj u u
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
⊢ s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s → ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)

pp: case mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
⊢ (∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)) → s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s

Tactic:
·

Goal state after:
case mp
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
⊢ s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s → ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
⊢ (∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)) → s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s

Tactic:
·

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
⊢ (∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)) → s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this✝ : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
this : 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2
⊢ 2 ^ (#P.parts - 1) * ↑m * (↑(#U) * ε) ≤ 2 ^ (#P.parts - 1) * ↑m * (2 * ↑(#(G.nonuniformWitness ε U V)))

pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this✝ : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
this : 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2
⊢ 0 < ↑(#U) * ε

Tactic:
·

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this✝ : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
this : 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2
⊢ 2 ^ (#P.parts - 1) * ↑m * (↑(#U) * ε) ≤ 2 ^ (#P.parts - 1) * ↑m * (2 * ↑(#(G.nonuniformWitness ε U V)))
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case left
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ (G'.induce s).verts ⊆ (G''.induce s').verts

pp: case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, (G'.induce s).Adj v w → (G''.induce s').Adj v w

Tactic:
·

Goal state after:
case left
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ (G'.induce s).verts ⊆ (G''.induce s').verts
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, (G'.induce s).Adj v w → (G''.induce s').Adj v w

Tactic:
·

Goal state after:
case right
V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, (G'.induce s).Adj v w → (G''.induce s').Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ : V
⊢ x✝ ∈ (G'.induce G'.verts).verts ↔ x✝ ∈ G'.verts

pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ (G'.induce G'.verts).Adj x✝¹ x✝ ↔ G'.Adj x✝¹ x✝

Tactic:
·

Goal state after:
case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ : V
⊢ x✝ ∈ (G'.induce G'.verts).verts ↔ x✝ ∈ G'.verts
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ (G'.induce G'.verts).Adj x✝¹ x✝ ↔ G'.Adj x✝¹ x✝

Tactic:
·

Goal state after:
case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ (G'.induce G'.verts).Adj x✝¹ x✝ ↔ G'.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case left
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ (G'.induce s ⊔ G'.induce s').verts ⊆ (G'.induce (s ∪ s')).verts

pp: case right
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ ∀ ⦃v w : V⦄, (G'.induce s ⊔ G'.induce s').Adj v w → (G'.induce (s ∪ s')).Adj v w

Tactic:
·

Goal state after:
case left
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ (G'.induce s ⊔ G'.induce s').verts ⊆ (G'.induce (s ∪ s')).verts
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ ∀ ⦃v w : V⦄, (G'.induce s ⊔ G'.induce s').Adj v w → (G'.induce (s ∪ s')).Adj v w

Tactic:
·

Goal state after:
case right
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ ∀ ⦃v w : V⦄, (G'.induce s ⊔ G'.induce s').Adj v w → (G'.induce (s ∪ s')).Adj v w