internlm/Lean-Github huggingface dataset:
Theorem: Graph.cancelling_steps_redCons
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
hyp : reduced p
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
⊢ redCons (EdgeBetween.bar e) (redCons e p) = 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
hyp : reduced p
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
⊢ redCons (EdgeBetween.bar e) t = cons (EdgeBetween.bar e) t
Theorem: Graph.cancelling_steps_redCons
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
hyp : reduced p
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
⊢ redCons (EdgeBetween.bar e) t = cons (EdgeBetween.bar e) t
Tactic:
cases prepend_cases e.bar t with
| inl h' =>
  assumption
| inr h' =>
  let ⟨t', h₁', h₂'⟩ := h'
  rw [h₂', h₁']
  rw [h₁, h₁'] at hyp
  simp [bar_bar] at *
  have split :
            cons e.bar (cons e t') =
              (nil v : EdgePath G v v) ++
                cons e.bar (cons e.bar.bar t') := by
              simp [nil_append]
  have :¬ reduced (cons e.bar (cons e t')) := by
    apply not_reduced_of_split split
  contradiction
Proof state after:
no goals
Theorem: Graph.cancelling_steps_redCons
Proof state before:
case inr.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
hyp : reduced p
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
h' : redCons (EdgeBetween.bar e) t = cons (EdgeBetween.bar e) t
⊢ redCons (EdgeBetween.bar e) t = cons (EdgeBetween.bar e) t
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.cancelling_steps_redCons
Proof state before:
case inr.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
hyp : reduced p
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
h' : ∃ t_1, t = cons (EdgeBetween.bar (EdgeBetween.bar e)) t_1 ∧ redCons (EdgeBetween.bar e) t = t_1
⊢ redCons (EdgeBetween.bar e) t = cons (EdgeBetween.bar e) t
Tactic:
let ⟨t', h₁', h₂'⟩ := h'
Proof state after:
case inr.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
hyp : reduced p
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
h' : ∃ t_1, t = cons (EdgeBetween.bar (EdgeBetween.bar e)) t_1 ∧ redCons (EdgeBetween.bar e) t = t_1
t' : EdgePath G v w
h₁' : t = cons (EdgeBetween.bar (EdgeBetween.bar e)) t'
h₂' : redCons (EdgeBetween.bar e) t = t'
⊢ redCons (EdgeBetween.bar e) t = cons (EdgeBetween.bar e) t
Theorem: Graph.cancelling_steps_redCons
Proof state before:
case inr.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
hyp : reduced p
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
h' : ∃ t_1, t = cons (EdgeBetween.bar (EdgeBetween.bar e)) t_1 ∧ redCons (EdgeBetween.bar e) t = t_1
t' : EdgePath G v w
h₁' : t = cons (EdgeBetween.bar (EdgeBetween.bar e)) t'
h₂' : redCons (EdgeBetween.bar e) t = t'
⊢ redCons (EdgeBetween.bar e) t = cons (EdgeBetween.bar e) t
Tactic:
rw [h₂', h₁']
Proof state after:
case inr.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
hyp : reduced p
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
h' : ∃ t_1, t = cons (EdgeBetween.bar (EdgeBetween.bar e)) t_1 ∧ redCons (EdgeBetween.bar e) t = t_1
t' : EdgePath G v w
h₁' : t = cons (EdgeBetween.bar (EdgeBetween.bar e)) t'
h₂' : redCons (EdgeBetween.bar e) t = t'
⊢ t' = cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) t')
Theorem: Graph.cancelling_steps_redCons
Proof state before:
case inr.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
hyp : reduced p
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
h' : ∃ t_1, t = cons (EdgeBetween.bar (EdgeBetween.bar e)) t_1 ∧ redCons (EdgeBetween.bar e) t = t_1
t' : EdgePath G v w
h₁' : t = cons (EdgeBetween.bar (EdgeBetween.bar e)) t'
h₂' : redCons (EdgeBetween.bar e) t = t'
⊢ t' = cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) t')
Tactic:
rw [h₁, h₁'] at hyp
Proof state after:
case inr.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
h' : ∃ t_1, t = cons (EdgeBetween.bar (EdgeBetween.bar e)) t_1 ∧ redCons (EdgeBetween.bar e) t = t_1
t' : EdgePath G v w
hyp : reduced (cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) t'))
h₁' : t = cons (EdgeBetween.bar (EdgeBetween.bar e)) t'
h₂' : redCons (EdgeBetween.bar e) t = t'
⊢ t' = cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) t')
Theorem: Graph.cancelling_steps_redCons
Proof state before:
case inr.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
h' : ∃ t_1, t = cons (EdgeBetween.bar (EdgeBetween.bar e)) t_1 ∧ redCons (EdgeBetween.bar e) t = t_1
t' : EdgePath G v w
hyp : reduced (cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) t'))
h₁' : t = cons (EdgeBetween.bar (EdgeBetween.bar e)) t'
h₂' : redCons (EdgeBetween.bar e) t = t'
⊢ t' = cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) t')
Tactic:
simp [bar_bar] at *
Proof state after:
case inr.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
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
t' : EdgePath G v w
h₂' : redCons (EdgeBetween.bar e) t = t'
h : p = cons (EdgeBetween.bar e) (redCons e p)
h' : t = cons e (redCons (EdgeBetween.bar e) t)
hyp : reduced (cons (EdgeBetween.bar e) (cons e t'))
h₁' : t = cons e t'
⊢ t' = cons (EdgeBetween.bar e) (cons e t')
Theorem: Graph.cancelling_steps_redCons
Proof state before:
case inr.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
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
t' : EdgePath G v w
h₂' : redCons (EdgeBetween.bar e) t = t'
h : p = cons (EdgeBetween.bar e) (redCons e p)
h' : t = cons e (redCons (EdgeBetween.bar e) t)
hyp : reduced (cons (EdgeBetween.bar e) (cons e t'))
h₁' : t = cons e t'
⊢ t' = cons (EdgeBetween.bar e) (cons e t')
Tactic:
have split :
          cons e.bar (cons e t') =
            (nil v : EdgePath G v v) ++
              cons e.bar (cons e.bar.bar t') := by
            simp [nil_append]
Proof state after:
case inr.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
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
t' : EdgePath G v w
h₂' : redCons (EdgeBetween.bar e) t = t'
h : p = cons (EdgeBetween.bar e) (redCons e p)
h' : t = cons e (redCons (EdgeBetween.bar e) t)
hyp : reduced (cons (EdgeBetween.bar e) (cons e t'))
h₁' : t = cons e t'
split :
  cons (EdgeBetween.bar e) (cons e t') =
    nil v ++ cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) t')
⊢ t' = cons (EdgeBetween.bar e) (cons e t')
Theorem: Graph.cancelling_steps_redCons
Proof state before:
case inr.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
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
t' : EdgePath G v w
h₂' : redCons (EdgeBetween.bar e) t = t'
h : p = cons (EdgeBetween.bar e) (redCons e p)
h' : t = cons e (redCons (EdgeBetween.bar e) t)
hyp : reduced (cons (EdgeBetween.bar e) (cons e t'))
h₁' : t = cons e t'
split :
  cons (EdgeBetween.bar e) (cons e t') =
    nil v ++ cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) t')
⊢ t' = cons (EdgeBetween.bar e) (cons e t')
Tactic:
have :¬ reduced (cons e.bar (cons e t')) := by
  apply not_reduced_of_split split
Proof state after:
case inr.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
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
t' : EdgePath G v w
h₂' : redCons (EdgeBetween.bar e) t = t'
h : p = cons (EdgeBetween.bar e) (redCons e p)
h' : t = cons e (redCons (EdgeBetween.bar e) t)
hyp : reduced (cons (EdgeBetween.bar e) (cons e t'))
h₁' : t = cons e t'
split :
  cons (EdgeBetween.bar e) (cons e t') =
    nil v ++ cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) t')
this : ¬reduced (cons (EdgeBetween.bar e) (cons e t'))
⊢ t' = cons (EdgeBetween.bar e) (cons e t')
Theorem: Graph.cancelling_steps_redCons
Proof state before:
case inr.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
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
t' : EdgePath G v w
h₂' : redCons (EdgeBetween.bar e) t = t'
h : p = cons (EdgeBetween.bar e) (redCons e p)
h' : t = cons e (redCons (EdgeBetween.bar e) t)
hyp : reduced (cons (EdgeBetween.bar e) (cons e t'))
h₁' : t = cons e t'
split :
  cons (EdgeBetween.bar e) (cons e t') =
    nil v ++ cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) t')
this : ¬reduced (cons (EdgeBetween.bar e) (cons e t'))
⊢ t' = cons (EdgeBetween.bar e) (cons e t')
Tactic:
contradiction
Proof state after:
no goals
Theorem: Graph.cancelling_steps_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
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
t' : EdgePath G v w
h₂' : redCons (EdgeBetween.bar e) t = t'
h : p = cons (EdgeBetween.bar e) (redCons e p)
h' : t = cons e (redCons (EdgeBetween.bar e) t)
hyp : reduced (cons (EdgeBetween.bar e) (cons e t'))
h₁' : t = cons e t'
⊢ cons (EdgeBetween.bar e) (cons e t') =
    nil v ++ cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) t')
Tactic:
simp [nil_append]
Proof state after:
no goals
Theorem: Graph.cancelling_steps_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
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
t' : EdgePath G v w
h₂' : redCons (EdgeBetween.bar e) t = t'
h : p = cons (EdgeBetween.bar e) (redCons e p)
h' : t = cons e (redCons (EdgeBetween.bar e) t)
hyp : reduced (cons (EdgeBetween.bar e) (cons e t'))
h₁' : t = cons e t'
split :
  cons (EdgeBetween.bar e) (cons e t') =
    nil v ++ cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) t')
⊢ ¬reduced (cons (EdgeBetween.bar e) (cons e t'))
Tactic:
apply not_reduced_of_split split
Proof state after:
no goals
Theorem: Graph.redCons_eq_cons_of_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 u v
p : EdgePath G v w
hyp : reduced (cons e p)
⊢ redCons e p = cons e p
Tactic:
cases prepend_cases e p with
| inl h =>
    rw [h]
| inr h =>
    let ⟨t, h₁, h₂⟩ := h
    rw [h₁] at hyp
    have split :
      cons e (cons e.bar t) =
        (nil u : EdgePath G u u) ++
          cons e (cons e.bar t) := by
        simp [nil_append]
    have :¬ reduced (cons e (cons e.bar t)) := by
            apply not_reduced_of_split split
    contradiction
Proof state after:
no goals
Theorem: Graph.redCons_eq_cons_of_reduced
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
hyp : reduced (cons e p)
h : redCons e p = cons e p
⊢ redCons e p = cons e p
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Graph.redCons_eq_cons_of_reduced
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
hyp : reduced (cons e p)
h : ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
⊢ redCons e p = cons e 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
hyp : reduced (cons e p)
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
⊢ redCons e p = cons e p
Theorem: Graph.redCons_eq_cons_of_reduced
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
hyp : reduced (cons e p)
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
⊢ redCons e p = cons e p
Tactic:
rw [h₁] at hyp
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
hyp : reduced (cons e (cons (EdgeBetween.bar e) t))
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
⊢ redCons e p = cons e p
Theorem: Graph.redCons_eq_cons_of_reduced
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
hyp : reduced (cons e (cons (EdgeBetween.bar e) t))
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
⊢ redCons e p = cons e p
Tactic:
have split :
  cons e (cons e.bar t) =
    (nil u : EdgePath G u u) ++
      cons e (cons e.bar t) := by
    simp [nil_append]
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
hyp : reduced (cons e (cons (EdgeBetween.bar e) t))
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
split : cons e (cons (EdgeBetween.bar e) t) = nil u ++ cons e (cons (EdgeBetween.bar e) t)
⊢ redCons e p = cons e p
Theorem: Graph.redCons_eq_cons_of_reduced
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
hyp : reduced (cons e (cons (EdgeBetween.bar e) t))
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
split : cons e (cons (EdgeBetween.bar e) t) = nil u ++ cons e (cons (EdgeBetween.bar e) t)
⊢ redCons e p = cons e p
Tactic:
have :¬ reduced (cons e (cons e.bar t)) := by
        apply not_reduced_of_split split
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
hyp : reduced (cons e (cons (EdgeBetween.bar e) t))
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
split : cons e (cons (EdgeBetween.bar e) t) = nil u ++ cons e (cons (EdgeBetween.bar e) t)
this : ¬reduced (cons e (cons (EdgeBetween.bar e) t))
⊢ redCons e p = cons e p
Theorem: Graph.redCons_eq_cons_of_reduced
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
hyp : reduced (cons e (cons (EdgeBetween.bar e) t))
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
split : cons e (cons (EdgeBetween.bar e) t) = nil u ++ cons e (cons (EdgeBetween.bar e) t)
this : ¬reduced (cons e (cons (EdgeBetween.bar e) t))
⊢ redCons e p = cons e p
Tactic:
contradiction
Proof state after:
no goals
Theorem: Graph.redCons_eq_cons_of_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 u v
p : EdgePath G v w
h : ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
t : EdgePath G u w
hyp : reduced (cons e (cons (EdgeBetween.bar e) t))
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.redCons_eq_cons_of_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 u v
p : EdgePath G v w
h : ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
t : EdgePath G u w
hyp : reduced (cons e (cons (EdgeBetween.bar e) t))
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
split : cons e (cons (EdgeBetween.bar e) t) = nil u ++ cons e (cons (EdgeBetween.bar e) t)
⊢ ¬reduced (cons e (cons (EdgeBetween.bar e) t))
Tactic:
apply not_reduced_of_split split
Proof state after:
no goals
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
⊢ [[cons e p]] = [[redCons e p]]
Tactic:
cases prepend_cases e p with
| inl h =>
    rw [h]
| inr h =>
    let ⟨t, h₁, h₂⟩ := h
    rw [h₂, h₁]
    apply Quot.sound
    have split :
      cons e (cons e.bar t) =
        (nil u : EdgePath G u u) ++
          cons e (cons e.bar t) := by
        simp [nil_append]
    rw [split]
    apply Reduction.step
Proof state after:
no goals
Theorem: Graph.cons_homotopic_redCons
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
⊢ [[cons e p]] = [[redCons e p]]
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Graph.cons_homotopic_redCons
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
⊢ [[cons e p]] = [[redCons e 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
⊢ [[cons e p]] = [[redCons e p]]
Theorem: Graph.cons_homotopic_redCons
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
⊢ [[cons e p]] = [[redCons e 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
⊢ [[cons e (cons (EdgeBetween.bar e) t)]] = [[t]]
Theorem: Graph.cons_homotopic_redCons
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
⊢ [[cons e (cons (EdgeBetween.bar e) t)]] = [[t]]
Tactic:
apply Quot.sound
Proof state after:
case inr.a
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
⊢ Reduction (cons e (cons (EdgeBetween.bar e) t)) t
Theorem: Graph.cons_homotopic_redCons
Proof state before:
case inr.a
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
⊢ Reduction (cons e (cons (EdgeBetween.bar e) t)) t
Tactic:
have split :
  cons e (cons e.bar t) =
    (nil u : EdgePath G u u) ++
      cons e (cons e.bar t) := by
    simp [nil_append]
Proof state after:
case inr.a
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
split : cons e (cons (EdgeBetween.bar e) t) = nil u ++ cons e (cons (EdgeBetween.bar e) t)
⊢ Reduction (cons e (cons (EdgeBetween.bar e) t)) t
Theorem: Graph.cons_homotopic_redCons
Proof state before:
case inr.a
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
split : cons e (cons (EdgeBetween.bar e) t) = nil u ++ cons e (cons (EdgeBetween.bar e) t)
⊢ Reduction (cons e (cons (EdgeBetween.bar e) t)) t
Tactic:
rw [split]
Proof state after:
case inr.a
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
split : cons e (cons (EdgeBetween.bar e) t) = nil u ++ cons e (cons (EdgeBetween.bar e) t)
⊢ Reduction (nil u ++ cons e (cons (EdgeBetween.bar e) t)) t
Theorem: Graph.cons_homotopic_redCons
Proof state before:
case inr.a
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
split : cons e (cons (EdgeBetween.bar e) t) = nil u ++ cons e (cons (EdgeBetween.bar e) t)
⊢ Reduction (nil u ++ cons e (cons (EdgeBetween.bar e) t)) t
Tactic:
apply Reduction.step
Proof state after:
no goals