mathlib-initiative/mathlib-tactics huggingface dataset:
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 {e}).deleteEdges (s \ {e})).Reachable u v

Tactic:
]

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: 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
⊢ s.encard < ↑k + 1

Tactic:
]

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
⊢ s.encard < ↑k + 1
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 : Fintype.card ↥left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
⊢ Nonempty (α ↪ ↥left)

Tactic:
]

Goal state after:
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 : Fintype.card ↥left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
⊢ Nonempty (α ↪ ↥left)
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 : Fintype.card ↥right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
⊢ Nonempty (β ↪ ↥right)

Tactic:
]

Goal state after:
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 : Fintype.card ↥right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
⊢ Nonempty (β ↪ ↥right)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.coe.Preconnected ∧ H.verts.Nonempty ↔ H.coe.Preconnected ∧ H.verts.Nonempty

Tactic:
]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected ∧ H.verts.Nonempty
⊢ H.Preconnected

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected ∧ H.verts.Nonempty
⊢ H.Preconnected
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected ∧ H.verts.Nonempty
⊢ H.verts.Nonempty

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected ∧ H.verts.Nonempty
⊢ H.verts.Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ (G.subgraphOfAdj huv).Connected

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ (G.subgraphOfAdj huv).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv : H.verts = H'.verts
h : H.Connected
⊢ (H'.copy H.verts hv H'.Adj ⋯).Connected

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv : H.verts = H'.verts
h : H.Connected
⊢ (H'.copy H.verts hv H'.Adj ⋯).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Preconnected
hK : K.Preconnected
hn : (H ⊓ K).verts.Nonempty
⊢ ∃ v, ∀ (w : ↑(H ⊔ K).verts), (H ⊔ K).coe.Reachable v w

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Preconnected
hK : K.Preconnected
hn : (H ⊓ K).verts.Nonempty
⊢ ∃ v, ∀ (w : ↑(H ⊔ K).verts), (H ⊔ K).coe.Reachable v w
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
⊢ ∃ v, H.verts = (G.connectedComponentMk v).supp

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
⊢ ∃ v, H.verts = (G.connectedComponentMk v).supp
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
v : V
G' : G.Subgraph
hconn : G'.Connected
hle : (G.connectedComponentMk v).toSubgraph ≤ G'
⊢ G' ≤ (G.connectedComponentMk v).toSubgraph

Tactic:
refine le_trans Subgraph.le_induce_top_verts <| Subgraph.induce_mono_right fun u hu ↦ ?_

Goal state after:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
v : V
G' : G.Subgraph
hconn : G'.Connected
hle : (G.connectedComponentMk v).toSubgraph ≤ G'
u : V
hu : u ∈ G'.verts
⊢ u ∈ (G.connectedComponentMk v).supp
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inl
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
⊢ G.Adj ((Subtype.val ∘ ⇑fα) (s₁.getLeft hs₁)) ((Subtype.val ∘ ⇑fβ) (s₂.getRight hs₂))

Tactic:
]

Goal state after:
case inl
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
⊢ G.Adj ((Subtype.val ∘ ⇑fα) (s₁.getLeft hs₁)) ((Subtype.val ∘ ⇑fβ) (s₂.getRight hs₂))
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inl
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
⊢ G.Adj (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) s₁) (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) s₂)

pp: case inr
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
⊢ G.Adj (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) s₁) (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) s₂)

Tactic:
· rw [← Sum.inl_getLeft s₁ hs₁, ← Sum.inr_getRight s₂ hs₂,
      Sum.elim_inl, Sum.elim_inr]
    exact h (by simp) (by simp)

Goal state after:
case inr
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
⊢ G.Adj (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) s₁) (Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) s₂)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inr
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
⊢ G.Adj ((Subtype.val ∘ ⇑fα) (s₂.getLeft hs₂)) ((Subtype.val ∘ ⇑fβ) (s₁.getRight hs₁))

Tactic:
]

Goal state after:
case inr
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
⊢ G.Adj ((Subtype.val ∘ ⇑fα) (s₂.getLeft hs₂)) ((Subtype.val ∘ ⇑fβ) (s₁.getRight hs₁))
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.toSubgraph = p✝.toSubgraph
⊢ G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝ ⊔ p✝.toSubgraph = G.subgraphOfAdj h✝ ⊔ p✝.toSubgraph

Tactic:
]

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.toSubgraph = p✝.toSubgraph
⊢ G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝ ⊔ p✝.toSubgraph = G.subgraphOfAdj h✝ ⊔ p✝.toSubgraph
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✝¹ : V
hl : ∃ a ∈ univ, { toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } a = x✝¹
x✝ : V
hr : ∃ a ∈ univ, { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } a = x✝
⊢ G.Adj x✝¹ x✝

Tactic:
]

Goal state after:
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✝¹ : V
hl : ∃ a ∈ univ, { toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } a = x✝¹
x✝ : V
hr : ∃ a ∈ univ, { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } a = x✝
⊢ G.Adj x✝¹ x✝
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.toSubgraph = c.toSubgraph

Tactic:
]

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✝
⊢ G.Adj ({ toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } w✝¹) ({ toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } w✝)

Tactic:
]

Goal state after:
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✝
⊢ G.Adj ({ toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } w✝¹) ({ toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } w✝)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
⊢ ∅.Finite

Tactic:
]

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
⊢ ∅.Finite
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : (p✝.toSubgraph.neighborSet w).Finite
⊢ ((G.subgraphOfAdj ha).neighborSet w ∪ p✝.toSubgraph.neighborSet w).Finite

Tactic:
]

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : (p✝.toSubgraph.neighborSet w).Finite
⊢ ((G.subgraphOfAdj ha).neighborSet w ∪ p✝.toSubgraph.neighborSet w).Finite
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s

Tactic:
]

Goal state after:
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ

Tactic:
]

Goal state after:
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ
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.toSubgraph.Adj w.penultimate v

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : 0 < w.length
⊢ w.toSubgraph.Adj w.penultimate v
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' ↔ p.toSubgraph.Adj u' v'

Tactic:
]

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
hw : w.edgeSet ⊆ G'.edgeSet
v' : V
hv' : ∃ e ∈ w.edges, v' ∈ e
⊢ v' ∈ G'.verts

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
hw : w.edgeSet ⊆ G'.edgeSet
v' : V
hv' : ∃ e ∈ w.edges, v' ∈ e
⊢ v' ∈ G'.verts
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
⊢ cons ⋯ (Walk.map ((cons h✝ w).toSubgraph.hom.comp (Subgraph.inclusion ⋯)) w.mapToSubgraph) = cons h✝ w

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v✝¹ v v✝ : V
h✝ : G.Adj u v✝
w : G.Walk v✝ v
⊢ cons ⋯ (Walk.map ((cons h✝ w).toSubgraph.hom.comp (Subgraph.inclusion ⋯)) w.mapToSubgraph) = cons h✝ w
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

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

Tactic:
]

Goal state after:
W₁ : Type u_2
W₂ : Type u_3
⊢ ((fun x ↦ s(Sum.inl x.1, Sum.inr x.2)) '' Set.univ).encard = Set.univ.encard
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
⊢ (completeBipartiteGraph ↑s ↑t).edgeSet.encard ≤ s.encard * t.encard

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Set V
hG : G.IsBipartiteWith s t
⊢ (completeBipartiteGraph ↑s ↑t).edgeSet.encard ≤ s.encard * t.encard
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h✝ : G.IsBipartite
hv : Finite V
s t : Set V
h : G.IsBipartiteWith s t
⊢ 4 * (s.encard * t.encard) ≤ ENat.card V ^ 2

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
h✝ : G.IsBipartite
hv : Finite V
s t : Set V
h : G.IsBipartiteWith s t
⊢ 4 * (s.encard * t.encard) ≤ ENat.card V ^ 2
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
⊢ cons ⋯ (Walk.map (Hom.comp { toFun := fun x ↦ ⟨↑x, ⋯⟩, map_rel' := ⋯ } (Subgraph.inclusion ⋯)) w.mapToSubgraph) =
    Walk.induce s (cons hadj w) hs

Tactic:
]

Goal state after:
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
⊢ cons ⋯ (Walk.map (Hom.comp { toFun := fun x ↦ ⟨↑x, ⋯⟩, map_rel' := ⋯ } (Subgraph.inclusion ⋯)) w.mapToSubgraph) =
    Walk.induce s (cons hadj w) hs
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h✝ : G.IsBipartite
hv : Finite V
s t : Set V
h : G.IsBipartiteWith s t
this : ↑s.ncard + ↑t.ncard ≤ ↑(Nat.card V)
⊢ 4 * (↑s.ncard * ↑t.ncard) ≤ ↑(Nat.card V) ^ 2

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
h✝ : G.IsBipartite
hv : Finite V
s t : Set V
h : G.IsBipartiteWith s t
this : ↑s.ncard + ↑t.ncard ≤ ↑(Nat.card V)
⊢ 4 * (↑s.ncard * ↑t.ncard) ≤ ↑(Nat.card V) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #{x |
        match x with
        | (x, y) => G.Adj x y} =
    #G.bipartiteDoubleCover.edgeFinset

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #{x |
        match x with
        | (x, y) => G.Adj x y} =
    #G.bipartiteDoubleCover.edgeFinset
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
⊢ 0 < p.length

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ 0 < p.length
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V ⊕ V
he : G.bipartiteDoubleCover.Adj v w
⊢ ∃ a,
    ∃ (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)) =
        s(v, w)

Tactic:
]

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V ⊕ V
he : G.bipartiteDoubleCover.Adj v w
⊢ ∃ a,
    ∃ (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)) =
        s(v, w)
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case inr.inr
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
q : G.Walk v w
hq : ↑q.length = G.edist v w
⊢ G.edist u w ≤ ↑(p.append q).length

Tactic:
]

Goal state after:
case inr.inr
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
q : G.Walk v w
hq : ↑q.length = G.edist v w
⊢ G.edist u w ≤ ↑(p.append q).length
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ sInf (Set.range fun x ↦ ↑x.reverse.length) = G.edist v u

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ sInf (Set.range fun x ↦ ↑x.reverse.length) = G.edist v u
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
⊢ ↑k ≠ ⊤

Tactic:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
k : ℕ
h : G.edist u v = ↑k
⊢ ↑k ≠ ⊤
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:
]

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
⊢ 1 ≠ ⊤
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
i' : ℕ
right✝¹ : i' < p.length
hl : p.getVert i' = p.getVert i
right✝ : p.getVert (i' + 1) = v
⊢ i' ≤ p.length

Tactic:
]

Goal state after:
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
i' : ℕ
right✝¹ : i' < p.length
hl : p.getVert i' = p.getVert i
right✝ : p.getVert (i' + 1) = v
⊢ i' ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
h : 0 < G.edist u v
⊢ G.edist u v = 1 ↔ G.Adj u v

Tactic:
]

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
h : 0 < G.edist u v
⊢ G.edist u v = 1 ↔ G.Adj u v
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
i' : ℕ
right✝¹ : i' < p.length
hl : p.getVert i' = p.getVert i
right✝ : p.getVert (i' + 1) = v
⊢ i ≤ p.length

Tactic:
]

Goal state after:
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
i' : ℕ
right✝¹ : i' < p.length
hl : p.getVert i' = p.getVert i
right✝ : p.getVert (i' + 1) = v
⊢ i ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case refine_4
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
w : V
hw : G.Adj u w ∧ G.Adj v w
⊢ G.edist u v ≤ 2

Tactic:
]

Goal state after:
case refine_4
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
w : V
hw : G.Adj u w ∧ G.Adj v w
⊢ G.edist u v ≤ 2