Theorem: Graph.Morphism.reduced_of_image_reduced (GroupComp/Graph/Covering.lean)

State before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η : EdgePath G₁ v w
⊢ reduced (map η f) → reduced η
Tactic:
intro hyp η' contra
State after:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η : EdgePath G₁ v w
hyp : reduced (map η f)
η' : EdgePath G₁ v w
contra : Reduction η η'
⊢ False

State before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η : EdgePath G₁ v w
hyp : reduced (map η f)
η' : EdgePath G₁ v w
contra : Reduction η η'
⊢ False
Tactic:
apply hyp (η'.map f)
State after:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η : EdgePath G₁ v w
hyp : reduced (map η f)
η' : EdgePath G₁ v w
contra : Reduction η η'
⊢ Reduction (map η f) (map η' f)

State before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η : EdgePath G₁ v w
hyp : reduced (map η f)
η' : EdgePath G₁ v w
contra : Reduction η η'
⊢ Reduction (map η f) (map η' f)
Tactic:
apply map_of_reduction
State after:
case a
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η : EdgePath G₁ v w
hyp : reduced (map η f)
η' : EdgePath G₁ v w
contra : Reduction η η'
⊢ Reduction η η'

State before:
case a
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
v w : V₁
η : EdgePath G₁ v w
hyp : reduced (map η f)
η' : EdgePath G₁ v w
contra : Reduction η η'
⊢ Reduction η η'
Tactic:
exact contra
State after:
no goals