internlm/Lean-Github huggingface dataset:
Theorem: Graph.cons_homotopic_redCons
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 u v
p : EdgePath G v w
h : ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
⊢ cons e (cons (EdgeBetween.bar e) t) = nil u ++ cons e (cons (EdgeBetween.bar e) t)
Tactic:
simp [nil_append]
Proof state after:
no goals
Theorem: Graph.reduction_nil
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
⊢ reduction (nil v) = nil v
Tactic:
simp [reduction]
Proof state after:
no goals
Theorem: Graph.reduction_cons
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
e : EdgeBetween G v w
p : EdgePath G w u
⊢ reduction (cons e p) = redCons e (reduction p)
Tactic:
simp [reduction]
Proof state after:
no goals
Theorem: Graph.reduction_reduced
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w : V
p : EdgePath G v w
⊢ reduced (reduction p)
Tactic:
induction p with
| nil _ =>
  simp [reduction_nil, reduced_nil]
| cons e p ih =>
  apply reduced_redCons
  assumption
Proof state after:
no goals
Theorem: Graph.reduction_reduced
Proof state before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ : V
⊢ reduced (reduction (nil v✝))
Tactic:
simp [reduction_nil, reduced_nil]
Proof state after:
no goals
Theorem: Graph.reduction_reduced
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced (reduction p)
⊢ reduced (reduction (cons e p))
Tactic:
apply reduced_redCons
Proof state after:
case cons.hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced (reduction p)
⊢ reduced (reduction p)
Theorem: Graph.reduction_reduced
Proof state before:
case cons.hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced (reduction p)
⊢ reduced (reduction p)
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.reduction_eq_self_of_reduced
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w : V
p : EdgePath G v w
hyp : reduced p
⊢ reduction p = p
Tactic:
induction p with
| nil _ =>
  simp [reduction_nil]
| cons e p ih =>
  rw [reduction_cons]
  have teq : reduction p = p := by
    apply ih
    apply tail_reduced
    assumption
  rw [teq]
  apply redCons_eq_cons_of_reduced
  assumption
Proof state after:
no goals
Theorem: Graph.reduction_eq_self_of_reduced
Proof state before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ : V
hyp : reduced (nil v✝)
⊢ reduction (nil v✝) = nil v✝
Tactic:
simp [reduction_nil]
Proof state after:
no goals
Theorem: Graph.reduction_eq_self_of_reduced
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ reduction (cons e p) = cons e p
Tactic:
rw [reduction_cons]
Proof state after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ redCons e (reduction p) = cons e p
Theorem: Graph.reduction_eq_self_of_reduced
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ redCons e (reduction p) = cons e p
Tactic:
have teq : reduction p = p := by
  apply ih
  apply tail_reduced
  assumption
Proof state after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
teq : reduction p = p
⊢ redCons e (reduction p) = cons e p
Theorem: Graph.reduction_eq_self_of_reduced
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
teq : reduction p = p
⊢ redCons e (reduction p) = cons e p
Tactic:
rw [teq]
Proof state after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
teq : reduction p = p
⊢ redCons e p = cons e p
Theorem: Graph.reduction_eq_self_of_reduced
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
teq : reduction p = p
⊢ redCons e p = cons e p
Tactic:
apply redCons_eq_cons_of_reduced
Proof state after:
case cons.hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
teq : reduction p = p
⊢ reduced (cons e p)
Theorem: Graph.reduction_eq_self_of_reduced
Proof state before:
case cons.hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
teq : reduction p = p
⊢ reduced (cons e p)
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.reduction_eq_self_of_reduced
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ reduction p = p
Tactic:
apply ih
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ reduced p
Theorem: Graph.reduction_eq_self_of_reduced
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ reduced p
Tactic:
apply tail_reduced
Proof state after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ reduced (cons ?e p)

case u
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ V

case e
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ EdgeBetween G ?u w✝
Theorem: Graph.reduction_eq_self_of_reduced
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ reduced (cons ?e p)

case u
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ V

case e
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ EdgeBetween G ?u w✝
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.reduction_homotopic_self
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w : V
p : EdgePath G v w
⊢ [[reduction p]] = [[p]]
Tactic:
induction p with
| nil _ =>
  simp [reduction_nil]
| cons e p ih =>
  simp [reduction_cons, ←cons_homotopic_redCons]
  apply cons_equiv_of_equiv
  assumption
Proof state after:
no goals
Theorem: Graph.reduction_homotopic_self
Proof state before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ : V
⊢ [[reduction (nil v✝)]] = [[nil v✝]]
Tactic:
simp [reduction_nil]
Proof state after:
no goals
Theorem: Graph.reduction_homotopic_self
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : [[reduction p]] = [[p]]
⊢ [[reduction (cons e p)]] = [[cons e p]]
Tactic:
simp [reduction_cons, ←cons_homotopic_redCons]
Proof state after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : [[reduction p]] = [[p]]
⊢ [[cons e (reduction p)]] = [[cons e p]]
Theorem: Graph.reduction_homotopic_self
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : [[reduction p]] = [[p]]
⊢ [[cons e (reduction p)]] = [[cons e p]]
Tactic:
apply cons_equiv_of_equiv
Proof state after:
case cons.a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : [[reduction p]] = [[p]]
⊢ [[reduction p]] = [[p]]
Theorem: Graph.reduction_homotopic_self
Proof state before:
case cons.a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : [[reduction p]] = [[p]]
⊢ [[reduction p]] = [[p]]
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.redCons_parity_neq
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 u v
p : EdgePath G v w
⊢ Even (List.length (toList (redCons e p))) ↔ ¬Even (List.length (toList p))
Tactic:
cases prepend_cases e p with
| inl h =>
  rw [h]
  simp only [cons_toList, List.length_cons]
  apply Nat.even_add_one
| inr h =>
  let ⟨t, h₁, h₂⟩ := h
  rw [h₂, h₁]
  simp  [cons_toList, List.length_cons, Nat.even_add_one]
Proof state after:
no goals
Theorem: Graph.redCons_parity_neq
Proof state before:
case inl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : redCons e p = cons e p
⊢ Even (List.length (toList (redCons e p))) ↔ ¬Even (List.length (toList p))
Tactic:
rw [h]
Proof state after:
case inl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : redCons e p = cons e p
⊢ Even (List.length (toList (cons e p))) ↔ ¬Even (List.length (toList p))
Theorem: Graph.redCons_parity_neq
Proof state before:
case inl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : redCons e p = cons e p
⊢ Even (List.length (toList (cons e p))) ↔ ¬Even (List.length (toList p))
Tactic:
simp only [cons_toList, List.length_cons]
Proof state after:
case inl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : redCons e p = cons e p
⊢ Even (Nat.succ (List.length (toList p))) ↔ ¬Even (List.length (toList p))
Theorem: Graph.redCons_parity_neq
Proof state before:
case inl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : redCons e p = cons e p
⊢ Even (Nat.succ (List.length (toList p))) ↔ ¬Even (List.length (toList p))
Tactic:
apply Nat.even_add_one
Proof state after:
no goals
Theorem: Graph.redCons_parity_neq
Proof state before:
case inr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
⊢ Even (List.length (toList (redCons e p))) ↔ ¬Even (List.length (toList p))
Tactic:
let ⟨t, h₁, h₂⟩ := h
Proof state after:
case inr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
⊢ Even (List.length (toList (redCons e p))) ↔ ¬Even (List.length (toList p))
Theorem: Graph.redCons_parity_neq
Proof state before:
case inr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
⊢ Even (List.length (toList (redCons e p))) ↔ ¬Even (List.length (toList p))
Tactic:
rw [h₂, h₁]
Proof state after:
case inr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
⊢ Even (List.length (toList t)) ↔ ¬Even (List.length (toList (cons (EdgeBetween.bar e) t)))
Theorem: Graph.redCons_parity_neq
Proof state before:
case inr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
⊢ Even (List.length (toList t)) ↔ ¬Even (List.length (toList (cons (EdgeBetween.bar e) t)))
Tactic:
simp  [cons_toList, List.length_cons, Nat.even_add_one]
Proof state after:
no goals
Theorem: Graph.reducedConcat_reduced
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
⊢ reduced (p:+e)
Tactic:
simp only [reducedConcat]
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
⊢ reduced (reverse (redCons (EdgeBetween.bar e) (reverse p)))
Theorem: Graph.reducedConcat_reduced
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
⊢ reduced (reverse (redCons (EdgeBetween.bar e) (reverse 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
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
⊢ reduced (redCons (EdgeBetween.bar e) (reverse p))
Theorem: Graph.reducedConcat_reduced
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
⊢ reduced (redCons (EdgeBetween.bar e) (reverse p))
Tactic:
apply reduced_redCons
Proof state after:
case a.hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
⊢ reduced (reverse p)
Theorem: Graph.reducedConcat_reduced
Proof state before:
case a.hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
⊢ reduced (reverse p)
Tactic:
apply reverse_reduced
Proof state after:
case a.hyp.a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
⊢ reduced p
Theorem: Graph.reducedConcat_reduced
Proof state before:
case a.hyp.a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
⊢ reduced p
Tactic:
apply hyp
Proof state after:
no goals
Theorem: Graph.reducedConcat_cancel_pair
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
⊢ p:+e:+EdgeBetween.bar e = p
Tactic:
have hyp' :=  reverse_reduced p hyp
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
⊢ p:+e:+EdgeBetween.bar e = p
Theorem: Graph.reducedConcat_cancel_pair
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
⊢ p:+e:+EdgeBetween.bar e = p
Tactic:
simp only [reducedConcat, EdgeBetween.bar_bar, reverse_reverse]
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
⊢ reverse (redCons e (redCons (EdgeBetween.bar e) (reverse p))) = p
Theorem: Graph.reducedConcat_cancel_pair
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
⊢ reverse (redCons e (redCons (EdgeBetween.bar e) (reverse p))) = p
Tactic:
let lm :
  redCons e.bar.bar (redCons (EdgeBetween.bar e) (reverse p))
    = reverse p :=
  by
    apply cancelling_steps_redCons
    assumption
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
lm : redCons (EdgeBetween.bar (EdgeBetween.bar e)) (redCons (EdgeBetween.bar e) (reverse p)) = reverse p :=
  cancelling_steps_redCons (EdgeBetween.bar e) (reverse p) hyp'
⊢ reverse (redCons e (redCons (EdgeBetween.bar e) (reverse p))) = p
Theorem: Graph.reducedConcat_cancel_pair
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
lm : redCons (EdgeBetween.bar (EdgeBetween.bar e)) (redCons (EdgeBetween.bar e) (reverse p)) = reverse p :=
  cancelling_steps_redCons (EdgeBetween.bar e) (reverse p) hyp'
⊢ reverse (redCons e (redCons (EdgeBetween.bar e) (reverse p))) = p
Tactic:
simp at lm
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
lm : redCons e (redCons (EdgeBetween.bar e) (reverse p)) = reverse p
⊢ reverse (redCons e (redCons (EdgeBetween.bar e) (reverse p))) = p
Theorem: Graph.reducedConcat_cancel_pair
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
lm : redCons e (redCons (EdgeBetween.bar e) (reverse p)) = reverse p
⊢ reverse (redCons e (redCons (EdgeBetween.bar e) (reverse p))) = p
Tactic:
rw [lm, reverse_reverse]
Proof state after:
no goals
Theorem: Graph.reducedConcat_cancel_pair
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
⊢ redCons (EdgeBetween.bar (EdgeBetween.bar e)) (redCons (EdgeBetween.bar e) (reverse p)) = reverse p
Tactic:
apply cancelling_steps_redCons
Proof state after:
case hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
⊢ reduced (reverse p)
Theorem: Graph.reducedConcat_cancel_pair
Proof state before:
case hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
⊢ reduced (reverse p)
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.concat_parity
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
⊢ Even (List.length (toList (p:+e))) ↔ ¬Even (List.length (toList p))
Tactic:
simp  [reducedConcat, reverse_toList]
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
⊢ Even (List.length (toList (redCons (EdgeBetween.bar e) (reverse p)))) ↔ ¬Even (List.length (toList p))
Theorem: Graph.concat_parity
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
⊢ Even (List.length (toList (redCons (EdgeBetween.bar e) (reverse p)))) ↔ ¬Even (List.length (toList p))
Tactic:
rw [redCons_parity_neq e.bar (reverse p)]
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
⊢ ¬Even (List.length (toList (reverse p))) ↔ ¬Even (List.length (toList p))
Theorem: Graph.concat_parity
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
⊢ ¬Even (List.length (toList (reverse p))) ↔ ¬Even (List.length (toList p))
Tactic:
simp [reverse_toList]
Proof state after:
no goals
Theorem: Graph.toList_cast_init
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v v' w : V
p : EdgePath G v w
eqn : v = v'
⊢ toList p = toList (eqn ▸ p)
Tactic:
cases eqn
Proof state after:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w : V
p : EdgePath G v w
⊢ toList p = toList ((_ : v = v) ▸ p)
Theorem: Graph.toList_cast_init
Proof state before:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w : V
p : EdgePath G v w
⊢ toList p = toList ((_ : v = v) ▸ p)
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.toList_cast_terminal
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w w' : V
p : EdgePath G v w
eqn : w = w'
⊢ toList p = toList (eqn ▸ p)
Tactic:
cases eqn
Proof state after:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w : V
p : EdgePath G v w
⊢ toList p = toList ((_ : w = w) ▸ p)
Theorem: Graph.toList_cast_terminal
Proof state before:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w : V
p : EdgePath G v w
⊢ toList p = toList ((_ : w = w) ▸ p)
Tactic:
rfl
Proof state after:
no goals
Theorem: coe_eq
Proof state before:
t : CantorTree
⊢ Coe.coe (Coe.coe t) = t
Tactic:
sorry
Proof state after:
no goals
Theorem: coe_eq'
Proof state before:
t : CantorTree'
⊢ Coe.coe (Coe.coe t) = t
Tactic:
sorry
Proof state after:
no goals
Theorem: evilFn_is_evil
Proof state before:
⊢ evilFn (Coe.coe (CantorTree.node evilFn)) = !evilFn (Coe.coe (CantorTree.node evilFn))
Tactic:
conv => 
  lhs
  rw [evilFn, coe_eq]
Proof state after:
no goals
Theorem: cantor_diagonal
Proof state before:
α : Type
f : α → α → Bool
⊢ ∃ t, ∀ (a : α), t ≠ f a
Tactic:
use (fun a ↦ !(f a a) )
Proof state after:
case h
α : Type
f : α → α → Bool
⊢ ∀ (a : α), (fun a => !f a a) ≠ f a