internlm/Lean-Github huggingface dataset:
Theorem: Graph.PathClass.mul_assoc'
Proof state before:
case mk.mk.mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
b : EdgePath G w u
c : EdgePath G u u'
⊢ (Quot.mk Reduction a ≫ Quot.mk Reduction b) ≫ Quot.mk Reduction c =
    Quot.mk Reduction a ≫ Quot.mk Reduction b ≫ Quot.mk Reduction c
Tactic:
simp [append_assoc]
Proof state after:
no goals
Theorem: Graph.PathClass.inv_eq_inv
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G v w
p : u ⟶ v
⊢ PathClass.inv p = inv p
Tactic:
rw [← Groupoid.inv_eq_inv]
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G v w
p : u ⟶ v
⊢ PathClass.inv p = Groupoid.inv p
Theorem: Graph.PathClass.inv_eq_inv
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G v w
p : u ⟶ v
⊢ PathClass.inv p = Groupoid.inv p
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.Subgraph.edges_terminal
Proof state before:
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
⊢ ∀ e ∈ H.edges, τ G e ∈ H.verts
Tactic:
intro e he
Proof state after:
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ τ G e ∈ H.verts
Theorem: Graph.Subgraph.edges_terminal
Proof state before:
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ τ G e ∈ H.verts
Tactic:
rw [← G.ι_bar e]
Proof state after:
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ G.ι (G.bar e) ∈ H.verts
Theorem: Graph.Subgraph.edges_terminal
Proof state before:
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ G.ι (G.bar e) ∈ H.verts
Tactic:
apply H.edges_init
Proof state after:
case a
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ G.bar e ∈ H.edges
Theorem: Graph.Subgraph.edges_terminal
Proof state before:
case a
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ G.bar e ∈ H.edges
Tactic:
apply H.edges_bar
Proof state after:
case a.a
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ e ∈ H.edges
Theorem: Graph.Subgraph.edges_terminal
Proof state before:
case a.a
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ e ∈ H.edges
Tactic:
exact he
Proof state after:
no goals
Theorem: Graph.Subgraph.bar_edges
Proof state before:
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
ebH : G.bar e ∈ H.edges
⊢ e ∈ H.edges
Tactic:
rw [← G.bar_bar e]
Proof state after:
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
ebH : G.bar e ∈ H.edges
⊢ G.bar (G.bar e) ∈ H.edges
Theorem: Graph.Subgraph.bar_edges
Proof state before:
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
ebH : G.bar e ∈ H.edges
⊢ G.bar (G.bar e) ∈ H.edges
Tactic:
apply edges_bar
Proof state after:
case a
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
ebH : G.bar e ∈ H.edges
⊢ G.bar e ∈ H.edges
Theorem: Graph.Subgraph.bar_edges
Proof state before:
case a
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
ebH : G.bar e ∈ H.edges
⊢ G.bar e ∈ H.edges
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.Subgraph.contains_concat
Proof 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
Proof state after:
no goals
Theorem: Graph.Subgraph.contains_concat
Proof 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]
Proof 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✝)
Theorem: Graph.Subgraph.contains_concat
Proof 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]
Proof 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)
Theorem: Graph.Subgraph.contains_concat
Proof 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
Proof 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
Theorem: Graph.Subgraph.contains_concat
Proof 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
Proof 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
Theorem: Graph.Subgraph.contains_concat
Proof 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
Proof 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
Theorem: Graph.Subgraph.contains_concat
Proof 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
Proof state after:
no goals
Theorem: Graph.Subgraph.contains_concat
Proof 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]
Proof 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')
Theorem: Graph.Subgraph.contains_concat
Proof 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
Proof state after:
no goals
Theorem: Graph.Subgraph.contains_head
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v : V
p : EdgePath G u v
⊢ contains H p → u ∈ H.verts
Tactic:
induction p with
| nil => simp
| cons e _ _ =>
  simp_rw [← e.init_eq]
  aesop
Proof state after:
no goals
Theorem: Graph.Subgraph.contains_head
Proof state before:
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ : V
⊢ contains H (EdgePath.nil v✝) → v✝ ∈ H.verts
Tactic:
simp
Proof state after:
no goals
Theorem: Graph.Subgraph.contains_head
Proof state before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
a✝ : EdgePath G w✝ u✝
a_ih✝ : contains H a✝ → w✝ ∈ H.verts
⊢ contains H (EdgePath.cons e a✝) → v✝ ∈ H.verts
Tactic:
simp_rw [← e.init_eq]
Proof state after:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
a✝ : EdgePath G w✝ u✝
a_ih✝ : contains H a✝ → w✝ ∈ H.verts
⊢ contains H (EdgePath.cons e a✝) → G.ι e.edge ∈ H.verts
Theorem: Graph.Subgraph.contains_head
Proof state before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
a✝ : EdgePath G w✝ u✝
a_ih✝ : contains H a✝ → w✝ ∈ H.verts
⊢ contains H (EdgePath.cons e a✝) → G.ι e.edge ∈ H.verts
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.Subgraph.contains_tail
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v : V
p : EdgePath G u v
⊢ contains H p → v ∈ H.verts
Tactic:
induction p <;> aesop
Proof state after:
no goals
Theorem: Graph.Subgraph.contains_append
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v w : V
p : EdgePath G u v
p' : EdgePath G v w
⊢ contains H (p ++ p') ↔ contains H p ∧ contains H p'
Tactic:
induction p <;> aesop
Proof state after:
no goals
Theorem: Graph.Subgraph.contains_reverse
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v : V
p : EdgePath G u v
⊢ contains H p → contains H (EdgePath.reverse p)
Tactic:
induction p with
  | nil => simp only  [contains_nil, EdgePath.reverse_nil, imp_self]
  | cons e p' ih =>
    rw [EdgePath.reverse_cons]
    simp only [contains_cons, contains_concat, EdgeBetween.bar_eq_bar, and_imp]
    intro he hp'H
    exact ⟨H.edges_bar _ he, ih hp'H⟩
Proof state after:
no goals
Theorem: Graph.Subgraph.contains_reverse
Proof state before:
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ : V
⊢ contains H (EdgePath.nil v✝) → contains H (EdgePath.reverse (EdgePath.nil v✝))
Tactic:
simp only  [contains_nil, EdgePath.reverse_nil, imp_self]
Proof state after:
no goals
Theorem: Graph.Subgraph.contains_reverse
Proof state before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H (EdgePath.reverse p')
⊢ contains H (EdgePath.cons e p') → contains H (EdgePath.reverse (EdgePath.cons e p'))
Tactic:
rw [EdgePath.reverse_cons]
Proof state after:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H (EdgePath.reverse p')
⊢ contains H (EdgePath.cons e p') → contains H (EdgePath.concat (EdgePath.reverse p') (EdgeBetween.bar e))
Theorem: Graph.Subgraph.contains_reverse
Proof state before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H (EdgePath.reverse p')
⊢ contains H (EdgePath.cons e p') → contains H (EdgePath.concat (EdgePath.reverse p') (EdgeBetween.bar e))
Tactic:
simp only [contains_cons, contains_concat, EdgeBetween.bar_eq_bar, and_imp]
Proof state after:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H (EdgePath.reverse p')
⊢ e.edge ∈ H.edges → contains H p' → G.bar e.edge ∈ H.edges ∧ contains H (EdgePath.reverse p')
Theorem: Graph.Subgraph.contains_reverse
Proof state before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H (EdgePath.reverse p')
⊢ e.edge ∈ H.edges → contains H p' → G.bar e.edge ∈ H.edges ∧ contains H (EdgePath.reverse p')
Tactic:
intro he hp'H
Proof state after:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H (EdgePath.reverse p')
he : e.edge ∈ H.edges
hp'H : contains H p'
⊢ G.bar e.edge ∈ H.edges ∧ contains H (EdgePath.reverse p')
Theorem: Graph.Subgraph.contains_reverse
Proof state before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H (EdgePath.reverse p')
he : e.edge ∈ H.edges
hp'H : contains H p'
⊢ G.bar e.edge ∈ H.edges ∧ contains H (EdgePath.reverse p')
Tactic:
exact ⟨H.edges_bar _ he, ih hp'H⟩
Proof state after:
no goals
Theorem: Graph.Subgraph.contains_le
Proof 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
Proof 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
Theorem: Graph.Subgraph.contains_le
Proof 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⟩
Proof state after:
no goals
Theorem: Graph.Subgraph.contains_le
Proof 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
Proof 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
Theorem: Graph.Subgraph.contains_le
Proof 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
Proof state after:
no goals
Theorem: Graph.Subgraph.contains_le
Proof 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 ⊢
Proof 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'
Theorem: Graph.Subgraph.contains_le
Proof 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⟩
Proof state after:
no goals
Theorem: Graph.Graph.hom.preserve_terminal
Proof state before:
V : Type u_2
E : Type u_3
V' : Type u_1
E' : Type u_4
G : Graph V E
G' : Graph V' E'
φ : hom G G'
e : E
⊢ φ.toFuncV (τ G e) = τ G' (φ.toFuncE e)
Tactic:
rw [← G.ι_bar, ← G'.ι_bar, preserve_init, preserve_bar]
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.path_class_of_contains_path
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
p : EdgePath G u v
hpΓ : Subgraph.contains Γ.toSubgraph p
⊢ [[p]] = u ⤳[Γ] v
Tactic:
apply Γ.path_unique (Γ.vertex_coe u) (Γ.vertex_coe v)
Proof state after:
case a
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
p : EdgePath G u v
hpΓ : Subgraph.contains Γ.toSubgraph p
⊢ Subgraph.contains Γ.toSubgraph p
Theorem: Graph.SpanningSubtree.path_class_of_contains_path
Proof state before:
case a
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
p : EdgePath G u v
hpΓ : Subgraph.contains Γ.toSubgraph p
⊢ Subgraph.contains Γ.toSubgraph p
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.tree_path_id
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u : V
⊢ (u ⤳[Γ] u) = 𝟙 u
Tactic:
symm
Proof state after:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u : V
⊢ 𝟙 u = u ⤳[Γ] u
Theorem: Graph.SpanningSubtree.tree_path_id
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u : V
⊢ 𝟙 u = u ⤳[Γ] u
Tactic:
apply path_class_of_contains_path
Proof state after:
case hpΓ
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u : V
⊢ Subgraph.contains Γ.toSubgraph (EdgePath.nil u)
Theorem: Graph.SpanningSubtree.tree_path_id
Proof state before:
case hpΓ
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u : V
⊢ Subgraph.contains Γ.toSubgraph (EdgePath.nil u)
Tactic:
simp
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.tree_path_comp
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v w : V
⊢ ((u ⤳[Γ] v) ≫ v ⤳[Γ] w) = u ⤳[Γ] w
Tactic:
apply path_class_of_contains_path
Proof state after:
case hpΓ
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v w : V
⊢ Subgraph.contains Γ.toSubgraph
    (↑((toSubtree Γ).toPreconnectedSubgraph.path (vertex_coe Γ u) (vertex_coe Γ v)) ++
      ↑((toSubtree Γ).toPreconnectedSubgraph.path (vertex_coe Γ v) (vertex_coe Γ w)))
Theorem: Graph.SpanningSubtree.tree_path_comp
Proof state before:
case hpΓ
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v w : V
⊢ Subgraph.contains Γ.toSubgraph
    (↑((toSubtree Γ).toPreconnectedSubgraph.path (vertex_coe Γ u) (vertex_coe Γ v)) ++
      ↑((toSubtree Γ).toPreconnectedSubgraph.path (vertex_coe Γ v) (vertex_coe Γ w)))
Tactic:
simp
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.tree_path_comp_right
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v w x : V
p : w ⟶ x
⊢ (u ⤳[Γ] v) ≫ (v ⤳[Γ] w) ≫ p = (u ⤳[Γ] w) ≫ p
Tactic:
rw [← Category.assoc, tree_path_comp]
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.singleton_tree_path
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e : EdgeBetween G u v
heΓ : e.edge ∈ Γ.edges
⊢ [[singletonPath e]] = u ⤳[Γ] v
Tactic:
apply path_class_of_contains_path
Proof state after:
case hpΓ
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e : EdgeBetween G u v
heΓ : e.edge ∈ Γ.edges
⊢ Subgraph.contains Γ.toSubgraph (singletonPath e)
Theorem: Graph.SpanningSubtree.singleton_tree_path
Proof state before:
case hpΓ
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e : EdgeBetween G u v
heΓ : e.edge ∈ Γ.edges
⊢ Subgraph.contains Γ.toSubgraph (singletonPath e)
Tactic:
simp
Proof state after:
case hpΓ
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e : EdgeBetween G u v
heΓ : e.edge ∈ Γ.edges
⊢ e.edge ∈ Γ.edges
Theorem: Graph.SpanningSubtree.singleton_tree_path
Proof state before:
case hpΓ
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e : EdgeBetween G u v
heΓ : e.edge ∈ Γ.edges
⊢ e.edge ∈ Γ.edges
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.surround_tree_edge
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e : EdgeBetween G u v
heΓ : e.edge ∈ Γ.edges
⊢ surroundEdge Γ e = 𝟙 (base Γ)
Tactic:
simp [surroundEdge, Γ.singleton_tree_path heΓ]
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.opp_path_eq_inv
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
⊢ (u ⤳[Γ] v) = inv (v ⤳[Γ] u)
Tactic:
rw [← hom_comp_eq_id]
Proof state after:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
⊢ ((v ⤳[Γ] u) ≫ u ⤳[Γ] v) = 𝟙 v
Theorem: Graph.SpanningSubtree.opp_path_eq_inv
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
⊢ ((v ⤳[Γ] u) ≫ u ⤳[Γ] v) = 𝟙 v
Tactic:
trans (v ⤳[Γ] v)
<;> simp
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.path_to_base_eq
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u : V
⊢ (u ⤳[Γ] base Γ) = inv (base Γ ⤳[Γ] u)
Tactic:
apply opp_path_eq_inv
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.surround_append
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v w : V
p : u ⟶ v
q : v ⟶ w
⊢ surround Γ p ≫ surround Γ q = surround Γ (p ≫ q)
Tactic:
simp only [surround, path_to_base_eq, Category.assoc, IsIso.inv_hom_id_assoc]
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.surround_nil
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u : V
⊢ surround Γ (𝟙 u) = 𝟙 (base Γ)
Tactic:
simp only [surround, path_to_base_eq, Category.id_comp, IsIso.hom_inv_id]
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.surround_cons
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
v✝ w✝ : V
e : EdgeBetween G v✝ w✝
a✝ : V
p : EdgePath G w✝ a✝
⊢ surround Γ [[EdgePath.cons e p]] = surroundEdge Γ e ≫ surround Γ [[p]]
Tactic:
erw [Graph.EdgePath.cons_eq_append_singletonPath, surround_append]
Proof state after:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
v✝ w✝ : V
e : EdgeBetween G v✝ w✝
a✝ : V
p : EdgePath G w✝ a✝
⊢ surround Γ [[singletonPath e ++ p]] = surround Γ ([[singletonPath e]] ≫ [[p]])
Theorem: Graph.SpanningSubtree.surround_cons
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
v✝ w✝ : V
e : EdgeBetween G v✝ w✝
a✝ : V
p : EdgePath G w✝ a✝
⊢ surround Γ [[singletonPath e ++ p]] = surround Γ ([[singletonPath e]] ≫ [[p]])
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.surround_inv
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
p : u ⟶ v
⊢ surround Γ (inv p) = inv (surround Γ p)
Tactic:
rw [← hom_comp_eq_id]
Proof state after:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
p : u ⟶ v
⊢ surround Γ p ≫ surround Γ (inv p) = 𝟙 (base Γ)
Theorem: Graph.SpanningSubtree.surround_inv
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
p : u ⟶ v
⊢ surround Γ p ≫ surround Γ (inv p) = 𝟙 (base Γ)
Tactic:
simp only [surround, path_to_base_eq, Category.assoc, IsIso.inv_hom_id_assoc,
IsIso.hom_inv_id_assoc, IsIso.hom_inv_id]
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.surround_loop
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
p : base Γ ⟶ base Γ
⊢ surround Γ p = p
Tactic:
simp only [surround, tree_path_id, Category.comp_id, Category.id_comp]
Proof state after:
no goals
Theorem: Graph.SpanningSubtree.surroundEdge_bar
Proof state before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e : EdgeBetween G u v
⊢ surroundEdge Γ (EdgeBetween.bar e) = inv (surroundEdge Γ e)
Tactic:
rw [surroundEdge, surroundEdge, ← surround_inv, Graph.EdgePath.singletonPath_bar,
  Graph.PathClass.reverse_class_eq_inv, Graph.PathClass.inv_eq_inv]
Proof state after:
no goals