internlm/Lean-Github huggingface dataset:
Theorem: Graph.PathClass.map_mul
Proof 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
Proof 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 η₂
Theorem: Graph.PathClass.map_mul
Proof 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
Proof 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 η₂
Theorem: Graph.PathClass.map_mul
Proof 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
Proof 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)
Theorem: Graph.PathClass.map_mul
Proof 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
Proof 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)
Theorem: Graph.PathClass.map_mul
Proof 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]
Proof state after:
no goals
Theorem: Graph.Morphism.localSection_toFuncE
Proof state before:
V : Type u
E : Type v
V₁ : Type ?u.89747
E₁ : Type ?u.89746
V₂ : Type ?u.89751
E₂ : Type ?u.89750
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
e₁ : E₁
h : v₁ = G₁.ι e₁
⊢ p.toFuncV v₁ = G₂.ι (p.toFuncE e₁)
Tactic:
rw [← p.toFuncV_init, h]
Proof state after:
no goals
Theorem: Graph.lifts_homotopic
Proof 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
Proof 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₂
Theorem: Graph.lifts_homotopic
Proof 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
Proof 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₂
Theorem: Graph.lifts_homotopic
Proof 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]
Proof 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₂
Theorem: Graph.lifts_homotopic
Proof 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
Proof 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₂
Theorem: Graph.lifts_homotopic
Proof 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
Proof 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₂
Theorem: Graph.lifts_homotopic
Proof 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
Proof 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₂ = []
Theorem: Graph.lifts_homotopic
Proof 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
Proof state after:
no goals
Theorem: Graph.lifts_homotopic
Proof 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 *
Proof 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₁') = []
Theorem: Graph.lifts_homotopic
Proof 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
Proof state after:
no goals
Theorem: Graph.lifts_homotopic
Proof 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 *
Proof 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₂'
Theorem: Graph.lifts_homotopic
Proof 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
Proof 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₂'
Theorem: Graph.lifts_homotopic
Proof 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
Proof 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₂'
Theorem: Graph.lifts_homotopic
Proof 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]
Proof 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₂'
Theorem: Graph.lifts_homotopic
Proof 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₂'
Proof 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₂')
Theorem: Graph.lifts_homotopic
Proof 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)
Proof 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
Theorem: Graph.lifts_homotopic
Proof 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)
Proof 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
Theorem: Graph.lifts_homotopic
Proof 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₂]
Proof 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))
Theorem: Graph.lifts_homotopic
Proof 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
Proof state after:
no goals