Theorem: Graph.PathClass.map_mul (GroupComp/Graph/Covering.lean)

State before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w u : V₁
⊢ ∀ (η₁ : PathClass G₁ v w) (η₂ : PathClass G₁ w u), map f (η₁ * η₂) = map f η₁ * map f η₂
Tactic:
apply Quot.ind
State after:
case mk
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w u : V₁
⊢ ∀ (a : EdgePath G₁ v w) (η₂ : PathClass G₁ w u),
    map f (Quot.mk Reduction a * η₂) = map f (Quot.mk Reduction a) * map f η₂

State before:
case mk
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w u : V₁
⊢ ∀ (a : EdgePath G₁ v w) (η₂ : PathClass G₁ w u),
    map f (Quot.mk Reduction a * η₂) = map f (Quot.mk Reduction a) * map f η₂
Tactic:
intro a
State after:
case mk
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w u : V₁
a : EdgePath G₁ v w
⊢ ∀ (η₂ : PathClass G₁ w u), map f (Quot.mk Reduction a * η₂) = map f (Quot.mk Reduction a) * map f η₂

State before:
case mk
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w u : V₁
a : EdgePath G₁ v w
⊢ ∀ (η₂ : PathClass G₁ w u), map f (Quot.mk Reduction a * η₂) = map f (Quot.mk Reduction a) * map f η₂
Tactic:
apply Quot.ind
State after:
case mk.mk
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w u : V₁
a : EdgePath G₁ v w
⊢ ∀ (a_1 : EdgePath G₁ w u),
    map f (Quot.mk Reduction a * Quot.mk Reduction a_1) = map f (Quot.mk Reduction a) * map f (Quot.mk Reduction a_1)

State before:
case mk.mk
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w u : V₁
a : EdgePath G₁ v w
⊢ ∀ (a_1 : EdgePath G₁ w u),
    map f (Quot.mk Reduction a * Quot.mk Reduction a_1) = map f (Quot.mk Reduction a) * map f (Quot.mk Reduction a_1)
Tactic:
intro b
State after:
case mk.mk
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w u : V₁
a : EdgePath G₁ v w
b : EdgePath G₁ w u
⊢ map f (Quot.mk Reduction a * Quot.mk Reduction b) = map f (Quot.mk Reduction a) * map f (Quot.mk Reduction b)

State before:
case mk.mk
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w u : V₁
a : EdgePath G₁ v w
b : EdgePath G₁ w u
⊢ map f (Quot.mk Reduction a * Quot.mk Reduction b) = map f (Quot.mk Reduction a) * map f (Quot.mk Reduction b)
Tactic:
simp only [mul_path_path, map_on_quotient, Morphism.append_map]
State after:
no goals