internlm/Lean-Github huggingface dataset:
Theorem: cantor_diagonal
Proof state before:
case h
α : Type
f : α → α → Bool
⊢ ∀ (a : α), (fun a => !f a a) ≠ f a
Tactic:
intro a h
Proof state after:
case h
α : Type
f : α → α → Bool
a : α
h : (fun a => !f a a) = f a
⊢ False
Theorem: cantor_diagonal
Proof state before:
case h
α : Type
f : α → α → Bool
a : α
h : (fun a => !f a a) = f a
⊢ False
Tactic:
let h' := congrFun h a
Proof state after:
case h
α : Type
f : α → α → Bool
a : α
h : (fun a => !f a a) = f a
h' : (!f a a) = f a a := congrFun h a
⊢ False
Theorem: cantor_diagonal
Proof state before:
case h
α : Type
f : α → α → Bool
a : α
h : (fun a => !f a a) = f a
h' : (!f a a) = f a a := congrFun h a
⊢ False
Tactic:
by_cases c:f a a <;> simp [c] at h'
Proof state after:
no goals
Theorem: cantorSurjection_surjective
Proof state before:
⊢ ∀ (f : CantorTree' → Bool), ∃ t, cantorSurjection t = f
Tactic:
intro f
Proof state after:
f : CantorTree' → Bool
⊢ ∃ t, cantorSurjection t = f
Theorem: cantorSurjection_surjective
Proof state before:
f : CantorTree' → Bool
⊢ ∃ t, cantorSurjection t = f
Tactic:
use CantorTree.node f
Proof state after:
case h
f : CantorTree' → Bool
⊢ cantorSurjection (CantorTree.node f) = f
Theorem: cantorSurjection_surjective
Proof state before:
case h
f : CantorTree' → Bool
⊢ cantorSurjection (CantorTree.node f) = f
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.UniversalCover.Edge.bar_bar
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ bar G x₀ (bar G x₀ e) = e
Tactic:
simp only [bar, EdgeBetween.bar_bar]
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
      is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) } =
    e
Theorem: Graph.UniversalCover.Edge.bar_bar
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
      is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) } =
    e
Tactic:
ext
Proof state after:
case τ₀
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
        is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) }.τ₀ =
    e.τ₀

case τ₁
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
        is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) }.τ₁ =
    e.τ₁

case nxt
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ HEq
    { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
        is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) }.nxt
    e.nxt

case p
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ HEq
    { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
        is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) }.p
    e.p
Theorem: Graph.UniversalCover.Edge.bar_bar
Proof state before:
case τ₀
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
        is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) }.τ₀ =
    e.τ₀
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.UniversalCover.Edge.bar_bar
Proof state before:
case τ₁
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
        is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) }.τ₁ =
    e.τ₁
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.UniversalCover.Edge.bar_bar
Proof state before:
case nxt
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ HEq
    { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
        is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) }.nxt
    e.nxt
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.UniversalCover.Edge.bar_bar
Proof state before:
case p
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ HEq
    { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
        is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) }.p
    e.p
Tactic:
simp only [Eq.ndrec, id_eq, heq_eq_eq]
Proof state after:
case p
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ e.p:+e.nxt:+EdgeBetween.bar e.nxt = e.p
Theorem: Graph.UniversalCover.Edge.bar_bar
Proof state before:
case p
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ e.p:+e.nxt:+EdgeBetween.bar e.nxt = e.p
Tactic:
apply reducedConcat_cancel_pair
Proof state after:
case p.hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ reduced e.p
Theorem: Graph.UniversalCover.Edge.bar_bar
Proof state before:
case p.hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ reduced e.p
Tactic:
exact e.is_reduced
Proof state after:
no goals
Theorem: Graph.UniversalCover.Edge.bar_neq_self
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ e ≠ bar G x₀ e
Tactic:
intro contra
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
⊢ False
Theorem: Graph.UniversalCover.Edge.bar_neq_self
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
⊢ False
Tactic:
have : e.p.toList.length =  (bar G x₀ e).p.toList.length
   := by
    rw [← contra]
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (bar G x₀ e).p)
⊢ False
Theorem: Graph.UniversalCover.Edge.bar_neq_self
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (bar G x₀ e).p)
⊢ False
Tactic:
simp [bar, Edge.p] at this
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
⊢ False
Theorem: Graph.UniversalCover.Edge.bar_neq_self
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
⊢ False
Tactic:
let h' := concat_parity e.p e.nxt
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ ¬Even (List.length (EdgePath.toList e.p)) :=
  concat_parity e.p e.nxt
⊢ False
Theorem: Graph.UniversalCover.Edge.bar_neq_self
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ ¬Even (List.length (EdgePath.toList e.p)) :=
  concat_parity e.p e.nxt
⊢ False
Tactic:
rw [this] at h'
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ ¬Even (List.length (EdgePath.toList (e.p:+e.nxt)))
⊢ False
Theorem: Graph.UniversalCover.Edge.bar_neq_self
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ ¬Even (List.length (EdgePath.toList (e.p:+e.nxt)))
⊢ False
Tactic:
symm at h'
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : ¬Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ Even (List.length (EdgePath.toList (e.p:+e.nxt)))
⊢ False
Theorem: Graph.UniversalCover.Edge.bar_neq_self
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : ¬Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ Even (List.length (EdgePath.toList (e.p:+e.nxt)))
⊢ False
Tactic:
let h'' := not_iff_self  h'
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : ¬Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ Even (List.length (EdgePath.toList (e.p:+e.nxt)))
h'' : False := not_iff_self h'
⊢ False
Theorem: Graph.UniversalCover.Edge.bar_neq_self
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : ¬Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ Even (List.length (EdgePath.toList (e.p:+e.nxt)))
h'' : False := not_iff_self h'
⊢ False
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.UniversalCover.Edge.bar_neq_self
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
⊢ List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (bar G x₀ e).p)
Tactic:
rw [← contra]
Proof state after:
no goals
Theorem: Graph.UniversalCover.shift_heq
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ τ₀ τ₁ τ₂ : V
edge : E
init_eq : G.ι edge = τ₀
term_eq₁ : τ G edge = τ₁
term_eq₂ : τ G edge = τ₂
⊢ HEq { edge := edge, init_eq := init_eq, term_eq := term_eq₁ }
    { edge := edge, init_eq := init_eq, term_eq := term_eq₂ }
Tactic:
cases term_eq₁
Proof state after:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ τ₀ τ₂ : V
edge : E
init_eq : G.ι edge = τ₀
term_eq₂ : τ G edge = τ₂
⊢ HEq { edge := edge, init_eq := init_eq, term_eq := (_ : τ G edge = τ G edge) }
    { edge := edge, init_eq := init_eq, term_eq := term_eq₂ }
Theorem: Graph.UniversalCover.shift_heq
Proof state before:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ τ₀ τ₂ : V
edge : E
init_eq : G.ι edge = τ₀
term_eq₂ : τ G edge = τ₂
⊢ HEq { edge := edge, init_eq := init_eq, term_eq := (_ : τ G edge = τ G edge) }
    { edge := edge, init_eq := init_eq, term_eq := term_eq₂ }
Tactic:
cases term_eq₂
Proof state after:
case refl.refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ τ₀ : V
edge : E
init_eq : G.ι edge = τ₀
⊢ HEq { edge := edge, init_eq := init_eq, term_eq := (_ : τ G edge = τ G edge) }
    { edge := edge, init_eq := init_eq, term_eq := (_ : τ G edge = τ G edge) }
Theorem: Graph.UniversalCover.shift_heq
Proof state before:
case refl.refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ τ₀ : V
edge : E
init_eq : G.ι edge = τ₀
⊢ HEq { edge := edge, init_eq := init_eq, term_eq := (_ : τ G edge = τ G edge) }
    { edge := edge, init_eq := init_eq, term_eq := (_ : τ G edge = τ G edge) }
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.UniversalCover.rayToRev_proj_list
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p : EdgePath G τ x₀
hyp : reduced (reverse p)
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G x₀ τ p hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList p))
Tactic:
induction p with
| nil _ =>
simp [rayToRev, nil_toList]
| cons e p' ih =>
rename_i x₀' u u'
have red_cons : reduced (cons e p') := by
  rw [← reverse_reverse (cons e p')]
  apply reverse_reduced
  assumption
have red_p' : reduced p' := by
  apply tail_reduced e p'
  assumption
have red' : reduced p'.reverse := by
  apply reverse_reduced
  assumption
simp [rayToRev, cons_toList, concat_toList, ih red']
Proof state after:
no goals
Theorem: Graph.UniversalCover.rayToRev_proj_list
Proof state before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ v✝ : V
hyp : reduced (reverse (nil v✝))
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G v✝ v✝ (nil v✝) hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (nil v✝)))
Tactic:
simp [rayToRev, nil_toList]
Proof state after:
no goals
Theorem: Graph.UniversalCover.rayToRev_proj_list
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u✝ w✝ p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u✝ v✝ (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))
Tactic:
rename_i x₀' u u'
Proof state after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))
Theorem: Graph.UniversalCover.rayToRev_proj_list
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))
Tactic:
have red_cons : reduced (cons e p') := by
  rw [← reverse_reverse (cons e p')]
  apply reverse_reduced
  assumption
Proof state after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))
Theorem: Graph.UniversalCover.rayToRev_proj_list
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))
Tactic:
have red_p' : reduced p' := by
  apply tail_reduced e p'
  assumption
Proof state after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
red_p' : reduced p'
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))
Theorem: Graph.UniversalCover.rayToRev_proj_list
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
red_p' : reduced p'
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))
Tactic:
have red' : reduced p'.reverse := by
  apply reverse_reduced
  assumption
Proof state after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
red_p' : reduced p'
red' : reduced (reverse p')
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))
Theorem: Graph.UniversalCover.rayToRev_proj_list
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
red_p' : reduced p'
red' : reduced (reverse p')
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))
Tactic:
simp [rayToRev, cons_toList, concat_toList, ih red']
Proof state after:
no goals
Theorem: Graph.UniversalCover.rayToRev_proj_list
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
⊢ reduced (cons e p')
Tactic:
rw [← reverse_reverse (cons e p')]
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
⊢ reduced (reverse (reverse (cons e p')))
Theorem: Graph.UniversalCover.rayToRev_proj_list
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
⊢ reduced (reverse (reverse (cons e p')))
Tactic:
apply reverse_reduced
Proof state after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
⊢ reduced (reverse (cons e p'))
Theorem: Graph.UniversalCover.rayToRev_proj_list
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
⊢ reduced (reverse (cons e p'))
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.UniversalCover.rayToRev_proj_list
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
⊢ reduced p'
Tactic:
apply tail_reduced e p'
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
⊢ reduced (cons e p')
Theorem: Graph.UniversalCover.rayToRev_proj_list
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
⊢ reduced (cons e p')
Tactic:
assumption
Proof state after:
no goals