Theorem: Graph.lifts_homotopic (GroupComp/Graph/Covering.lean)

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁ w₁ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁ w₁
e₂ : EdgePath G₁ v₂ w₂
hv : v₁ = v₂
⊢ List.map p.toFuncE (toList e₁) = List.map p.toFuncE (toList e₂) → toList e₁ = toList e₂
Tactic:
intro hyp
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁ w₁ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁ w₁
e₂ : EdgePath G₁ v₂ w₂
hv : v₁ = v₂
hyp : List.map p.toFuncE (toList e₁) = List.map p.toFuncE (toList e₂)
⊢ toList e₁ = toList e₂

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁ w₁ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁ w₁
e₂ : EdgePath G₁ v₂ w₂
v : V₁
hv : v = v₂
hyp : List.map p.toFuncE (toList (nil v)) = List.map p.toFuncE (toList e₂)
⊢ toList (nil v) = toList e₂
Tactic:
simp [nil_toList] at hyp
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁ w₁ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁ w₁
e₂ : EdgePath G₁ v₂ w₂
v : V₁
hv : v = v₂
hyp : [] = List.map p.toFuncE (toList e₂)
⊢ toList (nil v) = toList e₂

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁ w₁ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁ w₁
e₂ : EdgePath G₁ v₂ w₂
v : V₁
hv : v = v₂
hyp : [] = List.map p.toFuncE (toList e₂)
⊢ toList (nil v) = toList e₂
Tactic:
simp [nil_toList]
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁ w₁ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁ w₁
e₂ : EdgePath G₁ v₂ w₂
v : V₁
hv : v = v₂
hyp : [] = List.map p.toFuncE (toList e₂)
⊢ [] = toList e₂

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁ w₁ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁ w₁
e₂ : EdgePath G₁ v₂ w₂
v : V₁
hv : v = v₂
hyp : [] = List.map p.toFuncE (toList e₂)
⊢ [] = toList e₂
Tactic:
symm at hyp
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁ w₁ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁ w₁
e₂ : EdgePath G₁ v₂ w₂
v : V₁
hv : v = v₂
hyp : List.map p.toFuncE (toList e₂) = []
⊢ [] = toList e₂

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁ w₁ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁ w₁
e₂ : EdgePath G₁ v₂ w₂
v : V₁
hv : v = v₂
hyp : List.map p.toFuncE (toList e₂) = []
⊢ [] = toList e₂
Tactic:
rw [List.map_eq_nil] at hyp
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁ w₁ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁ w₁
e₂ : EdgePath G₁ v₂ w₂
v : V₁
hv : v = v₂
hyp : toList e₂ = []
⊢ [] = toList e₂

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁ w₁ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁ w₁
e₂ : EdgePath G₁ v₂ w₂
v : V₁
hv : v = v₂
hyp : toList e₂ = []
⊢ [] = toList e₂
Tactic:
symm
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁ w₁ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁ w₁
e₂ : EdgePath G₁ v₂ w₂
v : V₁
hv : v = v₂
hyp : toList e₂ = []
⊢ toList e₂ = []

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁ w₁ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁ w₁
e₂ : EdgePath G₁ v₂ w₂
v : V₁
hv : v = v₂
hyp : toList e₂ = []
⊢ toList e₂ = []
Tactic:
exact hyp
State after:
no goals

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂
w₁ v₁ w✝ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝
p₁' : EdgePath G₁ w✝ w₁
hv : v₁ = v₂
v : V₁
x✝ : v₁ = v
hyp : List.map p.toFuncE (toList (cons edg₁ p₁')) = List.map p.toFuncE (toList (nil v))
⊢ toList (cons edg₁ p₁') = toList (nil v)
Tactic:
simp [nil_toList] at *
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂
w₁ v₁ w✝ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝
p₁' : EdgePath G₁ w✝ w₁
hv : v₁ = v₂
v : V₁
x✝ : v₁ = v
hyp : toList (cons edg₁ p₁') = []
⊢ toList (cons edg₁ p₁') = []

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂
w₁ v₁ w✝ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝
p₁' : EdgePath G₁ w✝ w₁
hv : v₁ = v₂
v : V₁
x✝ : v₁ = v
hyp : toList (cons edg₁ p₁') = []
⊢ toList (cons edg₁ p₁') = []
Tactic:
assumption
State after:
no goals

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : List.map p.toFuncE (toList (cons edg₁ p₁')) = List.map p.toFuncE (toList (cons edg₂ p₂'))
⊢ toList (cons edg₁ p₁') = toList (cons edg₂ p₂')
Tactic:
simp [cons_toList] at *
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
⊢ edg₁.edge = edg₂.edge ∧ toList p₁' = toList p₂'

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
⊢ edg₁.edge = edg₂.edge ∧ toList p₁' = toList p₂'
Tactic:
let ⟨h₁, h₂⟩ := hyp
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
⊢ edg₁.edge = edg₂.edge ∧ toList p₁' = toList p₂'

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
⊢ edg₁.edge = edg₂.edge ∧ toList p₁' = toList p₂'
Tactic:
have edg_eq : edg₁.edge = edg₂.edge := by
  let eq₁ := p.localSection_toFuncE v₁ edg₁.edge (Eq.symm edg₁.init_eq)
  let eq₂ := p.localSection_toFuncE v₁ edg₂.edge (Eq.symm edg₂.init_eq)
  rw [← eq₁, ← eq₂]
  congr
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
edg_eq : edg₁.edge = edg₂.edge
⊢ edg₁.edge = edg₂.edge ∧ toList p₁' = toList p₂'

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
edg_eq : edg₁.edge = edg₂.edge
⊢ edg₁.edge = edg₂.edge ∧ toList p₁' = toList p₂'
Tactic:
simp [edg_eq]
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
edg_eq : edg₁.edge = edg₂.edge
⊢ toList p₁' = toList p₂'

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
edg_eq : edg₁.edge = edg₂.edge
⊢ toList p₁' = toList p₂'
Tactic:
apply lifts_homotopic p p₁' p₂'
State after:
case hv
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
edg_eq : edg₁.edge = edg₂.edge
⊢ w✝¹ = w✝

case a
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
edg_eq : edg₁.edge = edg₂.edge
⊢ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
⊢ edg₁.edge = edg₂.edge
Tactic:
let eq₁ := p.localSection_toFuncE v₁ edg₁.edge (Eq.symm edg₁.init_eq)
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
eq₁ : Morphism.localSection p v₁ (p.toFuncE edg₁.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₁.edge)) = edg₁.edge :=
  Morphism.localSection_toFuncE p v₁ edg₁.edge edg₁.init_eq.symm
⊢ edg₁.edge = edg₂.edge

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
eq₁ : Morphism.localSection p v₁ (p.toFuncE edg₁.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₁.edge)) = edg₁.edge :=
  Morphism.localSection_toFuncE p v₁ edg₁.edge edg₁.init_eq.symm
⊢ edg₁.edge = edg₂.edge
Tactic:
let eq₂ := p.localSection_toFuncE v₁ edg₂.edge (Eq.symm edg₂.init_eq)
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
eq₁ : Morphism.localSection p v₁ (p.toFuncE edg₁.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₁.edge)) = edg₁.edge :=
  Morphism.localSection_toFuncE p v₁ edg₁.edge edg₁.init_eq.symm
eq₂ : Morphism.localSection p v₁ (p.toFuncE edg₂.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₂.edge)) = edg₂.edge :=
  Morphism.localSection_toFuncE p v₁ edg₂.edge edg₂.init_eq.symm
⊢ edg₁.edge = edg₂.edge

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
eq₁ : Morphism.localSection p v₁ (p.toFuncE edg₁.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₁.edge)) = edg₁.edge :=
  Morphism.localSection_toFuncE p v₁ edg₁.edge edg₁.init_eq.symm
eq₂ : Morphism.localSection p v₁ (p.toFuncE edg₂.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₂.edge)) = edg₂.edge :=
  Morphism.localSection_toFuncE p v₁ edg₂.edge edg₂.init_eq.symm
⊢ edg₁.edge = edg₂.edge
Tactic:
rw [← eq₁, ← eq₂]
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
eq₁ : Morphism.localSection p v₁ (p.toFuncE edg₁.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₁.edge)) = edg₁.edge :=
  Morphism.localSection_toFuncE p v₁ edg₁.edge edg₁.init_eq.symm
eq₂ : Morphism.localSection p v₁ (p.toFuncE edg₂.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₂.edge)) = edg₂.edge :=
  Morphism.localSection_toFuncE p v₁ edg₂.edge edg₂.init_eq.symm
⊢ Morphism.localSection p v₁ (p.toFuncE edg₁.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₁.edge)) =
    Morphism.localSection p v₁ (p.toFuncE edg₂.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₂.edge))

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
eq₁ : Morphism.localSection p v₁ (p.toFuncE edg₁.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₁.edge)) = edg₁.edge :=
  Morphism.localSection_toFuncE p v₁ edg₁.edge edg₁.init_eq.symm
eq₂ : Morphism.localSection p v₁ (p.toFuncE edg₂.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₂.edge)) = edg₂.edge :=
  Morphism.localSection_toFuncE p v₁ edg₂.edge edg₂.init_eq.symm
⊢ Morphism.localSection p v₁ (p.toFuncE edg₁.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₁.edge)) =
    Morphism.localSection p v₁ (p.toFuncE edg₂.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₂.edge))
Tactic:
congr
State after:
no goals

State before:
case hv
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
edg_eq : edg₁.edge = edg₂.edge
⊢ w✝¹ = w✝
Tactic:
rw [← edg₁.term_eq, ← edg₂.term_eq, edg_eq]
State after:
no goals

State before:
case a
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
edg_eq : edg₁.edge = edg₂.edge
⊢ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
Tactic:
exact h₂
State after:
no goals