Theorem: Graph.PathClass.mul_assoc' (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✝
v w u u' : V
⊢ ∀ (p : v ⟶ w) (q : w ⟶ u) (r : u ⟶ u'), (p ≫ q) ≫ r = p ≫ q ≫ r
Tactic:
apply Quot.ind
State after:
case mk
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 u' : V
⊢ ∀ (a : EdgePath G v w) (q : w ⟶ u) (r : u ⟶ u'), (Quot.mk Reduction a ≫ q) ≫ r = Quot.mk Reduction a ≫ q ≫ r

State before:
case mk
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 u' : V
⊢ ∀ (a : EdgePath G v w) (q : w ⟶ u) (r : u ⟶ u'), (Quot.mk Reduction a ≫ q) ≫ r = Quot.mk Reduction a ≫ q ≫ r
Tactic:
intro a
State after:
case mk
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 u' : V
a : EdgePath G v w
⊢ ∀ (q : w ⟶ u) (r : u ⟶ u'), (Quot.mk Reduction a ≫ q) ≫ r = Quot.mk Reduction a ≫ q ≫ r

State before:
case mk
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 u' : V
a : EdgePath G v w
⊢ ∀ (q : w ⟶ u) (r : u ⟶ u'), (Quot.mk Reduction a ≫ q) ≫ r = Quot.mk Reduction a ≫ q ≫ r
Tactic:
apply Quot.ind
State after:
case mk.mk
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 u' : V
a : EdgePath G v w
⊢ ∀ (a_1 : EdgePath G w u) (r : u ⟶ u'),
    (Quot.mk Reduction a ≫ Quot.mk Reduction a_1) ≫ r = Quot.mk Reduction a ≫ Quot.mk Reduction a_1 ≫ r

State before:
case mk.mk
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 u' : V
a : EdgePath G v w
⊢ ∀ (a_1 : EdgePath G w u) (r : u ⟶ u'),
    (Quot.mk Reduction a ≫ Quot.mk Reduction a_1) ≫ r = Quot.mk Reduction a ≫ Quot.mk Reduction a_1 ≫ r
Tactic:
intro b
State after:
case mk.mk
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 u' : V
a : EdgePath G v w
b : EdgePath G w u
⊢ ∀ (r : u ⟶ u'), (Quot.mk Reduction a ≫ Quot.mk Reduction b) ≫ r = Quot.mk Reduction a ≫ Quot.mk Reduction b ≫ r

State before:
case mk.mk
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 u' : V
a : EdgePath G v w
b : EdgePath G w u
⊢ ∀ (r : u ⟶ u'), (Quot.mk Reduction a ≫ Quot.mk Reduction b) ≫ r = Quot.mk Reduction a ≫ Quot.mk Reduction b ≫ r
Tactic:
apply Quot.ind
State after:
case mk.mk.mk
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 u' : V
a : EdgePath G v w
b : EdgePath G w u
⊢ ∀ (a_1 : EdgePath G u u'),
    (Quot.mk Reduction a ≫ Quot.mk Reduction b) ≫ Quot.mk Reduction a_1 =
      Quot.mk Reduction a ≫ Quot.mk Reduction b ≫ Quot.mk Reduction a_1

State before:
case mk.mk.mk
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 u' : V
a : EdgePath G v w
b : EdgePath G w u
⊢ ∀ (a_1 : EdgePath G u u'),
    (Quot.mk Reduction a ≫ Quot.mk Reduction b) ≫ Quot.mk Reduction a_1 =
      Quot.mk Reduction a ≫ Quot.mk Reduction b ≫ Quot.mk Reduction a_1
Tactic:
intro c
State after:
case mk.mk.mk
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 u' : V
a : EdgePath G v w
b : EdgePath G w u
c : EdgePath G u u'
⊢ (Quot.mk Reduction a ≫ Quot.mk Reduction b) ≫ Quot.mk Reduction c =
    Quot.mk Reduction a ≫ Quot.mk Reduction b ≫ Quot.mk Reduction c

State before:
case mk.mk.mk
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 u' : V
a : EdgePath G v w
b : EdgePath G w u
c : EdgePath G u u'
⊢ (Quot.mk Reduction a ≫ Quot.mk Reduction b) ≫ Quot.mk Reduction c =
    Quot.mk Reduction a ≫ Quot.mk Reduction b ≫ Quot.mk Reduction c
Tactic:
simp [append_assoc]
State after:
no goals