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

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

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.Reachable ⟨a, ha⟩ ⟨b, hb⟩

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.Reachable ⟨a, ha⟩ ⟨b, hb⟩

pp: case inr.inr
V : Type u
G : SimpleGraph V
v b : V
hvw : G.Adj v b
ha hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨b, ha⟩ ⟨b, hb⟩

Tactic:
<;>

Goal state after:
case inl.inl
V : Type u
G : SimpleGraph V
w b : V
hvw : G.Adj b w
ha hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨b, ha⟩ ⟨b, hb⟩

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.Reachable ⟨a, ha⟩ ⟨b, hb⟩

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.Reachable ⟨a, ha⟩ ⟨b, hb⟩

case inr.inr
V : Type u
G : SimpleGraph V
v b : V
hvw : G.Adj v b
ha hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨b, ha⟩ ⟨b, hb⟩
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

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

pp: case inr
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
h : w ∈ p'.support
⊢ w ∈ p'.support

Tactic:
<;>

Goal state after:
case inl
V : Type u
G : SimpleGraph V
u v w x z : V
h : G.Adj x w
p' : G.Walk w z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
⊢ w ∈ p'.support

case inr
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
h : w ∈ p'.support
⊢ w ∈ p'.support
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
w u x : V
hadj : nil.toSubgraph.Adj w x
⊢ ¬nil.Nil

pp: case cons
V : Type u
G : SimpleGraph V
w u v x v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
hadj : (cons h✝ p✝).toSubgraph.Adj w x
⊢ ¬(cons h✝ p✝).Nil

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
w u x : V
hadj : nil.toSubgraph.Adj w x
⊢ ¬nil.Nil

case cons
V : Type u
G : SimpleGraph V
w u v x v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
hadj : (cons h✝ p✝).toSubgraph.Adj w x
⊢ ¬(cons h✝ p✝).Nil
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

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

pp: case cons
V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : e ∈ p✝.toSubgraph.edgeSet ↔ e ∈ p✝.edges
⊢ e ∈ (cons h✝ p✝).toSubgraph.edgeSet ↔ e ∈ (cons h✝ p✝).edges

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
u✝ : V
⊢ e ∈ nil.toSubgraph.edgeSet ↔ e ∈ nil.edges

case cons
V : Type u
G : SimpleGraph V
u v : V
e : Sym2 V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : e ∈ p✝.toSubgraph.edgeSet ↔ e ∈ p✝.edges
⊢ e ∈ (cons h✝ p✝).toSubgraph.edgeSet ↔ e ∈ (cons h✝ p✝).edges
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

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

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

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✝
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

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

pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (q : G.Walk w✝ w), (p✝.append q).toSubgraph = p✝.toSubgraph ⊔ q.toSubgraph
q : G.Walk w✝ w
⊢ ((cons h✝ p✝).append q).toSubgraph = (cons h✝ p✝).toSubgraph ⊔ q.toSubgraph

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
⊢ (nil.append q).toSubgraph = nil.toSubgraph ⊔ q.toSubgraph

case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (q : G.Walk w✝ w), (p✝.append q).toSubgraph = p✝.toSubgraph ⊔ q.toSubgraph
q : G.Walk w✝ w
⊢ ((cons h✝ p✝).append q).toSubgraph = (cons h✝ p✝).toSubgraph ⊔ q.toSubgraph
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case cons.e_a.verts
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
x✝ : V
⊢ x✝ ∈ (G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝).verts ↔ x✝ ∈ (G.subgraphOfAdj h✝).verts

pp: case cons.e_a.Adj
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
x✝¹ x✝ : V
⊢ (G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝).Adj x✝¹ x✝ ↔ (G.subgraphOfAdj h✝).Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case cons.e_a.verts
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
x✝ : V
⊢ x✝ ∈ (G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝).verts ↔ x✝ ∈ (G.subgraphOfAdj h✝).verts

case cons.e_a.Adj
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
x✝¹ x✝ : V
⊢ (G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝).Adj x✝¹ x✝ ↔ (G.subgraphOfAdj h✝).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

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

pp: case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
f : G →g G'
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : (Walk.map f p✝).toSubgraph = Subgraph.map f p✝.toSubgraph
⊢ (Walk.map f (cons h✝ p✝)).toSubgraph = Subgraph.map f (cons h✝ p✝).toSubgraph

Tactic:
<;>

Goal state after:
case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
f : G →g G'
u✝ : V
⊢ (Walk.map f nil).toSubgraph = Subgraph.map f nil.toSubgraph

case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
f : G →g G'
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : (Walk.map f p✝).toSubgraph = Subgraph.map f p✝.toSubgraph
⊢ (Walk.map f (cons h✝ p✝)).toSubgraph = Subgraph.map f (cons h✝ p✝).toSubgraph
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case refine_1.inl
W₁ : Type u_2
W₂ : Type u_3
v : W₁ ⊕ W₂
val✝ : W₁
h : s(Sum.inl val✝, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inl val✝, v) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

pp: case refine_1.inr
W₁ : Type u_2
W₂ : Type u_3
v : W₁ ⊕ W₂
val✝ : W₂
h : s(Sum.inr val✝, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inr val✝, v) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

Tactic:
<;>

Goal state after:
case refine_1.inl
W₁ : Type u_2
W₂ : Type u_3
v : W₁ ⊕ W₂
val✝ : W₁
h : s(Sum.inl val✝, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inl val✝, v) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

case refine_1.inr
W₁ : Type u_2
W₂ : Type u_3
v : W₁ ⊕ W₂
val✝ : W₂
h : s(Sum.inr val✝, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inr val✝, v) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case refine_1.inl.inl
W₁ : Type u_2
W₂ : Type u_3
val✝¹ val✝ : W₁
h : s(Sum.inl val✝¹, Sum.inl val✝) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inl val✝¹, Sum.inl val✝) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

pp: case refine_1.inl.inr
W₁ : Type u_2
W₂ : Type u_3
val✝¹ : W₁
val✝ : W₂
h : s(Sum.inl val✝¹, Sum.inr val✝) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inl val✝¹, Sum.inr val✝) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

pp: case refine_1.inr.inl
W₁ : Type u_2
W₂ : Type u_3
val✝¹ : W₂
val✝ : W₁
h : s(Sum.inr val✝¹, Sum.inl val✝) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inr val✝¹, Sum.inl val✝) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

pp: case refine_1.inr.inr
W₁ : Type u_2
W₂ : Type u_3
val✝¹ val✝ : W₂
h : s(Sum.inr val✝¹, Sum.inr val✝) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inr val✝¹, Sum.inr val✝) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

Tactic:
<;>

Goal state after:
case refine_1.inl.inl
W₁ : Type u_2
W₂ : Type u_3
val✝¹ val✝ : W₁
h : s(Sum.inl val✝¹, Sum.inl val✝) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inl val✝¹, Sum.inl val✝) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

case refine_1.inl.inr
W₁ : Type u_2
W₂ : Type u_3
val✝¹ : W₁
val✝ : W₂
h : s(Sum.inl val✝¹, Sum.inr val✝) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inl val✝¹, Sum.inr val✝) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

case refine_1.inr.inl
W₁ : Type u_2
W₂ : Type u_3
val✝¹ : W₂
val✝ : W₁
h : s(Sum.inr val✝¹, Sum.inl val✝) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inr val✝¹, Sum.inl val✝) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

case refine_1.inr.inr
W₁ : Type u_2
W₂ : Type u_3
val✝¹ val✝ : W₂
h : s(Sum.inr val✝¹, Sum.inr val✝) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inr val✝¹, Sum.inr val✝) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case inl
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
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

pp: case inr
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
left✝ : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
<;>

Goal state after:
case inl
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
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

case inr
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
left✝ : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Metric

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

pp: case refine_2.refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
⊢ 1 ≠ G.edist u v

Tactic:
<;>

Goal state after:
case refine_2.refine_1
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
⊢ 1 ≤ G.edist u v

case refine_2.refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
⊢ 1 ≠ G.edist u v
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case pos
V : Type u_1
u v : V
inst✝ : DecidableEq V
h : u = v
⊢ ⊥.edist u v = if u = v then 0 else ⊤

pp: case neg
V : Type u_1
u v : V
inst✝ : DecidableEq V
h : ¬u = v
⊢ ⊥.edist u v = if u = v then 0 else ⊤

Tactic:
<;>

Goal state after:
case pos
V : Type u_1
u v : V
inst✝ : DecidableEq V
h : u = v
⊢ ⊥.edist u v = if u = v then 0 else ⊤

case neg
V : Type u_1
u v : V
inst✝ : DecidableEq V
h : ¬u = v
⊢ ⊥.edist u v = if u = v then 0 else ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case pos
V : Type u_1
u v : V
inst✝ : DecidableEq V
h : u = v
⊢ ⊤.edist u v = if u = v then 0 else 1

pp: case neg
V : Type u_1
u v : V
inst✝ : DecidableEq V
h : ¬u = v
⊢ ⊤.edist u v = if u = v then 0 else 1

Tactic:
<;>

Goal state after:
case pos
V : Type u_1
u v : V
inst✝ : DecidableEq V
h : u = v
⊢ ⊤.edist u v = if u = v then 0 else 1

case neg
V : Type u_1
u v : V
inst✝ : DecidableEq V
h : ¬u = v
⊢ ⊤.edist u v = if u = v then 0 else 1
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case 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
r : V ⊕ V
hr : r ∈ right
l' : V ⊕ V
hl' : l' ∈ left
l : V
hl : Sum.inl l ∈ left
⊢ ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)

pp: case inr
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
r : V ⊕ V
hr : r ∈ right
l' : V ⊕ V
hl' : l' ∈ left
l : V
hl : Sum.inr l ∈ left
⊢ ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)

Tactic:
<;>

Goal state after:
case 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
r : V ⊕ V
hr : r ∈ right
l' : V ⊕ V
hl' : l' ∈ left
l : V
hl : Sum.inl l ∈ left
⊢ ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)

case inr
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
r : V ⊕ V
hr : r ∈ right
l' : V ⊕ V
hl' : l' ∈ left
l : V
hl : Sum.inr l ∈ left
⊢ ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case inl
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
right✝ : p.getVert (i' + 1) = v
hl : i' = i
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

pp: case inr
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
left✝ : p.getVert i' = v
hl : i' + 1 = i
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
<;>

Goal state after:
case inl
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
right✝ : p.getVert (i' + 1) = v
hl : i' = i
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

case inr
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
left✝ : p.getVert i' = v
hl : i' + 1 = i
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
u v : V
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W) (Sum.inl u)) ((Equiv.sumComm V W) (Sum.inl v)) ↔
    (G ⊕g H).Adj (Sum.inl u) (Sum.inl v)

pp: case inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
u : V
v : W
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W) (Sum.inl u)) ((Equiv.sumComm V W) (Sum.inr v)) ↔
    (G ⊕g H).Adj (Sum.inl u) (Sum.inr v)

pp: case inr.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' u : W
v : V
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W) (Sum.inr u)) ((Equiv.sumComm V W) (Sum.inl v)) ↔
    (G ⊕g H).Adj (Sum.inr u) (Sum.inl v)

pp: case inr.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' u v : W
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W) (Sum.inr u)) ((Equiv.sumComm V W) (Sum.inr v)) ↔
    (G ⊕g H).Adj (Sum.inr u) (Sum.inr v)

Tactic:
<;>

Goal state after:
case inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
u v : V
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W) (Sum.inl u)) ((Equiv.sumComm V W) (Sum.inl v)) ↔
    (G ⊕g H).Adj (Sum.inl u) (Sum.inl v)

case inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
u : V
v : W
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W) (Sum.inl u)) ((Equiv.sumComm V W) (Sum.inr v)) ↔
    (G ⊕g H).Adj (Sum.inl u) (Sum.inr v)

case inr.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' u : W
v : V
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W) (Sum.inr u)) ((Equiv.sumComm V W) (Sum.inl v)) ↔
    (G ⊕g H).Adj (Sum.inr u) (Sum.inl v)

case inr.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' u v : W
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W) (Sum.inr u)) ((Equiv.sumComm V W) (Sum.inr v)) ↔
    (G ⊕g H).Adj (Sum.inr u) (Sum.inr v)
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case pos
V : Type u_1
u v : V
h : u = v
⊢ ⊥.dist u v = 0

pp: case neg
V : Type u_1
u v : V
h : ¬u = v
⊢ ⊥.dist u v = 0

Tactic:
<;>

Goal state after:
case pos
V : Type u_1
u v : V
h : u = v
⊢ ⊥.dist u v = 0

case neg
V : Type u_1
u v : V
h : ¬u = v
⊢ ⊥.dist u v = 0
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case pos
V : Type u_1
u v : V
inst✝ : DecidableEq V
h : u = v
⊢ ⊤.dist u v = if u = v then 0 else 1

pp: case neg
V : Type u_1
u v : V
inst✝ : DecidableEq V
h : ¬u = v
⊢ ⊤.dist u v = if u = v then 0 else 1

Tactic:
<;>

Goal state after:
case pos
V : Type u_1
u v : V
inst✝ : DecidableEq V
h : u = v
⊢ ⊤.dist u v = if u = v then 0 else 1

case neg
V : Type u_1
u v : V
inst✝ : DecidableEq V
h : ¬u = v
⊢ ⊤.dist u v = if u = v then 0 else 1
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G →g G'
g : H →g H'
v : V ⊕ W
val✝ : V
⊢ (G ⊕g H).Adj (Sum.inl val✝) v → (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inl val✝)) (Sum.map (⇑f) (⇑g) v)

pp: case inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G →g G'
g : H →g H'
v : V ⊕ W
val✝ : W
⊢ (G ⊕g H).Adj (Sum.inr val✝) v → (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inr val✝)) (Sum.map (⇑f) (⇑g) v)

Tactic:
<;>

Goal state after:
case inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G →g G'
g : H →g H'
v : V ⊕ W
val✝ : V
⊢ (G ⊕g H).Adj (Sum.inl val✝) v → (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inl val✝)) (Sum.map (⇑f) (⇑g) v)

case inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v✝ v' : V
w w' : W
f : G →g G'
g : H →g H'
v : V ⊕ W
val✝ : W
⊢ (G ⊕g H).Adj (Sum.inr val✝) v → (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inr val✝)) (Sum.map (⇑f) (⇑g) v)