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₀)
e₁ e₂ : Edge G x₀
⊢ Setoid.r e₁ e₂ → e₁.τ₁ = e₂.τ₁
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₀)
e₁ e₂ : Edge G x₀
h : Setoid.r e₁ e₂
⊢ e₁.τ₁ = e₂.τ₁

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
e₁ e₂ : Edge G x₀
h : Setoid.r e₁ e₂
⊢ e₁.τ₁ = e₂.τ₁
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₀)
e₁ e₂ : Edge G x₀
h :
  if h : e₁.τ₀ = e₂.τ₀ ∧ e₁.τ₁ = e₂.τ₁ then
    Eq.rec (motive := fun a t => e₂.τ₀ = a → HEq (_ : e₁.τ₀ = e₂.τ₀) t → Prop)
      (fun h_1 =>
        Eq.rec (motive := fun x x_1 =>
          EdgeBetween G x e₂.τ₁ →
            (p' : EdgePath G x₀ x) →
              reduced p' → e₁.τ₀ = x ∧ e₁.τ₁ = e₂.τ₁ → (x_2 : e₁.τ₀ = x) → HEq x_2 (_ : e₁.τ₀ = e₁.τ₀) → Prop)
          (fun e' p' is_reduced c x h =>
            Eq.rec (motive := fun a t => e₂.τ₁ = a → HEq (_ : e₁.τ₁ = e₂.τ₁) t → Prop)
              (fun h =>
                Eq.rec (motive := fun x x_1 =>
                  EdgeBetween G e₁.τ₀ x →
                    e₁.τ₀ = e₁.τ₀ ∧ e₁.τ₁ = x → (x_2 : e₁.τ₁ = x) → HEq x_2 (_ : e₁.τ₁ = e₁.τ₁) → Prop)
                  (fun e' c x h => relH H e₁.p p' ∧ e₁.nxt = e') (_ : e₁.τ₁ = e₂.τ₁) e' c (_ : e₁.τ₁ = e₂.τ₁))
              (_ : e₁.τ₁ = e₂.τ₁) (_ : e₂.τ₁ = e₂.τ₁) (_ : HEq (_ : e₁.τ₁ = e₂.τ₁) (_ : e₁.τ₁ = e₂.τ₁)))
          (_ : e₁.τ₀ = e₂.τ₀) e₂.nxt e₂.p (_ : reduced e₂.p) (_ : e₁.τ₀ = e₂.τ₀ ∧ e₁.τ₁ = e₂.τ₁) (_ : e₁.τ₀ = e₂.τ₀))
      (_ : e₁.τ₀ = e₂.τ₀) (_ : e₂.τ₀ = e₂.τ₀) (_ : HEq (_ : e₁.τ₀ = e₂.τ₀) (_ : e₁.τ₀ = e₂.τ₀))
  else False
⊢ e₁.τ₁ = e₂.τ₁

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
e₁ e₂ : Edge G x₀
h :
  if h : e₁.τ₀ = e₂.τ₀ ∧ e₁.τ₁ = e₂.τ₁ then
    Eq.rec (motive := fun a t => e₂.τ₀ = a → HEq (_ : e₁.τ₀ = e₂.τ₀) t → Prop)
      (fun h_1 =>
        Eq.rec (motive := fun x x_1 =>
          EdgeBetween G x e₂.τ₁ →
            (p' : EdgePath G x₀ x) →
              reduced p' → e₁.τ₀ = x ∧ e₁.τ₁ = e₂.τ₁ → (x_2 : e₁.τ₀ = x) → HEq x_2 (_ : e₁.τ₀ = e₁.τ₀) → Prop)
          (fun e' p' is_reduced c x h =>
            Eq.rec (motive := fun a t => e₂.τ₁ = a → HEq (_ : e₁.τ₁ = e₂.τ₁) t → Prop)
              (fun h =>
                Eq.rec (motive := fun x x_1 =>
                  EdgeBetween G e₁.τ₀ x →
                    e₁.τ₀ = e₁.τ₀ ∧ e₁.τ₁ = x → (x_2 : e₁.τ₁ = x) → HEq x_2 (_ : e₁.τ₁ = e₁.τ₁) → Prop)
                  (fun e' c x h => relH H e₁.p p' ∧ e₁.nxt = e') (_ : e₁.τ₁ = e₂.τ₁) e' c (_ : e₁.τ₁ = e₂.τ₁))
              (_ : e₁.τ₁ = e₂.τ₁) (_ : e₂.τ₁ = e₂.τ₁) (_ : HEq (_ : e₁.τ₁ = e₂.τ₁) (_ : e₁.τ₁ = e₂.τ₁)))
          (_ : e₁.τ₀ = e₂.τ₀) e₂.nxt e₂.p (_ : reduced e₂.p) (_ : e₁.τ₀ = e₂.τ₀ ∧ e₁.τ₁ = e₂.τ₁) (_ : e₁.τ₀ = e₂.τ₀))
      (_ : e₁.τ₀ = e₂.τ₀) (_ : e₂.τ₀ = e₂.τ₀) (_ : HEq (_ : e₁.τ₀ = e₂.τ₀) (_ : e₁.τ₀ = e₂.τ₀))
  else False
⊢ e₁.τ₁ = e₂.τ₁
Tactic:
by_cases c:(e₁.τ₁=e₂.τ₁) <;> 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₀)
e₁ e₂ : Edge G x₀
c : e₁.τ₁ = e₂.τ₁
h :
  if h : e₁.τ₀ = e₂.τ₀ then
    Eq.rec (motive := fun a t => e₂.τ₀ = a → HEq (_ : e₁.τ₀ = e₂.τ₀) t → Prop)
      (fun h_1 =>
        Eq.rec (motive := fun x x_1 =>
          EdgeBetween G x e₂.τ₁ →
            (p' : EdgePath G x₀ x) →
              reduced p' → e₁.τ₀ = x ∧ e₁.τ₁ = e₂.τ₁ → (x_2 : e₁.τ₀ = x) → HEq x_2 (_ : e₁.τ₀ = e₁.τ₀) → Prop)
          (fun e' p' is_reduced c x h =>
            Eq.rec (motive := fun a t => e₂.τ₁ = a → HEq (_ : e₁.τ₁ = e₂.τ₁) t → Prop)
              (fun h =>
                Eq.rec (motive := fun x x_1 =>
                  EdgeBetween G e₁.τ₀ x →
                    e₁.τ₀ = e₁.τ₀ ∧ e₁.τ₁ = x → (x_2 : e₁.τ₁ = x) → HEq x_2 (_ : e₁.τ₁ = e₁.τ₁) → Prop)
                  (fun e' c x h => relH H e₁.p p' ∧ e₁.nxt = e') (_ : e₁.τ₁ = e₂.τ₁) e' c (_ : e₁.τ₁ = e₂.τ₁))
              (_ : e₁.τ₁ = e₂.τ₁) (_ : e₂.τ₁ = e₂.τ₁) (_ : HEq (_ : e₁.τ₁ = e₂.τ₁) (_ : e₁.τ₁ = e₂.τ₁)))
          (_ : e₁.τ₀ = e₂.τ₀) e₂.nxt e₂.p (_ : reduced e₂.p) (_ : e₁.τ₀ = e₂.τ₀ ∧ e₁.τ₁ = e₂.τ₁) (_ : e₁.τ₀ = e₂.τ₀))
      (_ : e₁.τ₀ = e₂.τ₀) (_ : e₂.τ₀ = e₂.τ₀) (_ : HEq (_ : e₁.τ₀ = e₂.τ₀) (_ : e₁.τ₀ = e₂.τ₀))
  else False
⊢ e₁.τ₁ = e₂.τ₁

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₀)
e₁ e₂ : Edge G x₀
c : e₁.τ₁ = e₂.τ₁
h :
  if h : e₁.τ₀ = e₂.τ₀ then
    Eq.rec (motive := fun a t => e₂.τ₀ = a → HEq (_ : e₁.τ₀ = e₂.τ₀) t → Prop)
      (fun h_1 =>
        Eq.rec (motive := fun x x_1 =>
          EdgeBetween G x e₂.τ₁ →
            (p' : EdgePath G x₀ x) →
              reduced p' → e₁.τ₀ = x ∧ e₁.τ₁ = e₂.τ₁ → (x_2 : e₁.τ₀ = x) → HEq x_2 (_ : e₁.τ₀ = e₁.τ₀) → Prop)
          (fun e' p' is_reduced c x h =>
            Eq.rec (motive := fun a t => e₂.τ₁ = a → HEq (_ : e₁.τ₁ = e₂.τ₁) t → Prop)
              (fun h =>
                Eq.rec (motive := fun x x_1 =>
                  EdgeBetween G e₁.τ₀ x →
                    e₁.τ₀ = e₁.τ₀ ∧ e₁.τ₁ = x → (x_2 : e₁.τ₁ = x) → HEq x_2 (_ : e₁.τ₁ = e₁.τ₁) → Prop)
                  (fun e' c x h => relH H e₁.p p' ∧ e₁.nxt = e') (_ : e₁.τ₁ = e₂.τ₁) e' c (_ : e₁.τ₁ = e₂.τ₁))
              (_ : e₁.τ₁ = e₂.τ₁) (_ : e₂.τ₁ = e₂.τ₁) (_ : HEq (_ : e₁.τ₁ = e₂.τ₁) (_ : e₁.τ₁ = e₂.τ₁)))
          (_ : e₁.τ₀ = e₂.τ₀) e₂.nxt e₂.p (_ : reduced e₂.p) (_ : e₁.τ₀ = e₂.τ₀ ∧ e₁.τ₁ = e₂.τ₁) (_ : e₁.τ₀ = e₂.τ₀))
      (_ : e₁.τ₀ = e₂.τ₀) (_ : e₂.τ₀ = e₂.τ₀) (_ : HEq (_ : e₁.τ₀ = e₂.τ₀) (_ : e₁.τ₀ = e₂.τ₀))
  else False
⊢ e₁.τ₁ = e₂.τ₁
Tactic:
simp [c]
State after:
no goals