internlm/Lean-Github huggingface dataset:
Theorem: Graph.SubgroupCover.Quot.localSection_composition'
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
p : EdgePath G x₀ τ
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ = G.ι nxt.edge
this :
  { τ₀ := τ, τ₁ := Graph.τ G nxt.edge,
      nxt :=
        { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ),
          term_eq := (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) },
      p := p, is_reduced := is_reduced } =
    { τ₀ := τ, τ₁ := τ₁,
      nxt := { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = τ₁) }, p := p,
      is_reduced := is_reduced }
⊢ { τ₀ := τ, τ₁ := τ₁,
      nxt := { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = τ₁) }, p := p,
      is_reduced := is_reduced } ≈
    { τ₀ := τ, τ₁ := τ₁,
      nxt := { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = τ₁) }, p := p,
      is_reduced := is_reduced }
Tactic:
apply @Setoid.refl _ (edgeSetoid H)
Proof state after:
no goals
Theorem: Graph.SubgroupCover.Quot.localSection_composition'
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
p : EdgePath G x₀ τ
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ = G.ι nxt.edge
⊢ { τ₀ := τ, τ₁ := Graph.τ G nxt.edge,
      nxt :=
        { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ),
          term_eq := (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) },
      p := p, is_reduced := is_reduced } =
    { τ₀ := τ, τ₁ := τ₁,
      nxt := { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = τ₁) }, p := p,
      is_reduced := is_reduced }
Tactic:
simp [nxt.term_eq, eq_of_edge_eq]
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
p : EdgePath G x₀ τ
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ = G.ι nxt.edge
⊢ HEq { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) }
    { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = τ₁) }
Theorem: Graph.SubgroupCover.Quot.localSection_composition'
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
p : EdgePath G x₀ τ
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ = G.ι nxt.edge
⊢ HEq { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) }
    { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = τ₁) }
Tactic:
congr
Proof state after:
case e_5.h
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₀ τ
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ = G.ι nxt.edge
⊢ Graph.τ G nxt.edge = τ₁

case e_8
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₀ τ
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ = G.ι nxt.edge
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) (_ : Graph.τ G nxt.edge = τ₁)
Theorem: Graph.SubgroupCover.Quot.localSection_composition'
Proof state before:
case e_5.h
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₀ τ
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ = G.ι nxt.edge
⊢ Graph.τ G nxt.edge = τ₁

case e_8
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₀ τ
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ = G.ι nxt.edge
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) (_ : Graph.τ G nxt.edge = τ₁)
Tactic:
rw [nxt.term_eq]
Proof state after:
case e_8
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₀ τ
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ = G.ι nxt.edge
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) (_ : Graph.τ G nxt.edge = τ₁)
Theorem: Graph.SubgroupCover.Quot.localSection_composition'
Proof state before:
case e_8
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₀ τ
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ = G.ι nxt.edge
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) (_ : Graph.τ G nxt.edge = τ₁)
Tactic:
have l {τ : V}(pf: G.τ nxt.edge = τ) :
  HEq (rfl: G.τ nxt.edge  = G.τ nxt.edge ) pf   := by
  cases pf
  simp
Proof state after:
case e_8
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₀ τ
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ = G.ι nxt.edge
l : ∀ {τ : V} (pf : Graph.τ G nxt.edge = τ), HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) pf
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) (_ : Graph.τ G nxt.edge = τ₁)
Theorem: Graph.SubgroupCover.Quot.localSection_composition'
Proof state before:
case e_8
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₀ τ
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ = G.ι nxt.edge
l : ∀ {τ : V} (pf : Graph.τ G nxt.edge = τ), HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) pf
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) (_ : Graph.τ G nxt.edge = τ₁)
Tactic:
apply l nxt.term_eq
Proof state after:
no goals
Theorem: Graph.SubgroupCover.Quot.localSection_composition'
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
p : EdgePath G x₀ τ✝
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ✝ = G.ι nxt.edge
τ : V
pf : Graph.τ G nxt.edge = τ
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) pf
Tactic:
cases pf
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
p : EdgePath G x₀ τ
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ = G.ι nxt.edge
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge)
Theorem: Graph.SubgroupCover.Quot.localSection_composition'
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
p : EdgePath G x₀ τ
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ = G.ι nxt.edge
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge)
Tactic:
simp
Proof state after:
no goals
Theorem: Graph.SubgroupCover.Quot.edge_from
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 : Edge G x₀
τ₀ : V
⊢ τ₀ = e.τ₀ → ∃ τ₁ nxt p', ∃ (red : reduced p'), e = { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }
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 : Edge G x₀
τ₀ : V
h : τ₀ = e.τ₀
⊢ ∃ τ₁ nxt p', ∃ (red : reduced p'), e = { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }
Theorem: Graph.SubgroupCover.Quot.edge_from
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 : Edge G x₀
τ₀ : V
h : τ₀ = e.τ₀
⊢ ∃ τ₁ nxt p', ∃ (red : reduced p'), e = { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }
Tactic:
cases h
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₀)
e : Edge G x₀
⊢ ∃ τ₁ nxt p', ∃ (red : reduced p'), e = { τ₀ := e.τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }
Theorem: Graph.SubgroupCover.Quot.edge_from
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₀)
e : Edge G x₀
⊢ ∃ τ₁ nxt p', ∃ (red : reduced p'), e = { τ₀ := e.τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }
Tactic:
use e.τ₁, e.nxt, e.p, e.is_reduced
Proof state after:
no goals
Theorem: Graph.SubgroupCover.Quot.edge_to
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 : Edge G x₀
τ₀ τ₁ : V
⊢ τ₀ = e.τ₀ →
    e.τ₁ = τ₁ → ∃ nxt p', ∃ (red : reduced p'), e = { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }
Tactic:
intro h₁ 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 : Edge G x₀
τ₀ τ₁ : V
h₁ : τ₀ = e.τ₀
h₂ : e.τ₁ = τ₁
⊢ ∃ nxt p', ∃ (red : reduced p'), e = { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }
Theorem: Graph.SubgroupCover.Quot.edge_to
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 : Edge G x₀
τ₀ τ₁ : V
h₁ : τ₀ = e.τ₀
h₂ : e.τ₁ = τ₁
⊢ ∃ nxt p', ∃ (red : reduced p'), e = { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }
Tactic:
cases h₁
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₀)
e : Edge G x₀
τ₁ : V
h₂ : e.τ₁ = τ₁
⊢ ∃ nxt p', ∃ (red : reduced p'), e = { τ₀ := e.τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }
Theorem: Graph.SubgroupCover.Quot.edge_to
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₀)
e : Edge G x₀
τ₁ : V
h₂ : e.τ₁ = τ₁
⊢ ∃ nxt p', ∃ (red : reduced p'), e = { τ₀ := e.τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }
Tactic:
cases 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₀)
e : Edge G x₀
⊢ ∃ nxt p', ∃ (red : reduced p'), e = { τ₀ := e.τ₀, τ₁ := e.τ₁, nxt := nxt, p := p', is_reduced := red }
Theorem: Graph.SubgroupCover.Quot.edge_to
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₀)
e : Edge G x₀
⊢ ∃ nxt p', ∃ (red : reduced p'), e = { τ₀ := e.τ₀, τ₁ := e.τ₁, nxt := nxt, p := p', is_reduced := red }
Tactic:
use e.nxt, e.p, e.is_reduced
Proof state after:
no goals
Theorem: Graph.SubgroupCover.liftFactors
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₀)
w₂ : V
e : EdgePath G x₀ w₂
⊢ lift e (groupCoverProj H) (basepoint H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) =
    liftViaUniv H e
Tactic:
apply unique_Pathlift
Proof state after:
no goals
Theorem: Graph.SubgroupCover.liftTermFactors
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₀)
w₂ : V
e : EdgePath G x₀ w₂
⊢ (lift e (groupCoverProj H) (basepoint H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))).τ =
    ⟦liftTerminal (proj G x₀) (UniversalCover.basepoint G x₀)
        (_ : (proj G x₀).toFuncV (UniversalCover.basepoint G x₀) = (proj G x₀).toFuncV (UniversalCover.basepoint G x₀))
        e⟧
Tactic:
rw [liftFactors]
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₀)
w₂ : V
e : EdgePath G x₀ w₂
⊢ (liftViaUniv H e).τ =
    ⟦liftTerminal (proj G x₀) (UniversalCover.basepoint G x₀)
        (_ : (proj G x₀).toFuncV (UniversalCover.basepoint G x₀) = (proj G x₀).toFuncV (UniversalCover.basepoint G x₀))
        e⟧
Theorem: Graph.SubgroupCover.liftTermFactors
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₀)
w₂ : V
e : EdgePath G x₀ w₂
⊢ (liftViaUniv H e).τ =
    ⟦liftTerminal (proj G x₀) (UniversalCover.basepoint G x₀)
        (_ : (proj G x₀).toFuncV (UniversalCover.basepoint G x₀) = (proj G x₀).toFuncV (UniversalCover.basepoint G x₀))
        e⟧
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.SubgroupCover.reduced_liftTerminal_factor
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₀)
w₂ : V
e : EdgePath G x₀ w₂
hyp : reduced e
⊢ (lift e (groupCoverProj H) (basepoint H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))).τ =
    ⟦{ τ := w₂, p := e, is_reduced := hyp }⟧
Tactic:
rw [liftTermFactors, reduced_liftTerminal]
Proof state after:
no goals
Theorem: Graph.SubgroupCover.reduced_liftTerminal_factor'
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₀)
w₂ : V
e : EdgePath G x₀ w₂
hyp : reduced e
⊢ liftTerminal (groupCoverProj H) (basepoint H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) e =
    ⟦{ τ := w₂, p := e, is_reduced := hyp }⟧
Tactic:
apply reduced_liftTerminal_factor
Proof state after:
no goals
Theorem: Graph.SubgroupCover.imageInSubgroup
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₀)
⊢ ∀ (h : π₁ (groupCover H) (basepoint H)),
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h ∈
      H
Tactic:
apply Quot.ind
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ ∀ (a : EdgePath (groupCover H) (basepoint H) (basepoint H)),
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        (Quot.mk Reduction a) ∈
      H
Theorem: Graph.SubgroupCover.imageInSubgroup
Proof state before:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ ∀ (a : EdgePath (groupCover H) (basepoint H) (basepoint H)),
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        (Quot.mk Reduction a) ∈
      H
Tactic:
intro η
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
⊢ (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      (Quot.mk Reduction η) ∈
    H
Theorem: Graph.SubgroupCover.imageInSubgroup
Proof state before:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
⊢ (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      (Quot.mk Reduction η) ∈
    H
Tactic:
let θ : EdgePath G x₀ x₀ := η.map (groupCoverProj H)
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
⊢ (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      (Quot.mk Reduction η) ∈
    H
Theorem: Graph.SubgroupCover.imageInSubgroup
Proof state before:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
⊢ (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      (Quot.mk Reduction η) ∈
    H
Tactic:
let heqn := reduction_homotopic_self θ
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
⊢ (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      (Quot.mk Reduction η) ∈
    H
Theorem: Graph.SubgroupCover.imageInSubgroup
Proof state before:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
⊢ (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      (Quot.mk Reduction η) ∈
    H
Tactic:
simp [Morphism.π₁map, PathClass.map]
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
⊢ [[EdgePath.map η (groupCoverProj H)]] ∈ H
Theorem: Graph.SubgroupCover.imageInSubgroup
Proof state before:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
⊢ [[EdgePath.map η (groupCoverProj H)]] ∈ H
Tactic:
rw [← heqn]
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
⊢ [[reduction θ]] ∈ H
Theorem: Graph.SubgroupCover.imageInSubgroup
Proof state before:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
⊢ [[reduction θ]] ∈ H
Tactic:
have term_eqn :=
  liftTerminal_eq_of_homotopic (groupCoverProj H)
  (basepoint H) rfl heqn
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
term_eqn :
  liftTerminal (groupCoverProj H) (basepoint H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) (reduction θ) =
    liftTerminal (groupCoverProj H) (basepoint H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) θ
⊢ [[reduction θ]] ∈ H
Theorem: Graph.SubgroupCover.imageInSubgroup
Proof state before:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
term_eqn :
  liftTerminal (groupCoverProj H) (basepoint H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) (reduction θ) =
    liftTerminal (groupCoverProj H) (basepoint H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) θ
⊢ [[reduction θ]] ∈ H
Tactic:
rw [liftTerminal_of_proj (groupCoverProj H)  η] at term_eqn
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
term_eqn :
  liftTerminal (groupCoverProj H) (basepoint H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) (reduction θ) =
    basepoint H
⊢ [[reduction θ]] ∈ H
Theorem: Graph.SubgroupCover.imageInSubgroup
Proof state before:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
term_eqn :
  liftTerminal (groupCoverProj H) (basepoint H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) (reduction θ) =
    basepoint H
⊢ [[reduction θ]] ∈ H
Tactic:
rw [reduced_liftTerminal_factor' H (reduction θ)
  (by apply reduction_reduced)] at term_eqn
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
term_eqn : ⟦{ τ := x₀, p := reduction θ, is_reduced := (_ : reduced (reduction θ)) }⟧ = basepoint H
⊢ [[reduction θ]] ∈ H
Theorem: Graph.SubgroupCover.imageInSubgroup
Proof state before:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
term_eqn : ⟦{ τ := x₀, p := reduction θ, is_reduced := (_ : reduced (reduction θ)) }⟧ = basepoint H
⊢ [[reduction θ]] ∈ H
Tactic:
simp only [basepoint, UniversalCover.basepoint] at term_eqn
Proof state after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
term_eqn :
  ⟦{ τ := x₀, p := reduction (EdgePath.map η (groupCoverProj H)), is_reduced := (_ : reduced (reduction θ)) }⟧ =
    ⟦{ τ := x₀, p := nil x₀, is_reduced := (_ : reduced (nil x₀)) }⟧
⊢ [[reduction θ]] ∈ H