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

State before:
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ : V
p : EdgePath G a✝¹ a✝
w✝ : V
e : EdgeBetween G a✝ w✝
⊢ contains H (EdgePath.concat p e) ↔ e.edge ∈ H.edges ∧ contains H p
Tactic:
induction p with
  | nil =>
    rw [EdgePath.concat]
    simp only [contains_cons, contains_nil, and_congr_right_iff]
    intro he
    have := e.init_eq ▸ H.edges_init e.edge he
    have := e.term_eq ▸ H.edges_terminal e.edge he
    simp_all only
  | cons e p' ih =>
    rw [EdgePath.concat_cons]
    aesop
State after:
no goals

State before:
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝ v✝ : V
e : EdgeBetween G v✝ w✝
⊢ contains H (EdgePath.concat (EdgePath.nil v✝) e) ↔ e.edge ∈ H.edges ∧ contains H (EdgePath.nil v✝)
Tactic:
rw [EdgePath.concat]
State after:
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝ v✝ : V
e : EdgeBetween G v✝ w✝
⊢ contains H (EdgePath.cons e (EdgePath.nil w✝)) ↔ e.edge ∈ H.edges ∧ contains H (EdgePath.nil v✝)

State before:
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝ v✝ : V
e : EdgeBetween G v✝ w✝
⊢ contains H (EdgePath.cons e (EdgePath.nil w✝)) ↔ e.edge ∈ H.edges ∧ contains H (EdgePath.nil v✝)
Tactic:
simp only [contains_cons, contains_nil, and_congr_right_iff]
State after:
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝ v✝ : V
e : EdgeBetween G v✝ w✝
⊢ e.edge ∈ H.edges → (w✝ ∈ H.verts ↔ v✝ ∈ H.verts)

State before:
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝ v✝ : V
e : EdgeBetween G v✝ w✝
⊢ e.edge ∈ H.edges → (w✝ ∈ H.verts ↔ v✝ ∈ H.verts)
Tactic:
intro he
State after:
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝ v✝ : V
e : EdgeBetween G v✝ w✝
he : e.edge ∈ H.edges
⊢ w✝ ∈ H.verts ↔ v✝ ∈ H.verts

State before:
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝ v✝ : V
e : EdgeBetween G v✝ w✝
he : e.edge ∈ H.edges
⊢ w✝ ∈ H.verts ↔ v✝ ∈ H.verts
Tactic:
have := e.init_eq ▸ H.edges_init e.edge he
State after:
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝ v✝ : V
e : EdgeBetween G v✝ w✝
he : e.edge ∈ H.edges
this : v✝ ∈ H.verts
⊢ w✝ ∈ H.verts ↔ v✝ ∈ H.verts

State before:
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝ v✝ : V
e : EdgeBetween G v✝ w✝
he : e.edge ∈ H.edges
this : v✝ ∈ H.verts
⊢ w✝ ∈ H.verts ↔ v✝ ∈ H.verts
Tactic:
have := e.term_eq ▸ H.edges_terminal e.edge he
State after:
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝ v✝ : V
e : EdgeBetween G v✝ w✝
he : e.edge ∈ H.edges
this✝ : v✝ ∈ H.verts
this : w✝ ∈ H.verts
⊢ w✝ ∈ H.verts ↔ v✝ ∈ H.verts

State before:
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝ v✝ : V
e : EdgeBetween G v✝ w✝
he : e.edge ∈ H.edges
this✝ : v✝ ∈ H.verts
this : w✝ ∈ H.verts
⊢ w✝ ∈ H.verts ↔ v✝ ∈ H.verts
Tactic:
simp_all only
State after:
no goals

State before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝¹ v✝ w✝ u✝ : V
e✝ : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : ∀ {e : EdgeBetween G u✝ w✝¹}, contains H (EdgePath.concat p' e) ↔ e.edge ∈ H.edges ∧ contains H p'
e : EdgeBetween G u✝ w✝¹
⊢ contains H (EdgePath.concat (EdgePath.cons e✝ p') e) ↔ e.edge ∈ H.edges ∧ contains H (EdgePath.cons e✝ p')
Tactic:
rw [EdgePath.concat_cons]
State after:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝¹ v✝ w✝ u✝ : V
e✝ : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : ∀ {e : EdgeBetween G u✝ w✝¹}, contains H (EdgePath.concat p' e) ↔ e.edge ∈ H.edges ∧ contains H p'
e : EdgeBetween G u✝ w✝¹
⊢ contains H (EdgePath.cons e✝ (EdgePath.concat p' e)) ↔ e.edge ∈ H.edges ∧ contains H (EdgePath.cons e✝ p')

State before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝¹ v✝ w✝ u✝ : V
e✝ : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : ∀ {e : EdgeBetween G u✝ w✝¹}, contains H (EdgePath.concat p' e) ↔ e.edge ∈ H.edges ∧ contains H p'
e : EdgeBetween G u✝ w✝¹
⊢ contains H (EdgePath.cons e✝ (EdgePath.concat p' e)) ↔ e.edge ∈ H.edges ∧ contains H (EdgePath.cons e✝ p')
Tactic:
aesop
State after:
no goals