internlm/Lean-Github huggingface dataset:
Theorem: Graph.SubgroupCover.terminal₁_eq_of_r
Proof 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]
Proof state after:
no goals
Theorem: Graph.SubgroupCover.terminal₀_eq_of_r
Proof 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
Proof 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₂.τ₀
Theorem: Graph.SubgroupCover.terminal₀_eq_of_r
Proof 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
Proof 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₂.τ₀
Theorem: Graph.SubgroupCover.terminal₀_eq_of_r
Proof 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
Proof 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₂.τ₀
Theorem: Graph.SubgroupCover.terminal₀_eq_of_r
Proof 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]
Proof state after:
no goals
Theorem: Graph.SubgroupCover.edge_eq_of_r
Proof 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₁.nxt.edge = e₂.nxt.edge
Tactic:
intro ⟨τ₀, τ₁, e, p, _⟩ ⟨τ₀', τ₁', e', p', _⟩
Proof 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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
τ₀' τ₁' : V
e' : EdgeBetween G τ₀' τ₁'
p' : EdgePath G x₀ τ₀'
is_reduced✝ : reduced p'
⊢ Setoid.r { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }
      { τ₀ := τ₀', τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ } →
    { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }.nxt.edge =
      { τ₀ := τ₀', τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ }.nxt.edge
Theorem: Graph.SubgroupCover.edge_eq_of_r
Proof 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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
τ₀' τ₁' : V
e' : EdgeBetween G τ₀' τ₁'
p' : EdgePath G x₀ τ₀'
is_reduced✝ : reduced p'
⊢ Setoid.r { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }
      { τ₀ := τ₀', τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ } →
    { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }.nxt.edge =
      { τ₀ := τ₀', τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ }.nxt.edge
Tactic:
if c:τ₀=τ₀' ∧ τ₁ = τ₁' then
  cases c.left
  cases c.right
  simp [Setoid.r, relH]
  intro _ h
  rw [h]
else
  simp [Setoid.r, relH, c]
Proof state after:
no goals
Theorem: Graph.SubgroupCover.edge_eq_of_r
Proof 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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
τ₀' τ₁' : V
e' : EdgeBetween G τ₀' τ₁'
p' : EdgePath G x₀ τ₀'
is_reduced✝ : reduced p'
c : τ₀ = τ₀' ∧ τ₁ = τ₁'
⊢ Setoid.r { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }
      { τ₀ := τ₀', τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ } →
    { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }.nxt.edge =
      { τ₀ := τ₀', τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ }.nxt.edge
Tactic:
cases c.left
Proof state after:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
τ₁' : V
e' : EdgeBetween G τ₀ τ₁'
p' : EdgePath G x₀ τ₀
is_reduced✝ : reduced p'
c : τ₀ = τ₀ ∧ τ₁ = τ₁'
⊢ Setoid.r { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }
      { τ₀ := τ₀, τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ } →
    { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }.nxt.edge =
      { τ₀ := τ₀, τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ }.nxt.edge
Theorem: Graph.SubgroupCover.edge_eq_of_r
Proof state before:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
τ₁' : V
e' : EdgeBetween G τ₀ τ₁'
p' : EdgePath G x₀ τ₀
is_reduced✝ : reduced p'
c : τ₀ = τ₀ ∧ τ₁ = τ₁'
⊢ Setoid.r { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }
      { τ₀ := τ₀, τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ } →
    { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }.nxt.edge =
      { τ₀ := τ₀, τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ }.nxt.edge
Tactic:
cases c.right
Proof state after:
case refl.refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
p' : EdgePath G x₀ τ₀
is_reduced✝ : reduced p'
e' : EdgeBetween G τ₀ τ₁
c : τ₀ = τ₀ ∧ τ₁ = τ₁
⊢ Setoid.r { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }
      { τ₀ := τ₀, τ₁ := τ₁, nxt := e', p := p', is_reduced := is_reduced✝ } →
    { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }.nxt.edge =
      { τ₀ := τ₀, τ₁ := τ₁, nxt := e', p := p', is_reduced := is_reduced✝ }.nxt.edge
Theorem: Graph.SubgroupCover.edge_eq_of_r
Proof state before:
case refl.refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
p' : EdgePath G x₀ τ₀
is_reduced✝ : reduced p'
e' : EdgeBetween G τ₀ τ₁
c : τ₀ = τ₀ ∧ τ₁ = τ₁
⊢ Setoid.r { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }
      { τ₀ := τ₀, τ₁ := τ₁, nxt := e', p := p', is_reduced := is_reduced✝ } →
    { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }.nxt.edge =
      { τ₀ := τ₀, τ₁ := τ₁, nxt := e', p := p', is_reduced := is_reduced✝ }.nxt.edge
Tactic:
simp [Setoid.r, relH]
Proof state after:
case refl.refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
p' : EdgePath G x₀ τ₀
is_reduced✝ : reduced p'
e' : EdgeBetween G τ₀ τ₁
c : τ₀ = τ₀ ∧ τ₁ = τ₁
⊢ [[p ++ reverse p']] ∈ H → e = e' → e.edge = e'.edge
Theorem: Graph.SubgroupCover.edge_eq_of_r
Proof state before:
case refl.refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
p' : EdgePath G x₀ τ₀
is_reduced✝ : reduced p'
e' : EdgeBetween G τ₀ τ₁
c : τ₀ = τ₀ ∧ τ₁ = τ₁
⊢ [[p ++ reverse p']] ∈ H → e = e' → e.edge = e'.edge
Tactic:
intro _ h
Proof state after:
case refl.refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
p' : EdgePath G x₀ τ₀
is_reduced✝ : reduced p'
e' : EdgeBetween G τ₀ τ₁
c : τ₀ = τ₀ ∧ τ₁ = τ₁
a✝ : [[p ++ reverse p']] ∈ H
h : e = e'
⊢ e.edge = e'.edge
Theorem: Graph.SubgroupCover.edge_eq_of_r
Proof state before:
case refl.refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
p' : EdgePath G x₀ τ₀
is_reduced✝ : reduced p'
e' : EdgeBetween G τ₀ τ₁
c : τ₀ = τ₀ ∧ τ₁ = τ₁
a✝ : [[p ++ reverse p']] ∈ H
h : e = e'
⊢ e.edge = e'.edge
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Graph.SubgroupCover.edge_eq_of_r
Proof 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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
τ₀' τ₁' : V
e' : EdgeBetween G τ₀' τ₁'
p' : EdgePath G x₀ τ₀'
is_reduced✝ : reduced p'
c : ¬(τ₀ = τ₀' ∧ τ₁ = τ₁')
⊢ Setoid.r { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }
      { τ₀ := τ₀', τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ } →
    { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }.nxt.edge =
      { τ₀ := τ₀', τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ }.nxt.edge
Tactic:
simp [Setoid.r, relH, c]
Proof state after:
no goals
Theorem: Graph.SubgroupCover.Quot.bar_bar
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ ∀ (ebar : Quotient (edgeSetoid H)), bar H (bar H ebar) = ebar
Tactic:
apply Quotient.ind
Proof state after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ ∀ (a : Edge G x₀), bar H (bar H ⟦a⟧) = ⟦a⟧
Theorem: Graph.SubgroupCover.Quot.bar_bar
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ ∀ (a : Edge G x₀), bar H (bar H ⟦a⟧) = ⟦a⟧
Tactic:
intro e
Proof state after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
e : Edge G x₀
⊢ bar H (bar H ⟦e⟧) = ⟦e⟧
Theorem: Graph.SubgroupCover.Quot.bar_bar
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
e : Edge G x₀
⊢ bar H (bar H ⟦e⟧) = ⟦e⟧
Tactic:
simp [bar_eq_barn]
Proof state after:
no goals
Theorem: Graph.SubgroupCover.Quot.bar_ne_self
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ ∀ (ebar : Quotient (edgeSetoid H)), ebar ≠ bar H ebar
Tactic:
apply Quotient.ind
Proof state after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ ∀ (a : Edge G x₀), ⟦a⟧ ≠ bar H ⟦a⟧
Theorem: Graph.SubgroupCover.Quot.bar_ne_self
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ ∀ (a : Edge G x₀), ⟦a⟧ ≠ bar H ⟦a⟧
Tactic:
intro ⟨τ₀, τ₁, e, p, pf⟩
Proof state after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
⊢ ⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧ ≠
    bar H ⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧
Theorem: Graph.SubgroupCover.Quot.bar_ne_self
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
⊢ ⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧ ≠
    bar H ⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧
Tactic:
simp [bar_eq_barn, Edge.bar_eq_bar]
Proof state after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
⊢ ¬⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧ =
      ⟦{ τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }⟧
Theorem: Graph.SubgroupCover.Quot.bar_ne_self
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
⊢ ¬⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧ =
      ⟦{ τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }⟧
Tactic:
intro contra
Proof state after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
contra :
  ⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧ =
    ⟦{ τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }⟧
⊢ False
Theorem: Graph.SubgroupCover.Quot.bar_ne_self
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
contra :
  ⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧ =
    ⟦{ τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }⟧
⊢ False
Tactic:
rw [@Quotient.eq _ (edgeSetoid H)] at contra
Proof state after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
contra :
  { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
⊢ False
Theorem: Graph.SubgroupCover.Quot.bar_ne_self
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
contra :
  { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
⊢ False
Tactic:
let lem := terminal₀_eq_of_r H contra
Proof state after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
contra :
  { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }.τ₀ =
  { τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }.τ₀ :=
  terminal₀_eq_of_r H contra
⊢ False
Theorem: Graph.SubgroupCover.Quot.bar_ne_self
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
contra :
  { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }.τ₀ =
  { τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }.τ₀ :=
  terminal₀_eq_of_r H contra
⊢ False
Tactic:
simp only at lem
Proof state after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
contra :
  { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : τ₀ = τ₁ := terminal₀_eq_of_r H contra
⊢ False
Theorem: Graph.SubgroupCover.Quot.bar_ne_self
Proof state before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
contra :
  { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : τ₀ = τ₁ := terminal₀_eq_of_r H contra
⊢ False
Tactic:
cases lem
Proof state after:
case a.refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ : V
p : EdgePath G x₀ τ₀
pf : reduced p
e : EdgeBetween G τ₀ τ₀
contra :
  { τ₀ := τ₀, τ₁ := τ₀, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₀, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : τ₀ = τ₀ := terminal₀_eq_of_r H contra
⊢ False
Theorem: Graph.SubgroupCover.Quot.bar_ne_self
Proof state before:
case a.refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ : V
p : EdgePath G x₀ τ₀
pf : reduced p
e : EdgeBetween G τ₀ τ₀
contra :
  { τ₀ := τ₀, τ₁ := τ₀, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₀, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : τ₀ = τ₀ := terminal₀_eq_of_r H contra
⊢ False
Tactic:
simp [HasEquiv.Equiv, Setoid.r, relH] at contra
Proof state after:
case a.refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ : V
p : EdgePath G x₀ τ₀
pf : reduced p
e : EdgeBetween G τ₀ τ₀
contra✝ :
  { τ₀ := τ₀, τ₁ := τ₀, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₀, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : τ₀ = τ₀ := terminal₀_eq_of_r H contra✝
contra : [[p ++ reverse (p:+e)]] ∈ H ∧ e = EdgeBetween.bar e
⊢ False