Theorem: Graph.Subgraph.contains_le (GroupComp/Subgraph.lean)

State before:
V : Type u_1
E : Type u_2
G : Graph V E
H✝ : Subgraph G
u v : V
H H' : Subgraph G
p : EdgePath G u v
hpH : contains H p
h : H ≤ H'
⊢ contains H' p
Tactic:
let ⟨hv, he⟩ := h
State after:
V : Type u_1
E : Type u_2
G : Graph V E
H✝ : Subgraph G
u v : V
H H' : Subgraph G
p : EdgePath G u v
hpH : contains H p
h : H ≤ H'
hv : H.verts ⊆ H'.verts
he : H.edges ⊆ H'.edges
⊢ contains H' p

State before:
V : Type u_1
E : Type u_2
G : Graph V E
H✝ : Subgraph G
u v : V
H H' : Subgraph G
p : EdgePath G u v
hpH : contains H p
h : H ≤ H'
hv : H.verts ⊆ H'.verts
he : H.edges ⊆ H'.edges
⊢ contains H' p
Tactic:
induction p with
  | nil => apply hv; exact hpH
  | cons e p' ih =>
    simp at hpH ⊢
    refine' ⟨he hpH.left, ih hpH.right⟩
State after:
no goals

State before:
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H✝ : Subgraph G
u v : V
H H' : Subgraph G
h : H ≤ H'
hv : H.verts ⊆ H'.verts
he : H.edges ⊆ H'.edges
v✝ : V
hpH : contains H (EdgePath.nil v✝)
⊢ contains H' (EdgePath.nil v✝)
Tactic:
apply hv
State after:
case nil.a
V : Type u_1
E : Type u_2
G : Graph V E
H✝ : Subgraph G
u v : V
H H' : Subgraph G
h : H ≤ H'
hv : H.verts ⊆ H'.verts
he : H.edges ⊆ H'.edges
v✝ : V
hpH : contains H (EdgePath.nil v✝)
⊢ v✝ ∈ H.verts

State before:
case nil.a
V : Type u_1
E : Type u_2
G : Graph V E
H✝ : Subgraph G
u v : V
H H' : Subgraph G
h : H ≤ H'
hv : H.verts ⊆ H'.verts
he : H.edges ⊆ H'.edges
v✝ : V
hpH : contains H (EdgePath.nil v✝)
⊢ v✝ ∈ H.verts
Tactic:
exact hpH
State after:
no goals

State before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H✝ : Subgraph G
u v : V
H H' : Subgraph G
h : H ≤ H'
hv : H.verts ⊆ H'.verts
he : H.edges ⊆ H'.edges
v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H' p'
hpH : contains H (EdgePath.cons e p')
⊢ contains H' (EdgePath.cons e p')
Tactic:
simp at hpH ⊢
State after:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H✝ : Subgraph G
u v : V
H H' : Subgraph G
h : H ≤ H'
hv : H.verts ⊆ H'.verts
he : H.edges ⊆ H'.edges
v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H' p'
hpH : e.edge ∈ H.edges ∧ contains H p'
⊢ e.edge ∈ H'.edges ∧ contains H' p'

State before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H✝ : Subgraph G
u v : V
H H' : Subgraph G
h : H ≤ H'
hv : H.verts ⊆ H'.verts
he : H.edges ⊆ H'.edges
v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H' p'
hpH : e.edge ∈ H.edges ∧ contains H p'
⊢ e.edge ∈ H'.edges ∧ contains H' p'
Tactic:
refine' ⟨he hpH.left, ih hpH.right⟩
State after:
no goals