Theorem: Graph.SubgroupCover.terminal_eq_of_r (GroupComp/Graph/SubgroupCover.lean)

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
v₁ v₂ : Vert G x₀
⊢ Setoid.r v₁ v₂ → v₁.τ = v₂.τ
Tactic:
intro h
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
v₁ v₂ : Vert G x₀
h : Setoid.r v₁ v₂
⊢ v₁.τ = v₂.τ

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
v₁ v₂ : Vert G x₀
h : Setoid.r v₁ v₂
⊢ v₁.τ = v₂.τ
Tactic:
simp [Setoid.r] at h
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
v₁ v₂ : Vert G x₀
h :
  if h : v₁.τ = v₂.τ then
    Eq.rec (motive := fun a t => v₂.τ = a → HEq (_ : v₁.τ = v₂.τ) t → Prop)
      (fun h_1 =>
        Eq.rec (motive := fun x x_1 =>
          (v₂ : EdgePath G x₀ x) → reduced v₂ → (c : v₁.τ = x) → HEq c (_ : v₁.τ = v₁.τ) → Prop)
          (fun v₂ is_reduced c h => relH H v₁.p v₂) (_ : v₁.τ = v₂.τ) v₂.p (_ : reduced v₂.p) (_ : v₁.τ = v₂.τ))
      (_ : v₁.τ = v₂.τ) (_ : v₂.τ = v₂.τ) (_ : HEq (_ : v₁.τ = v₂.τ) (_ : v₁.τ = v₂.τ))
  else False
⊢ v₁.τ = v₂.τ

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
v₁ v₂ : Vert G x₀
h :
  if h : v₁.τ = v₂.τ then
    Eq.rec (motive := fun a t => v₂.τ = a → HEq (_ : v₁.τ = v₂.τ) t → Prop)
      (fun h_1 =>
        Eq.rec (motive := fun x x_1 =>
          (v₂ : EdgePath G x₀ x) → reduced v₂ → (c : v₁.τ = x) → HEq c (_ : v₁.τ = v₁.τ) → Prop)
          (fun v₂ is_reduced c h => relH H v₁.p v₂) (_ : v₁.τ = v₂.τ) v₂.p (_ : reduced v₂.p) (_ : v₁.τ = v₂.τ))
      (_ : v₁.τ = v₂.τ) (_ : v₂.τ = v₂.τ) (_ : HEq (_ : v₁.τ = v₂.τ) (_ : v₁.τ = v₂.τ))
  else False
⊢ v₁.τ = v₂.τ
Tactic:
by_cases c:v₁.τ=v₂.τ <;> simp [c] at h
State after:
case pos
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
v₁ v₂ : Vert G x₀
c : v₁.τ = v₂.τ
h :
  Eq.rec (motive := fun a t => v₂.τ = a → HEq (_ : v₁.τ = v₂.τ) t → Prop)
    (fun h =>
      Eq.rec (motive := fun x x_1 =>
        (v₂ : EdgePath G x₀ x) → reduced v₂ → (c : v₁.τ = x) → HEq c (_ : v₁.τ = v₁.τ) → Prop)
        (fun v₂ is_reduced c h => relH H v₁.p v₂) (_ : v₁.τ = v₂.τ) v₂.p (_ : reduced v₂.p) (_ : v₁.τ = v₂.τ))
    (_ : v₁.τ = v₂.τ) (_ : v₂.τ = v₂.τ) (_ : HEq (_ : v₁.τ = v₂.τ) (_ : v₁.τ = v₂.τ))
⊢ v₁.τ = v₂.τ

State before:
case pos
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
v₁ v₂ : Vert G x₀
c : v₁.τ = v₂.τ
h :
  Eq.rec (motive := fun a t => v₂.τ = a → HEq (_ : v₁.τ = v₂.τ) t → Prop)
    (fun h =>
      Eq.rec (motive := fun x x_1 =>
        (v₂ : EdgePath G x₀ x) → reduced v₂ → (c : v₁.τ = x) → HEq c (_ : v₁.τ = v₁.τ) → Prop)
        (fun v₂ is_reduced c h => relH H v₁.p v₂) (_ : v₁.τ = v₂.τ) v₂.p (_ : reduced v₂.p) (_ : v₁.τ = v₂.τ))
    (_ : v₁.τ = v₂.τ) (_ : v₂.τ = v₂.τ) (_ : HEq (_ : v₁.τ = v₂.τ) (_ : v₁.τ = v₂.τ))
⊢ v₁.τ = v₂.τ
Tactic:
simp [c]
State after:
no goals