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

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
⊢ H.Adj ((C (G.connectedComponentMk a✝)) ⟨a✝, ⋯⟩) ((C (G.connectedComponentMk b✝)) ⟨b✝, ⋯⟩)

Tactic:
convert (C (G.connectedComponentMk _)).map_rel h using 3

Goal state after:
case e'_1
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
⊢ ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)

case e'_2
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
⊢ (fun x ↦ x ∈ G.connectedComponentMk b✝) = fun x ↦ x ∈ G.connectedComponentMk a✝

case e'_4.e'_3
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_1✝¹ : ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)
e_2✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
e_3✝ : (fun x ↦ V') ≍ fun x ↦ V'
e_1✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
⊢ (G.connectedComponentMk b✝).toSimpleGraph.Adj ≍ (G.connectedComponentMk a✝).toSimpleGraph.Adj

case e'_5
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_1✝ : ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk a✝).toSimpleGraph.Adj →r H.Adj)
⊢ G.connectedComponentMk b✝ = G.connectedComponentMk a✝

case e'_6
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
e_2✝ : ↥(G.connectedComponentMk b✝) = ↥(G.connectedComponentMk a✝)
⊢ (fun x ↦ x ∈ G.connectedComponentMk b✝) = fun x ↦ x ∈ G.connectedComponentMk a✝
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
h : G = ⊥
⊢ ∀ {a b : V}, ⊥.Adj a b → (completeGraph (Fin 1)).Adj (0 a) (0 b)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
C : G.Coloring α
⊢ card α ≤ card (Fin (card α))

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
⊢ G.deleteEdges {s(v, w)} ≤ G

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ n ≤ card (Fin n)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n ↔ ∃ C, ∀ (v : V), C v < n

Tactic:
constructor
  · rintro hc
    have C : G.Coloring (Fin n) := hc.toColoring (by simp)
    let f := Embedding.completeGraph (@Fin.valEmbedding n)
    use f.toHom.comp C
    intro v
    exact Fin.is_lt (C.1 v)
  · rintro ⟨C, Cf⟩
    refine ⟨Coloring.mk ?_ ?_⟩
    · exact fun v => ⟨C v, Cf v⟩
    · rintro v w hvw
      simp only [Fin.mk_eq_mk, Ne]
      exact C.valid hvw

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ ⨅ n ∈ Set.ofPred G.Colorable, ↑n ≠ ⊤ ↔ ∃ n, G.Colorable n

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case refl
V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
v : V
⊢ G.Adj v v → 0 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
⊢ 0 < G.chromaticNumber

Tactic:
rw [hc.chromaticNumber_eq_sInf, Nat.cast_pos]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
⊢ 0 < sInf {n' | G.Colorable n'}
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp.refine_2
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ s(v, w) ∈ (Walk.cons ⋯ ↑p.toPath).edges

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
h : card α ≤ sInf {n' | G.Colorable n'}
C : G.Coloring α
i : α
hi : ∀ (a : V), C a ≠ i
D : G.Coloring { a // a ≠ i } := { toFun := fun v ↦ ⟨C v, ⋯⟩, map_rel' := ⋯ }
⊢ card { a // a ≠ i } = card (Fin (card α - 1))

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : ¬G.Adj x y
⊢ (G.deleteEdges {s(x, y)}).Connected

pp: case inr
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
⊢ (G.deleteEdges {s(x, y)}).Connected

Tactic:
· rwa [deleteEdges, Disjoint.sdiff_eq_left (by simpa)]

Goal state after:
case inr
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
⊢ (G.deleteEdges {s(x, y)}).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
inst✝ : Nonempty V
⊢ ⊥.Colorable 1

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case inl
V : Type u
h✝ : Finite V
this : Fintype V
⊢ ⊤.chromaticNumber = ENat.card V

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case inr
V : Type u
h✝ : Infinite V
⊢ ⊤.chromaticNumber = ENat.card V

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case inl.inl
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ val✝ : V
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val✝¹) (Sum.inl val✝) → (Sum.inl val✝¹).isRight ≠ (Sum.inl val✝).isRight

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case inl.inr
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ : V
val✝ : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val✝¹) (Sum.inr val✝) → (Sum.inl val✝¹).isRight ≠ (Sum.inr val✝).isRight

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case inr.inl
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ : W
val✝ : V
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val✝¹) (Sum.inl val✝) → (Sum.inr val✝¹).isRight ≠ (Sum.inl val✝).isRight

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case inr.inr
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ val✝ : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val✝¹) (Sum.inr val✝) → (Sum.inr val✝¹).isRight ≠ (Sum.inr val✝).isRight

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
C : (completeBipartiteGraph V W).Coloring (Fin 2)
b : Fin 2
v : V
w : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inl v) (Sum.inr w)

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
⊢ s.card ≤ Nat.card ↥s

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι✝ : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
ι : Type u_4
V : ι → Type u_5
⊢ ∀ {v w : (i : ι) × V i}, (completeMultipartiteGraph V).Adj v w → v.fst ≠ w.fst

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ G.neighborFinset v = bipartiteAbove G.Adj t v

Tactic:
isBipartiteWith_neighborFinset h hv,

Goal state after:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ {w ∈ t | G.Adj v w} = bipartiteAbove G.Adj t v
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case empty.inl
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
ℬ : Finset (Finset α)
hℬ : ℬ = ∅ ∨ ℬ = {∅}
⊢ (∑ s ∈ ∅, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ ∅ ⊼ ℬ, f₃ s) * ∑ s ∈ ∅ ⊻ ℬ, f₄ s

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case empty.inr.inl
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ ∅ → ∀ ⦃t : Finset α⦄, t ⊆ ∅ → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
⊢ (∑ s ∈ {∅}, f₁ s) * ∑ s ∈ ∅, f₂ s ≤ (∑ s ∈ {∅} ⊼ ∅, f₃ s) * ∑ s ∈ {∅} ⊻ ∅, f₄ s

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: case refine_2.inr
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk : k ≠ 0
h : ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v
s : Set (Sym2 V)
hs : s.encard < ↑(k + 1)
e : Sym2 V
he : e ∈ s
⊢ (G.deleteEdges s).Reachable u v

Tactic:
rw [← Set.insert_sdiff_self_of_mem he, Set.insert_eq, ← deleteEdges_deleteEdges]

Goal state after:
case refine_2.inr
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk : k ≠ 0
h : ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v
s : Set (Sym2 V)
hs : s.encard < ↑(k + 1)
e : Sym2 V
he : e ∈ s
⊢ ((G.deleteEdges {e}).deleteEdges (s \ {e})).Reachable u v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
⊢ 2 ≠ 0

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
s₁ s₂ : α ⊕ β
p₁ p₂ : α
⊢ Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inl p₁) =
      Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inl p₂) →
    Sum.inl p₁ = Sum.inl p₂

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).coe.Preconnected

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a : V
ha : a ∈ (G.subgraphOfAdj hvw).verts
b : V
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
s₁ s₂ : α ⊕ β
p₁ p₂ : β
⊢ Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inr p₁) =
      Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inr p₂) →
    Sum.inr p₁ = Sum.inr p₂

Tactic:
simp

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

Goal state before:
pp: case inl.inr
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj a b
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Adj ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
simp

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

Goal state before:
pp: case inr.inl
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj b a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Adj ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (cons h nil).toSubgraph = G.subgraphOfAdj h

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isLeft = true
hs₂ : s₂.isRight = true
⊢ (Subtype.val ∘ ⇑fα) (s₁.getLeft hs₁) ∈ ↑left

Tactic:
simp

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
⊢ w ∈ nil.toSubgraph.verts ↔ w ∈ nil.support

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isLeft = true
hs₂ : s₂.isRight = true
⊢ (Subtype.val ∘ ⇑fβ) (s₂.getRight hs₂) ∈ ↑right

Tactic:
simp

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

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ : V
⊢ x✝ ∈ h.toWalk.toSubgraph.verts ↔ x✝ ∈ (G.subgraphOfAdj h).verts

Tactic:
simp

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

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝¹ x✝ : V
⊢ h.toWalk.toSubgraph.Adj x✝¹ x✝ ↔ (G.subgraphOfAdj h).Adj x✝¹ x✝

Tactic:
simp

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.reverse.toSubgraph = nil.toSubgraph

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isRight = true
hs₂ : s₂.isLeft = true
⊢ (Subtype.val ∘ ⇑fα) (s₂.getLeft hs₂) ∈ ↑left

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isRight = true
hs₂ : s₂.isLeft = true
⊢ (Subtype.val ∘ ⇑fβ) (s₁.getRight hs₁) ∈ ↑right

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝ : completeBipartiteGraph α β ⊑ G
f : (completeBipartiteGraph α β).Copy G
⊢ #(map { toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } univ) = Fintype.card α

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝ : completeBipartiteGraph α β ⊑ G
f : (completeBipartiteGraph α β).Copy G
⊢ #(map { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } univ) = Fintype.card β

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝² : completeBipartiteGraph α β ⊑ G
f : (completeBipartiteGraph α β).Copy G
x✝¹ x✝ : V
w✝¹ : α
left✝¹ : w✝¹ ∈ univ
hl : { toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } w✝¹ = x✝¹
w✝ : β
left✝ : w✝ ∈ univ
hr : { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } w✝ = x✝
⊢ (completeBipartiteGraph α β).Adj (Sum.inl w✝¹) (Sum.inr w✝)

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
G' : SimpleGraph V
w x : V
p : G.Walk u v
h : G ≤ G'
⊢ (mapLe h p).toSubgraph.Adj w x ↔ p.toSubgraph.Adj w x

Tactic:
simp

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

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
hi : 0 < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert 0) ((cons hxy i').getVert (0 + 1))

Tactic:
simp

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

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert (n✝ + 1)) ((cons hxy i').getVert (n✝ + 1 + 1))

Tactic:
simp only [Walk.toSubgraph, getVert_cons_succ, Subgraph.sup_adj, subgraphOfAdj_adj, Sym2.eq,
        Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]

Goal state after:
case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy i').length
⊢ (u✝ = i'.getVert n✝ ∧ v✝ = i'.getVert (n✝ + 1) ∨ u✝ = i'.getVert (n✝ + 1) ∧ v✝ = i'.getVert n✝) ∨
    i'.toSubgraph.Adj (i'.getVert n✝) (i'.getVert (n✝ + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.IsBipartite
x✝ : Infinite V
⊢ 4 * G.edgeSet.encard ≤ ENat.card V ^ 2

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V ⊕ V
val✝¹ val✝ : V
hadj : G.bipartiteDoubleCover.Adj (Sum.inl val✝¹) (Sum.inr val✝)
⊢ (completeBipartiteGraph V V).Adj (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V ⊕ V
val✝¹ val✝ : V
hadj : G.bipartiteDoubleCover.Adj (Sum.inr val✝¹) (Sum.inl val✝)
⊢ (completeBipartiteGraph V V).Adj (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
⊢ 1 ≠ ⊤

Tactic:
simp

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
u v : V
h : 2 < G.edist u v
⊢ u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅

Tactic:
have hn : u ≠ v := fun hc ↦ by simp [hc] at h

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
u v : V
h : 2 < G.edist u v
hn : u ≠ v
⊢ u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
⊢ G.dist v v = 0

Tactic:
simp

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

Goal state before:
pp: case inl.inl.inl
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
r : V
hr : Sum.inl r ∈ right
l' : V
hl' : Sum.inl l' ∈ left
⊢ ((Sum.inl l).isLeft = true → (Sum.inl l').isLeft = true) ∧ ((Sum.inl l).isRight = true → (Sum.inl l').isRight = true)

Tactic:
simp

Goal state after: