mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w x y z : V
h : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
⊢ w = y ∨ w ∈ p'.support → w ∈ p'.support

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w x y z : V
h : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
⊢ w ∈ p'.support → w = y ∨ w ∈ p'.support

Tactic:
by

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:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.toSubgraph.verts ↔ w ∈ p.support

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
w u v x : V
p : G.Walk u v
hadj : p.toSubgraph.Adj w x
⊢ ¬p.Nil

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u ∈ p.toSubgraph.verts

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ v ∈ p.toSubgraph.verts

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
e : Sym2 V
⊢ e ∈ p.toSubgraph.edgeSet ↔ e ∈ p.edges

Tactic:
by

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
⊢ h.toWalk.toSubgraph = G.subgraphOfAdj h

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.append q).toSubgraph = p.toSubgraph ⊔ q.toSubgraph

Tactic:
by

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:
by

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:
by

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
⊢ (_root_.completeBipartiteGraph α β).Copy G

Tactic:
by

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:
by

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:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.toSubgraph = p.toSubgraph

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
c : G.Walk v v
h : u ∈ c.support
⊢ (c.rotate u h).toSubgraph = c.toSubgraph

Tactic:
by

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:
by

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 β
⊢ completeBipartiteGraph α β ⊑ G →
    ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween ↑left ↑right

Tactic:
by

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
f : G →g G'
p : G.Walk u v
⊢ (Walk.map f p).toSubgraph = Subgraph.map f p.toSubgraph

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
H : G.Subgraph
⊢ Disjoint {x | ↑x ∈ s} {x | ↑x ∈ t}

Tactic:
by

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:
by

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

Goal state before:
pp: V : Type u_1
v✝ w✝ : V
G✝ : SimpleGraph V
s✝ t✝ s t : Set V
G : SimpleGraph V
v w : V
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s) → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)

Tactic:
by

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
⊢ (between s t G).Adj v w ↔ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
⊢ between s t G = between t s G

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ (p.toSubgraph.neighborSet w).Finite

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.toSubgraph ≤ ⊤.induce {v_1 | v_1 ∈ p.support}

Tactic:
by

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
⊢ G.neighborSet v ⊆ (between s sᶜ G).neighborSet v ∪ s

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
i : ℕ
hi : i < w.length
⊢ w.toSubgraph.Adj (w.getVert i) (w.getVert (i + 1))

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : ¬w.Nil
⊢ w.toSubgraph.Adj u w.snd

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : 0 < w.length
⊢ w.length - 1 < w.length

Tactic:
by

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

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
⊢ G.neighborSet w ⊆ (between s sᶜ G).neighborSet w ∪ sᶜ

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : ¬w.Nil
⊢ w.toSubgraph.Adj w.penultimate v

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
⊢ p.toSubgraph.Adj u' v' ↔ s(u', v') ∈ p.edges

Tactic:
by

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
s : Finset V
inst✝ : DecidableRel G.Adj
hv : v ∈ s
⊢ G.neighborFinset v ⊆ (between (↑s) (↑s)ᶜ G).neighborFinset v ∪ s

Tactic:
by

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
s : Finset V
inst✝ : DecidableRel G.Adj
hv : v ∈ s
⊢ (between (↑s) (↑s)ᶜ G).IsBipartiteWith ↑s ↑sᶜ

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
w : G.Walk u v
⊢ w.toSubgraph.Adj u' v' ↔ ∃ i, s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
⊢ w.toSubgraph ≤ G' ↔ w.edgeSet ⊆ G'.edgeSet

Tactic:
by

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
s : Finset V
inst✝ : DecidableRel G.Adj
hv : v ∈ s
⊢ G.degree v ≤ (between (↑s) (↑s)ᶜ G).degree v + #s

Tactic:
by

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

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
s : Finset V
inst✝ : DecidableRel G.Adj
hw : w ∈ sᶜ
⊢ w ∈ (↑s)ᶜ

Tactic:
by

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

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
s : Finset V
inst✝ : DecidableRel G.Adj
hw : w ∈ sᶜ
⊢ G.neighborFinset w ⊆ (between (↑s) (↑s)ᶜ G).neighborFinset w ∪ sᶜ

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst✝ : DecidableEq V
⊢ p.bypass.toSubgraph ≤ p.toSubgraph

Tactic:
by

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

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
s : Finset V
inst✝ : DecidableRel G.Adj
hw : w ∈ sᶜ
⊢ (between (↑s) (↑s)ᶜ G).IsBipartiteWith ↑s ↑sᶜ

Tactic:
by

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

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
s : Finset V
inst✝ : DecidableRel G.Adj
hw : w ∈ sᶜ
⊢ G.degree w ≤ (between (↑s) (↑s)ᶜ G).degree w + #sᶜ

Tactic:
by

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

Goal state before:
pp: W₁ : Type u_2
W₂ : Type u_3
⊢ (completeBipartiteGraph W₁ W₂).edgeSet = Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝¹ v v✝ : V
h✝ : G.Adj u v✝
w : G.Walk v✝ v
⊢ Walk.map (cons h✝ w).toSubgraph.hom (cons h✝ w).mapToSubgraph = cons h✝ w

Tactic:
by

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

Goal state before:
pp: W₁ : Type u_2
W₂ : Type u_3
⊢ Function.Injective fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

Tactic:
by

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

Goal state before:
pp: W₁ : Type u_2
W₂ : Type u_3
⊢ (completeBipartiteGraph W₁ W₂).edgeSet.encard = ENat.card W₁ * ENat.card W₂

Tactic:
by

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v✝ w✝ : V
s : Set V
u v : V
w : G.Walk u v
hs : ∀ x ∈ w.support, x ∈ s
x✝ : ↑w.toSubgraph.verts
⊢ ↑x✝ ∈ s

Tactic:
by

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
W₁ : Type u_2
W₂ : Type u_3
inst✝ : DecidableRel fun x1 x2 ↦ x1 ∈ x2
hG : G.IsBipartiteWith s t
x✝ : ↑G.edgeSet
e : Sym2 V
he : e ∈ G.edgeSet
⊢ ∀ (a b : V) (h : G.Adj a b),
    (⋯.by_cases (fun h ↦ ⟨s(Sum.inl ⟨a, ⋯⟩, Sum.inr ⟨b, ⋯⟩), ⋯⟩) fun h ↦ ⟨s(Sum.inl ⟨b, ⋯⟩, Sum.inr ⟨a, ⋯⟩), ⋯⟩) =
      ⋯.by_cases (fun h ↦ ⟨s(Sum.inl ⟨b, ⋯⟩, Sum.inr ⟨a, ⋯⟩), ⋯⟩) fun h ↦ ⟨s(Sum.inl ⟨a, ⋯⟩, Sum.inr ⟨b, ⋯⟩), ⋯⟩

Tactic:
by

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
W₁ : Type u_2
W₂ : Type u_3
inst✝ : DecidableRel fun x1 x2 ↦ x1 ∈ x2
hG : G.IsBipartiteWith s t
⊢ Function.Injective fun x ↦
    match x with
    | ⟨e, he⟩ =>
      Sym2.fromRelNdrec e he
        (fun u v h ↦
          ⋯.by_cases (fun h ↦ ⟨s(Sum.inl ⟨u, ⋯⟩, Sum.inr ⟨v, ⋯⟩), ⋯⟩) fun h ↦ ⟨s(Sum.inl ⟨v, ⋯⟩, Sum.inr ⟨u, ⋯⟩), ⋯⟩)
        ⋯

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
hG : G.IsBipartiteWith s t
⊢ G.edgeSet.encard ≤ s.encard * t.encard

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
u v✝¹ v v✝ : V
hadj : G.Adj u v✝
w : G.Walk v✝ v
hs : ∀ x ∈ (cons hadj w).support, x ∈ s
⊢ Walk.map { toFun := fun x ↦ ⟨↑x, ⋯⟩, map_rel' := ⋯ } (cons hadj w).mapToSubgraph = Walk.induce s (cons hadj w) hs

Tactic:
by

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

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

Tactic:
by

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
G : SimpleGraph V
x✝¹ x✝ : V ⊕ V
⊢ (match x✝¹, x✝ with
    | Sum.inl v', Sum.inr w' => G.Adj v' w'
    | Sum.inr v', Sum.inl w' => G.Adj v' w'
    | x, x_1 => False) →
    match x✝, x✝¹ with
    | Sum.inl v', Sum.inr w' => G.Adj v' w'
    | Sum.inr v', Sum.inl w' => G.Adj v' w'
    | x, x_1 => False

Tactic:
by

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:
by

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:
by

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.inl val✝)
⊢ (completeBipartiteGraph V V).Adj (Sum.inl val✝¹) (Sum.inl val✝)

Tactic:
by

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.inr val✝)
⊢ (completeBipartiteGraph V V).Adj (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ w.toSubgraph.IsInduced ↔ w.IsChordless

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : α → β
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
⊢ (∑ a ∈ s, f₁ a) * ∑ a ∈ t, f₂ a ≤ (∑ a ∈ s ⊼ t, f₃ a) * ∑ a ∈ s ⊻ t, f₄ a

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
x✝ : V × V
h :
  x✝ ∈
    {x |
      match x with
      | (x, y) => G.Adj x y}
⊢ (match x✝, h with
    | (v, w), x => s(Sum.inl v, Sum.inr w)) ∈
    G.bipartiteDoubleCover.edgeFinset

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : DecidableEq α
s t : Finset α
⊢ #s * #t ≤ #(s ⊼ t) * #(s ⊻ t)

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ p.toSubgraph.neighborSet u = {p.snd}

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ ¬p.reverse.Nil

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : α → β
inst✝ : Fintype α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
⊢ (∑ a, f₁ a) * ∑ a, f₂ a ≤ (∑ a, f₃ a) * ∑ a, f₄ a

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ (a₁ : V × V)
    (ha₁ :
      a₁ ∈
        {x |
          match x with
          | (x, y) => G.Adj x y})
    (a₂ : V × V)
    (ha₂ :
      a₂ ∈
        {x |
          match x with
          | (x, y) => G.Adj x y}),
    ((match a₁, ha₁ with
        | (v, w), x => s(Sum.inl v, Sum.inr w)) =
        match a₂, ha₂ with
        | (v, w), x => s(Sum.inl v, Sum.inr w)) →
      a₁ = a₂

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ p.toSubgraph.neighborSet v = {p.penultimate}

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h : i ≠ 0
h' : i < p.length
⊢ i - 1 < p.length

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v = 0 ↔ u = v

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v = 0 ↔ u = v

Tactic:
by
  simp [edist]

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1) →
    ∃ i_1,
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v w : V
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v ≠ ⊤ ↔ G.Reachable u v

Tactic:
by

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
⊢ edist ?m.16 ?m.17 ?m.18 ≠ ⊤

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v = 1 ↔ G.Adj u v

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v

Tactic:
by

Goal state after: