Theorem: Graph.UniversalCover.homotopic_iff_reduction_eq (GroupComp/Graph/UniversalCover.lean)

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
⊢ [[p₁]] = [[p₂]] ↔ reduction p₁ = reduction p₂
Tactic:
apply Iff.intro
State after:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
⊢ [[p₁]] = [[p₂]] → reduction p₁ = reduction p₂

case mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
⊢ reduction p₁ = reduction p₂ → [[p₁]] = [[p₂]]

State before:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
⊢ [[p₁]] = [[p₂]] → reduction p₁ = reduction p₂
Tactic:
intro eql
State after:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[p₁]] = [[p₂]]
⊢ reduction p₁ = reduction p₂

State before:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[p₁]] = [[p₂]]
⊢ reduction p₁ = reduction p₂
Tactic:
rw [← reduction_homotopic_self p₁, ← reduction_homotopic_self p₂] at eql
State after:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[reduction p₁]] = [[reduction p₂]]
⊢ reduction p₁ = reduction p₂

State before:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[reduction p₁]] = [[reduction p₂]]
⊢ reduction p₁ = reduction p₂
Tactic:
have red₁ : reduced (reduction p₁) := by
  apply reduction_reduced
State after:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[reduction p₁]] = [[reduction p₂]]
red₁ : reduced (reduction p₁)
⊢ reduction p₁ = reduction p₂

State before:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[reduction p₁]] = [[reduction p₂]]
red₁ : reduced (reduction p₁)
⊢ reduction p₁ = reduction p₂
Tactic:
have red₂ : reduced (reduction p₂) := by
  apply reduction_reduced
State after:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[reduction p₁]] = [[reduction p₂]]
red₁ : reduced (reduction p₁)
red₂ : reduced (reduction p₂)
⊢ reduction p₁ = reduction p₂

State before:
case mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[reduction p₁]] = [[reduction p₂]]
red₁ : reduced (reduction p₁)
red₂ : reduced (reduction p₂)
⊢ reduction p₁ = reduction p₂
Tactic:
exact reduced_unique x₀ τ red₁ red₂ eql
State after:
no goals

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[reduction p₁]] = [[reduction p₂]]
⊢ reduced (reduction p₁)
Tactic:
apply reduction_reduced
State after:
no goals

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
eql : [[reduction p₁]] = [[reduction p₂]]
red₁ : reduced (reduction p₁)
⊢ reduced (reduction p₂)
Tactic:
apply reduction_reduced
State after:
no goals

State before:
case mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
⊢ reduction p₁ = reduction p₂ → [[p₁]] = [[p₂]]
Tactic:
intro hyp
State after:
case mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp : reduction p₁ = reduction p₂
⊢ [[p₁]] = [[p₂]]

State before:
case mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp : reduction p₁ = reduction p₂
⊢ [[p₁]] = [[p₂]]
Tactic:
rw [← reduction_homotopic_self p₁, ← reduction_homotopic_self p₂]
State after:
case mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp : reduction p₁ = reduction p₂
⊢ [[reduction p₁]] = [[reduction p₂]]

State before:
case mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
hyp : reduction p₁ = reduction p₂
⊢ [[reduction p₁]] = [[reduction p₂]]
Tactic:
rw [hyp]
State after:
no goals