Theorem: Graph.tail_reduced (GroupComp/Graph.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 v✝ w✝
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
⊢ reduced (cons e p) → reduced p
Tactic:
intro red p' red'
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'
⊢ False

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

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

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

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

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