Theorem: Graph.concat_equiv_of_equiv (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✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
⊢ [[a₁]] = [[a₂]] → [[concat a₁ b]] = [[concat a₂ b]]
Tactic:
intro r
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✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
⊢ [[concat a₁ b]] = [[concat a₂ b]]

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✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
⊢ [[concat a₁ b]] = [[concat a₂ b]]
Tactic:
have: concat a₁  b = a₁ ++ (concat (nil _) b) := by 
  rw [append_concat, append_nil]
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✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
this : concat a₁ b = a₁ ++ concat (nil w) b
⊢ [[concat a₁ b]] = [[concat a₂ b]]

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✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
this : concat a₁ b = a₁ ++ concat (nil w) b
⊢ [[concat a₁ b]] = [[concat a₂ b]]
Tactic:
rw [this]
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✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
this : concat a₁ b = a₁ ++ concat (nil w) b
⊢ [[a₁ ++ concat (nil w) b]] = [[concat a₂ b]]

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✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
this : concat a₁ b = a₁ ++ concat (nil w) b
⊢ [[a₁ ++ concat (nil w) b]] = [[concat a₂ b]]
Tactic:
have: concat a₂  b = a₂ ++ (concat (nil _) b) := by 
  rw [append_concat, append_nil]
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✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
this✝ : concat a₁ b = a₁ ++ concat (nil w) b
this : concat a₂ b = a₂ ++ concat (nil w) b
⊢ [[a₁ ++ concat (nil w) b]] = [[concat a₂ b]]

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✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
this✝ : concat a₁ b = a₁ ++ concat (nil w) b
this : concat a₂ b = a₂ ++ concat (nil w) b
⊢ [[a₁ ++ concat (nil w) b]] = [[concat a₂ b]]
Tactic:
rw [this, ← mul_path_path, ← mul_path_path, r]
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✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
⊢ concat a₁ b = a₁ ++ concat (nil w) b
Tactic:
rw [append_concat, append_nil]
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✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
r : [[a₁]] = [[a₂]]
this : concat a₁ b = a₁ ++ concat (nil w) b
⊢ concat a₂ b = a₂ ++ concat (nil w) b
Tactic:
rw [append_concat, append_nil]
State after:
no goals