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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : ¬0 < a
⊢ 0 < m + 1 ∧ m + 1 ≤ m + 1 ∧ m + 1 ≤ a * m + b * (m + 1) ∧ a * m + (b - 1) * (m + 1) = a * m + b * (m + 1) - (m + 1)

Tactic:
rw [tsub_mul, one_mul]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
h : ¬0 < a
⊢ 0 < m + 1 ∧
    m + 1 ≤ m + 1 ∧ m + 1 ≤ a * m + b * (m + 1) ∧ a * m + (b * (m + 1) - (m + 1)) = a * m + b * (m + 1) - (m + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
⊢ 0 < n ∧
    n ≤ m + 1 ∧
      n ≤ a * m + b * (m + 1) ∧ (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n

Tactic:
rw [hn, ← hs]
    split_ifs with h <;> rw [tsub_mul, one_mul]
    · refine ⟨m_pos, le_succ _, le_add_right (Nat.le_mul_of_pos_left _ ‹0 < a›), ?_⟩
      rw [tsub_add_eq_add_tsub (Nat.le_mul_of_pos_left _ h)]
    · refine ⟨succ_pos', le_rfl,
        le_add_left (Nat.le_mul_of_pos_left _ <| hab.resolve_left ‹¬0 < a›), ?_⟩
      rw [← add_tsub_assoc_of_le (Nat.le_mul_of_pos_left _ <| hab.resolve_left ‹¬0 < a›)]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts)

Tactic:
obtain h | h := P.parts.eq_empty_or_nonempty
  · simp [h]
  calc
    _ ≤ (#P.parts : 𝕜) * (↑(#A / #P.parts) * ↑(#A / #P.parts + 1)) :=
        mod_cast card_biUnion_le_card_mul _ _ _ fun U hU ↦ ?_
    _ = #P.parts * ↑(#A / #P.parts) * ↑(#A / #P.parts + 1) := by rw [mul_assoc]
    _ ≤ #A * (#A / #P.parts + 1) :=
        mul_le_mul (mod_cast Nat.mul_div_le _ _) ?_ (by positivity) (by positivity)
    _ = _ := by rw [← div_add_same (mod_cast h.card_pos.ne'), mul_div_assoc]
  · simpa using Nat.cast_div_le
  suffices (#U - 1) * #U ≤ #A / #P.parts * (#A / #P.parts + 1) by
    rwa [Nat.mul_sub_right_distrib, one_mul, ← offDiag_card] at this
  have := hP.card_part_le_average_add_one hU
  refine Nat.mul_le_mul ((Nat.sub_le_sub_right this 1).trans ?_) this
  simp only [Nat.add_succ_sub_one, add_zero, le_rfl]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ε / 2 * ↑(#A) ^ 2

Tactic:
by
  obtain rfl | hA : A = ⊥ ∨ _ := A.eq_empty_or_nonempty
  · simp [Subsingleton.elim P ⊥]
  apply hP.card_biUnion_offDiag_le'.trans
  rw [div_le_iff₀ (Nat.cast_pos.2 (P.parts_nonempty hA.ne_empty).card_pos)]
  have : (#A : 𝕜) + #P.parts ≤ 2 * #A := by
    rw [two_mul]; gcongr; exact P.card_parts_le_card
  refine (mul_le_mul_of_nonneg_left this <| by positivity).trans ?_
  suffices 1 ≤ ε / 4 * #P.parts by
    rw [mul_left_comm, ← sq]
    convert! mul_le_mul_of_nonneg_left this (mul_nonneg zero_le_two <| sq_nonneg (#A : 𝕜)) using 1
      <;> ring
  rwa [← div_le_iff₀', one_div_div]
  positivity

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

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
⊢ G.deleteEdges G'.edgeSet = G \ G'

Tactic:
ext

Goal state after:
V : Type u_1
G G' : SimpleGraph V
x✝¹ x✝ : V
⊢ (G.deleteEdges G'.edgeSet).Adj x✝¹ x✝ ↔ (G \ G').Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
⊢ G.deleteEdges s = G.deleteEdges (s ∩ G.edgeSet)

Tactic:
ext

Goal state after:
V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ (G.deleteEdges s).Adj x✝¹ x✝ ↔ (G.deleteEdges (s ∩ G.edgeSet)).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
s t : Set (Sym2 V)
⊢ (fromEdgeSet s).deleteEdges t = fromEdgeSet (s \ t)

Tactic:
ext

Goal state after:
V : Type u_1
s t : Set (Sym2 V)
x✝¹ x✝ : V
⊢ ((fromEdgeSet s).deleteEdges t).Adj x✝¹ x✝ ↔ (fromEdgeSet (s \ t)).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.coe.spanningCoe = G'.spanningCoe

Tactic:
ext

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ G'.coe.spanningCoe.Adj x✝¹ x✝ ↔ G'.spanningCoe.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: case hbc
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ 6 * #P.parts ^ 2 ≤ (#P.parts * #P.parts - #P.parts) * 7

Tactic:
rw [tsub_mul]

Goal state after:
case hbc
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ 6 * #P.parts ^ 2 ≤ #P.parts * #P.parts * 7 - #P.parts * 7
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: ι : Sort u_1
V : Type u
G : SimpleGraph V
a b : V
inst✝ : Nonempty ι
f : ι → G.Subgraph
⊢ (⨅ i, f i).Adj a b ↔ ∀ (i : ι), (f i).Adj a b

Tactic:
rw [iInf, sInf_adj_of_nonempty (Set.range_nonempty _)]
  simp

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

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
ι✝ : Type u
κ✝ : ι✝ → Type u
f : (a : ι✝) → κ✝ a → G.Subgraph
⊢ (⨅ a, ⨆ b, f a b).Adj = (⨆ g, ⨅ a, f a (g a)).Adj

Tactic:
ext

Goal state after:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
ι✝ : Type u
κ✝ : ι✝ → Type u
f : (a : ι✝) → κ✝ a → G.Subgraph
x✝¹ x✝ : V
⊢ (⨅ a, ⨆ b, f a b).Adj x✝¹ x✝ ↔ (⨆ g, ⨅ a, f a (g a)).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ 6 / 7 * ↑(#P.parts) ^ 2 * ε ^ 5 * (7 / 24) ≤ ↑(#P.parts.offDiag) * ε ^ 5 * (22 / 75)

Tactic:
by
        gcongr ?_ * _ * ?_
        · rw [← mul_div_right_comm, div_le_iff₀ (by simp), offDiag_card]
          norm_cast
          rw [tsub_mul]
          refine le_tsub_of_add_le_left ?_
          nlinarith
        · norm_num

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set G.Subgraph
v : V
⊢ (sSup s).neighborSet v = ⋃ G' ∈ s, G'.neighborSet v

Tactic:
ext

Goal state after:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
v x✝ : V
⊢ x✝ ∈ (sSup s).neighborSet v ↔ x✝ ∈ ⋃ G' ∈ s, G'.neighborSet v
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set G.Subgraph
v : V
⊢ (sInf s).neighborSet v = (⋂ G' ∈ s, G'.neighborSet v) ∩ G.neighborSet v

Tactic:
ext

Goal state after:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
v x✝ : V
⊢ x✝ ∈ (sInf s).neighborSet v ↔ x✝ ∈ (⋂ G' ∈ s, G'.neighborSet v) ∩ G.neighborSet v
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H₁ H₂ : G.Subgraph
h : Disjoint H₁ H₂
⊢ H₁.edgeSet ⊓ H₂.edgeSet ⊆ ⊥

Tactic:
by simpa using edgeSet_mono h.le_bot

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H H' : G.Subgraph
⊢ Disjoint H.verts H'.verts ↔ Disjoint H H'

Tactic:
constructor

Goal state after:
case mp
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
⊢ Disjoint H.verts H'.verts → Disjoint H H'

case mpr
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
⊢ Disjoint H H' → Disjoint H.verts H'.verts
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H.verts H'.verts
M' : G.Subgraph
hsub₀ : M'.verts ⊆ H.verts
right✝¹ : ∀ ⦃v w : V⦄, M'.Adj v w → H.Adj v w
hsub₁ : M'.verts ⊆ H'.verts
right✝ : ∀ ⦃v w : V⦄, M'.Adj v w → H'.Adj v w
⊢ M' ≤ ⊥

Tactic:
rw [le_bot_iff]

Goal state after:
case mp
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H.verts H'.verts
M' : G.Subgraph
hsub₀ : M'.verts ⊆ H.verts
right✝¹ : ∀ ⦃v w : V⦄, M'.Adj v w → H.Adj v w
hsub₁ : M'.verts ⊆ H'.verts
right✝ : ∀ ⦃v w : V⦄, M'.Adj v w → H'.Adj v w
⊢ M' = ⊥
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H.verts H'.verts
M' : G.Subgraph
hsub₀ : M'.verts ⊆ H.verts
right✝¹ : ∀ ⦃v w : V⦄, M'.Adj v w → H.Adj v w
hsub₁ : M'.verts ⊆ H'.verts
right✝ : ∀ ⦃v w : V⦄, M'.Adj v w → H'.Adj v w
⊢ M' = ⊥

Tactic:
ext

Goal state after:
case mp.verts
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H.verts H'.verts
M' : G.Subgraph
hsub₀ : M'.verts ⊆ H.verts
right✝¹ : ∀ ⦃v w : V⦄, M'.Adj v w → H.Adj v w
hsub₁ : M'.verts ⊆ H'.verts
right✝ : ∀ ⦃v w : V⦄, M'.Adj v w → H'.Adj v w
x✝ : V
⊢ x✝ ∈ M'.verts ↔ x✝ ∈ ⊥.verts

case mp.Adj
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H.verts H'.verts
M' : G.Subgraph
hsub₀ : M'.verts ⊆ H.verts
right✝¹ : ∀ ⦃v w : V⦄, M'.Adj v w → H.Adj v w
hsub₁ : M'.verts ⊆ H'.verts
right✝ : ∀ ⦃v w : V⦄, M'.Adj v w → H'.Adj v w
x✝¹ x✝ : V
⊢ M'.Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ⊆ H.verts
h₁ : S ⊆ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := { verts := {v}, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
M : G.Subgraph
h : v ∈ M.verts
⊢ M' ≤ M

Tactic:
constructor

Goal state after:
case left
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ⊆ H.verts
h₁ : S ⊆ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := ⋯
M : G.Subgraph
h : v ∈ M.verts
⊢ M'.verts ⊆ M.verts

case right
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ⊆ H.verts
h₁ : S ⊆ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := ⋯
M : G.Subgraph
h : v ∈ M.verts
⊢ ∀ ⦃v w : V⦄, M'.Adj v w → M.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
⊢ ⇑(g.comp f) = ⇑g ∘ ⇑f

Tactic:
ext

Goal state after:
α : Type u_4
β : Type u_5
γ : Type u_6
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
x✝ : α
⊢ (g.comp f) x✝ = (⇑g ∘ ⇑f) x✝
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ ofLE G G ⋯ = id G

Tactic:
ext

Goal state after:
V : Type u_1
G : SimpleGraph V
a✝ : V
⊢ (ofLE G G ⋯) a✝ = (id G) a✝
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
G₁ G₂ G₃ : SimpleGraph V
h₁₂ : G₁ ≤ G₂
h₂₃ : G₂ ≤ G₃
⊢ (ofLE G₂ G₃ h₂₃).comp (ofLE G₁ G₂ h₁₂) = ofLE G₁ G₃ ⋯

Tactic:
ext

Goal state after:
V : Type u_1
G₁ G₂ G₃ : SimpleGraph V
h₁₂ : G₁ ≤ G₂
h₂₃ : G₂ ≤ G₃
a✝ : V
⊢ ((ofLE G₂ G₃ h₂₃).comp (ofLE G₁ G₂ h₁₂)) a✝ = (ofLE G₁ G₃ ⋯) a✝
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
⊢ H' ∈ Set.range toSubgraph ↔ H' ∈ {B' | Nonempty (A ≃g B'.coe)}

Tactic:
constructor

Goal state after:
case mp
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
⊢ H' ∈ Set.range toSubgraph → H' ∈ {B' | Nonempty (A ≃g B'.coe)}

case mpr
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
⊢ H' ∈ {B' | Nonempty (A ≃g B'.coe)} → H' ∈ Set.range toSubgraph
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ Subgraph.map Hom.id H = H

Tactic:
ext

Goal state after:
case verts
V : Type u
G : SimpleGraph V
H : G.Subgraph
x✝ : V
⊢ x✝ ∈ (Subgraph.map Hom.id H).verts ↔ x✝ ∈ H.verts

case Adj
V : Type u
G : SimpleGraph V
H : G.Subgraph
x✝¹ x✝ : V
⊢ (Subgraph.map Hom.id H).Adj x✝¹ x✝ ↔ H.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
U : Type u_2
G'' : SimpleGraph U
H : G.Subgraph
f : G →g G'
g : G' →g G''
⊢ Subgraph.map (g.comp f) H = Subgraph.map g (Subgraph.map f H)

Tactic:
ext

Goal state after:
case verts
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
U : Type u_2
G'' : SimpleGraph U
H : G.Subgraph
f : G →g G'
g : G' →g G''
x✝ : U
⊢ x✝ ∈ (Subgraph.map (g.comp f) H).verts ↔ x✝ ∈ (Subgraph.map g (Subgraph.map f H)).verts

case Adj
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
U : Type u_2
G'' : SimpleGraph U
H : G.Subgraph
f : G →g G'
g : G' →g G''
x✝¹ x✝ : U
⊢ (Subgraph.map (g.comp f) H).Adj x✝¹ x✝ ↔ (Subgraph.map g (Subgraph.map f H)).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
⊢ Subgraph.map f H₁ ≤ Subgraph.map f H₂

Tactic:
constructor

Goal state after:
case left
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
⊢ (Subgraph.map f H₁).verts ⊆ (Subgraph.map f H₂).verts

case right
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
⊢ ∀ ⦃v w : W⦄, (Subgraph.map f H₁).Adj v w → (Subgraph.map f H₂).Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
⊢ Subgraph.map f (H₁ ⊔ H₂) = Subgraph.map f H₁ ⊔ Subgraph.map f H₂

Tactic:
ext

Goal state after:
case verts
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
x✝ : W
⊢ x✝ ∈ (Subgraph.map f (H₁ ⊔ H₂)).verts ↔ x✝ ∈ (Subgraph.map f H₁ ⊔ Subgraph.map f H₂).verts

case Adj
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
x✝¹ x✝ : W
⊢ (Subgraph.map f (H₁ ⊔ H₂)).Adj x✝¹ x✝ ↔ (Subgraph.map f H₁ ⊔ Subgraph.map f H₂).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
e : G ≃g H
⊢ Subgraph.map e.toHom ⊤ = ⊤

Tactic:
ext

Goal state after:
case verts
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
e : G ≃g H
x✝ : W
⊢ x✝ ∈ (Subgraph.map e.toHom ⊤).verts ↔ x✝ ∈ ⊤.verts

case Adj
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
e : G ≃g H
x✝¹ x✝ : W
⊢ (Subgraph.map e.toHom ⊤).Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝
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
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
this :
  ∀ B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts, #(B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id) ≤ m
⊢ ∑ a ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts with a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty,
      #(a \ {A ∈ (chunk hP G ε hU).parts | A ⊆ a}.biUnion id) ≤
    ∑ B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts with B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty, m

Tactic:
gcongr with B hB
      exact this B <| filter_subset _ _ hB

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

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : G'.Subgraph
h : H ≤ H'
⊢ Subgraph.comap f H ≤ Subgraph.comap f H'

Tactic:
constructor

Goal state after:
case left
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : G'.Subgraph
h : H ≤ H'
⊢ (Subgraph.comap f H).verts ⊆ (Subgraph.comap f H').verts

case right
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H H' : G'.Subgraph
h : H ≤ H'
⊢ ∀ ⦃v w : V⦄, (Subgraph.comap f H).Adj v w → (Subgraph.comap f H').Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
f : G →g H
⊢ Subgraph.comap f ⊤ = ⊤

Tactic:
ext

Goal state after:
case verts
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
f : G →g H
x✝ : V
⊢ x✝ ∈ (Subgraph.comap f ⊤).verts ↔ x✝ ∈ ⊤.verts

case Adj
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
f : G →g H
x✝¹ x✝ : V
⊢ (Subgraph.comap f ⊤).Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Copy

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

Tactic:
constructor

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

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.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : V
inst✝ : DecidableEq V
⊢ G.replaceVertex s s = G

Tactic:
ext

Goal state after:
V : Type u_1
G : SimpleGraph V
s : V
inst✝ : DecidableEq V
x✝¹ x✝ : V
⊢ (G.replaceVertex s s).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ G.singletonSubgraph v ≤ H

Tactic:
constructor

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

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: V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
⊢ Subgraph.map f (G.singletonSubgraph v) = G'.singletonSubgraph (f v)

Tactic:
ext

Goal state after:
case verts
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
x✝ : W
⊢ x✝ ∈ (Subgraph.map f (G.singletonSubgraph v)).verts ↔ x✝ ∈ (G'.singletonSubgraph (f v)).verts

case Adj
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
x✝¹ x✝ : W
⊢ (Subgraph.map f (G.singletonSubgraph v)).Adj x✝¹ x✝ ↔ (G'.singletonSubgraph (f v)).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
⊢ H = G.singletonSubgraph v

Tactic:
ext

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

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: V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ G.subgraphOfAdj ⋯ ≤ H

Tactic:
constructor

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

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 ⋯ = G.subgraphOfAdj hvw

Tactic:
ext

Goal state after:
case verts
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝ : V
⊢ x✝ ∈ (G.subgraphOfAdj ⋯).verts ↔ x✝ ∈ (G.subgraphOfAdj hvw).verts

case Adj
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (G.subgraphOfAdj ⋯).Adj x✝¹ x✝ ↔ (G.subgraphOfAdj hvw).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ Subgraph.map f (G.subgraphOfAdj hvw) = G'.subgraphOfAdj ⋯

Tactic:
ext

Goal state after:
case verts
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
x✝ : W
⊢ x✝ ∈ (Subgraph.map f (G.subgraphOfAdj hvw)).verts ↔ x✝ ∈ (G'.subgraphOfAdj ⋯).verts

case Adj
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
x✝¹ x✝ : W
⊢ (Subgraph.map f (G.subgraphOfAdj hvw)).Adj x✝¹ x✝ ↔ (G'.subgraphOfAdj ⋯).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
hvw : G.Adj v w
hv : u ≠ v
hw : u ≠ w
⊢ (G.subgraphOfAdj hvw).neighborSet u = ∅

Tactic:
ext

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
hvw : G.Adj v w
hv : u ≠ v
hw : u ≠ w
x✝ : V
⊢ x✝ ∈ (G.subgraphOfAdj hvw).neighborSet u ↔ x✝ ∈ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (G.subgraphOfAdj h).support = {u, v}

Tactic:
ext

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ : V
⊢ x✝ ∈ (G.subgraphOfAdj h).support ↔ x✝ ∈ {u, v}
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
⊢ Subgraph.restrict (Subgraph.coeSubgraph G'') = G''

Tactic:
ext

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

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✝