internlm/Lean-Github huggingface dataset:
Theorem: Graph.tail_reduced
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✝
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
red : reduced (cons e p)
p' : EdgePath G v w
red' : Reduction p p'
⊢ False
Tactic:
let ⟨u, u', e', p₁, p₂, eqn⟩   := red'.property
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✝
u✝ v w : V
e : EdgeBetween G u✝ v
p : EdgePath G v w
red : reduced (cons e p)
p' : EdgePath G v w
red' : Reduction p p'
u u' : V
e' : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p
⊢ False
Theorem: Graph.tail_reduced
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✝
u✝ v w : V
e : EdgeBetween G u✝ v
p : EdgePath G v w
red : reduced (cons e p)
p' : EdgePath G v w
red' : Reduction p p'
u u' : V
e' : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p
⊢ False
Tactic:
let eqn' : (cons e p₁) ++ cons e' (cons e'.bar p₂) = 
  cons e p := by
    simp [cons_append]
    exact eqn
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✝
u✝ v w : V
e : EdgeBetween G u✝ v
p : EdgePath G v w
red : reduced (cons e p)
p' : EdgePath G v w
red' : Reduction p p'
u u' : V
e' : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p
eqn' : cons e p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = cons e p :=
  Eq.mpr
    (id
      ((cons.injEq e (p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂)) v e p).trans
        ((congr (congrArg And (eq_self v))
              ((congr (congrArg And ((heq_eq_eq e e).trans (eq_self e)))
                    (heq_eq_eq (p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂)) p)).trans
                (true_and (p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p)))).trans
          (true_and (p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p)))))
    eqn
⊢ False
Theorem: Graph.tail_reduced
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✝
u✝ v w : V
e : EdgeBetween G u✝ v
p : EdgePath G v w
red : reduced (cons e p)
p' : EdgePath G v w
red' : Reduction p p'
u u' : V
e' : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p
eqn' : cons e p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = cons e p :=
  Eq.mpr
    (id
      ((cons.injEq e (p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂)) v e p).trans
        ((congr (congrArg And (eq_self v))
              ((congr (congrArg And ((heq_eq_eq e e).trans (eq_self e)))
                    (heq_eq_eq (p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂)) p)).trans
                (true_and (p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p)))).trans
          (true_and (p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p)))))
    eqn
⊢ False
Tactic:
let h' := not_reduced_of_split (Eq.symm eqn')
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✝
u✝ v w : V
e : EdgeBetween G u✝ v
p : EdgePath G v w
red : reduced (cons e p)
p' : EdgePath G v w
red' : Reduction p p'
u u' : V
e' : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p
eqn' : cons e p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = cons e p :=
  Eq.mpr
    (id
      ((cons.injEq e (p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂)) v e p).trans
        ((congr (congrArg And (eq_self v))
              ((congr (congrArg And ((heq_eq_eq e e).trans (eq_self e)))
                    (heq_eq_eq (p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂)) p)).trans
                (true_and (p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p)))).trans
          (true_and (p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p)))))
    eqn
h' : ¬reduced (cons e p) := not_reduced_of_split eqn'.symm
⊢ False
Theorem: Graph.tail_reduced
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✝
u✝ v w : V
e : EdgeBetween G u✝ v
p : EdgePath G v w
red : reduced (cons e p)
p' : EdgePath G v w
red' : Reduction p p'
u u' : V
e' : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p
eqn' : cons e p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = cons e p :=
  Eq.mpr
    (id
      ((cons.injEq e (p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂)) v e p).trans
        ((congr (congrArg And (eq_self v))
              ((congr (congrArg And ((heq_eq_eq e e).trans (eq_self e)))
                    (heq_eq_eq (p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂)) p)).trans
                (true_and (p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p)))).trans
          (true_and (p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p)))))
    eqn
h' : ¬reduced (cons e p) := not_reduced_of_split eqn'.symm
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Graph.tail_reduced
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✝
u✝ v w : V
e : EdgeBetween G u✝ v
p : EdgePath G v w
red : reduced (cons e p)
p' : EdgePath G v w
red' : Reduction p p'
u u' : V
e' : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p
⊢ cons e p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = cons e p
Tactic:
simp [cons_append]
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✝
u✝ v w : V
e : EdgeBetween G u✝ v
p : EdgePath G v w
red : reduced (cons e p)
p' : EdgePath G v w
red' : Reduction p p'
u u' : V
e' : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p
⊢ p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p
Theorem: Graph.tail_reduced
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✝
u✝ v w : V
e : EdgeBetween G u✝ v
p : EdgePath G v w
red : reduced (cons e p)
p' : EdgePath G v w
red' : Reduction p p'
u u' : V
e' : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p
⊢ p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p
Tactic:
exact eqn
Proof state after:
no goals
Theorem: Graph.reverse_reduced
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✝
v w : V
p : EdgePath G v w
⊢ reduced p → reduced (reverse p)
Tactic:
intro red rev_targ rev_red
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
⊢ False
Theorem: Graph.reverse_reduced
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
⊢ False
Tactic:
let ⟨u, u', e, p₁, p₂, eqn⟩   := rev_red.property
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
⊢ False
Theorem: Graph.reverse_reduced
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
⊢ False
Tactic:
apply red (reverse p₂ ++ reverse p₁)
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
⊢ Reduction p (reverse p₂ ++ reverse p₁)
Theorem: Graph.reverse_reduced
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
⊢ Reduction p (reverse p₂ ++ reverse p₁)
Tactic:
let eqn' := congrArg reverse eqn
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = reverse (reverse p) := congrArg reverse eqn
⊢ Reduction p (reverse p₂ ++ reverse p₁)
Theorem: Graph.reverse_reduced
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = reverse (reverse p) := congrArg reverse eqn
⊢ Reduction p (reverse p₂ ++ reverse p₁)
Tactic:
simp [reverse_reverse] at eqn'
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
⊢ Reduction p (reverse p₂ ++ reverse p₁)
Theorem: Graph.reverse_reduced
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
⊢ Reduction p (reverse p₂ ++ reverse p₁)
Tactic:
have eqn'' : (reverse p₂) ++ (cons e (cons e.bar (reverse p₁))) =
  p := by
    rw [←eqn', reverse_append]
    simp [reverse_cons]
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
eqn'' : reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁)) = p
⊢ Reduction p (reverse p₂ ++ reverse p₁)
Theorem: Graph.reverse_reduced
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
eqn'' : reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁)) = p
⊢ Reduction p (reverse p₂ ++ reverse p₁)
Tactic:
rw [←eqn'']
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
eqn'' : reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁)) = p
⊢ Reduction (reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁))) (reverse p₂ ++ reverse p₁)
Theorem: Graph.reverse_reduced
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
eqn'' : reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁)) = p
⊢ Reduction (reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁))) (reverse p₂ ++ reverse p₁)
Tactic:
apply Reduction.step
Proof state after:
no goals
Theorem: Graph.reverse_reduced
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
⊢ reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁)) = p
Tactic:
rw [←eqn', reverse_append]
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
⊢ reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁)) =
    reverse (cons e (cons (EdgeBetween.bar e) p₂)) ++ reverse p₁
Theorem: Graph.reverse_reduced
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
⊢ reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁)) =
    reverse (cons e (cons (EdgeBetween.bar e) p₂)) ++ reverse p₁
Tactic:
simp [reverse_cons]
Proof state after:
no goals
Theorem: Graph.reverse_reduced_iff
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✝
v w : V
p : EdgePath G v w
⊢ reduced p ↔ reduced (reverse p)
Tactic:
apply Iff.intro
Proof state after:
case mp
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 : V
p : EdgePath G v w
⊢ reduced p → reduced (reverse p)

case mpr
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 : V
p : EdgePath G v w
⊢ reduced (reverse p) → reduced p
Theorem: Graph.reverse_reduced_iff
Proof state before:
case mp
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 : V
p : EdgePath G v w
⊢ reduced p → reduced (reverse p)
Tactic:
exact reverse_reduced p
Proof state after:
no goals
Theorem: Graph.reverse_reduced_iff
Proof state before:
case mpr
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 : V
p : EdgePath G v w
⊢ reduced (reverse p) → reduced p
Tactic:
intro h
Proof state after:
case mpr
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 : V
p : EdgePath G v w
h : reduced (reverse p)
⊢ reduced p
Theorem: Graph.reverse_reduced_iff
Proof state before:
case mpr
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 : V
p : EdgePath G v w
h : reduced (reverse p)
⊢ reduced p
Tactic:
rw [← reverse_reverse p]
Proof state after:
case mpr
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 : V
p : EdgePath G v w
h : reduced (reverse p)
⊢ reduced (reverse (reverse p))
Theorem: Graph.reverse_reduced_iff
Proof state before:
case mpr
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 : V
p : EdgePath G v w
h : reduced (reverse p)
⊢ reduced (reverse (reverse p))
Tactic:
apply reverse_reduced
Proof state after:
case mpr.a
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 : V
p : EdgePath G v w
h : reduced (reverse p)
⊢ reduced (reverse p)
Theorem: Graph.reverse_reduced_iff
Proof state before:
case mpr.a
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 : V
p : EdgePath G v w
h : reduced (reverse p)
⊢ reduced (reverse p)
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.append_cons_bar_cons
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
u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
⊢ [[p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)]] = [[p₁ ++ p₂]]
Tactic:
have := Reduction.step _ _ e p₁ p₂
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
u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
this : Reduction (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (p₁ ++ p₂)
⊢ [[p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)]] = [[p₁ ++ p₂]]
Theorem: Graph.append_cons_bar_cons
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
u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
this : Reduction (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (p₁ ++ p₂)
⊢ [[p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)]] = [[p₁ ++ p₂]]
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.append_cons_cons_bar
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
u' : V
e : EdgeBetween G u' u
p₁ : EdgePath G v u
p₂ : EdgePath G u w
⊢ [[p₁ ++ cons (EdgeBetween.bar e) (cons e p₂)]] = [[p₁ ++ p₂]]
Tactic:
have := append_cons_bar_cons e.bar p₁ p₂
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
u' : V
e : EdgeBetween G u' u
p₁ : EdgePath G v u
p₂ : EdgePath G u w
this : [[p₁ ++ cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) p₂)]] = [[p₁ ++ p₂]]
⊢ [[p₁ ++ cons (EdgeBetween.bar e) (cons e p₂)]] = [[p₁ ++ p₂]]
Theorem: Graph.append_cons_cons_bar
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
u' : V
e : EdgeBetween G u' u
p₁ : EdgePath G v u
p₂ : EdgePath G u w
this : [[p₁ ++ cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) p₂)]] = [[p₁ ++ p₂]]
⊢ [[p₁ ++ cons (EdgeBetween.bar e) (cons e p₂)]] = [[p₁ ++ p₂]]
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.left_append_step
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✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
rel : Reduction b₁ b₂
⊢ [[a ++ b₁]] = [[a ++ b₂]]
Tactic:
induction rel
Proof state after:
case step
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 : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ (p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝))]] = [[a ++ (p₁✝ ++ p₂✝)]]
Theorem: Graph.left_append_step
Proof state before:
case step
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 : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ (p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝))]] = [[a ++ (p₁✝ ++ p₂✝)]]
Tactic:
repeat (rw [← append_assoc])
Proof state after:
case step
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 : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝)]] = [[a ++ p₁✝ ++ p₂✝]]
Theorem: Graph.left_append_step
Proof state before:
case step
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 : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝)]] = [[a ++ p₁✝ ++ p₂✝]]
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.left_append_step
Proof state before:
case step
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 : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝)]] = [[a ++ (p₁✝ ++ p₂✝)]]
Tactic:
(rw [← append_assoc])
Proof state after:
case step
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 : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝)]] = [[a ++ p₁✝ ++ p₂✝]]
Theorem: Graph.left_append_step
Proof state before:
case step
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 : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝)]] = [[a ++ (p₁✝ ++ p₂✝)]]
Tactic:
rw [← append_assoc]
Proof state after:
case step
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 : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝)]] = [[a ++ p₁✝ ++ p₂✝]]