Theorem: Graph.cons_homotopic_redCons (GroupComp/Graph/ReducedPaths.lean)

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
State after:
no goals

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]
State after:
no goals

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
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]]

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₁]
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]]

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
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

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]
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

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]
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

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
State after:
no goals

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]
State after:
no goals