Theorem: Graph.PathClass.mul_assoc (Lectures/Graph.lean)

State before:
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
⊢ ∀ (p : PathClass G v w) (q : PathClass G w u) (r : PathClass G u u'), mul (mul p q) r = mul p (mul q r)
Tactic:
apply Quot.ind
State after:
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
⊢ ∀ (a : EdgePath G v w) (q : PathClass G w u) (r : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) q) r = mul (Quot.mk Reduction a) (mul q r)

State before:
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
⊢ ∀ (a : EdgePath G v w) (q : PathClass G w u) (r : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) q) r = mul (Quot.mk Reduction a) (mul q r)
Tactic:
intro a
State after:
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
⊢ ∀ (q : PathClass G w u) (r : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) q) r = mul (Quot.mk Reduction a) (mul q r)

State before:
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
⊢ ∀ (q : PathClass G w u) (r : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) q) r = mul (Quot.mk Reduction a) (mul q r)
Tactic:
apply Quot.ind
State after:
case mk.mk
V : Type u
E : Type v
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 : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) (Quot.mk Reduction a_1)) r =
      mul (Quot.mk Reduction a) (mul (Quot.mk Reduction a_1) r)

State before:
case mk.mk
V : Type u
E : Type v
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 : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) (Quot.mk Reduction a_1)) r =
      mul (Quot.mk Reduction a) (mul (Quot.mk Reduction a_1) r)
Tactic:
intro b
State after:
case mk.mk
V : Type u
E : Type v
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 : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) (Quot.mk Reduction b)) r = mul (Quot.mk Reduction a) (mul (Quot.mk Reduction b) r)

State before:
case mk.mk
V : Type u
E : Type v
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 : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) (Quot.mk Reduction b)) r = mul (Quot.mk Reduction a) (mul (Quot.mk Reduction b) r)
Tactic:
apply Quot.ind
State after:
case mk.mk.mk
V : Type u
E : Type v
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'),
    mul (mul (Quot.mk Reduction a) (Quot.mk Reduction b)) (Quot.mk Reduction a_1) =
      mul (Quot.mk Reduction a) (mul (Quot.mk Reduction b) (Quot.mk Reduction a_1))

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

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