internlm/Lean-Github huggingface dataset:
Theorem: Graph.SubgroupCover.range_proj
Proof state before:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
⊢ (∃ x_1,
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          x_1 =
        x) ↔
    x ∈ H
Tactic:
let l := proj_image H x
Proof state after:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
⊢ (∃ x_1,
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          x_1 =
        x) ↔
    x ∈ H
Theorem: Graph.SubgroupCover.range_proj
Proof state before:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
⊢ (∃ x_1,
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          x_1 =
        x) ↔
    x ∈ H
Tactic:
apply Iff.intro
Proof state after:
case h.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
⊢ (∃ x_1,
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          x_1 =
        x) →
    x ∈ H

case h.mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
⊢ x ∈ H →
    ∃ x_1,
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          x_1 =
        x
Theorem: Graph.SubgroupCover.range_proj
Proof state before:
case h.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
⊢ (∃ x_1,
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          x_1 =
        x) →
    x ∈ H
Tactic:
intro ⟨h, heq⟩
Proof state after:
case h.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
h : π₁ (groupCover H) (basepoint H)
heq :
  (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h =
    x
⊢ x ∈ H
Theorem: Graph.SubgroupCover.range_proj
Proof state before:
case h.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
h : π₁ (groupCover H) (basepoint H)
heq :
  (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h =
    x
⊢ x ∈ H
Tactic:
apply l.2
Proof state after:
case h.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
h : π₁ (groupCover H) (basepoint H)
heq :
  (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h =
    x
⊢ ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'
Theorem: Graph.SubgroupCover.range_proj
Proof state before:
case h.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
h : π₁ (groupCover H) (basepoint H)
heq :
  (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h =
    x
⊢ ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'
Tactic:
use h
Proof state after:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
h : π₁ (groupCover H) (basepoint H)
heq :
  (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h =
    x
⊢ x =
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h
Theorem: Graph.SubgroupCover.range_proj
Proof state before:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
h : π₁ (groupCover H) (basepoint H)
heq :
  (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h =
    x
⊢ x =
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h
Tactic:
rw [heq]
Proof state after:
no goals
Theorem: Graph.SubgroupCover.range_proj
Proof state before:
case h.mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
⊢ x ∈ H →
    ∃ x_1,
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          x_1 =
        x
Tactic:
intro g
Proof state after:
case h.mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
g : x ∈ H
⊢ ∃ x_1,
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        x_1 =
      x
Theorem: Graph.SubgroupCover.range_proj
Proof state before:
case h.mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
g : x ∈ H
⊢ ∃ x_1,
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        x_1 =
      x
Tactic:
let ⟨h, heq⟩  := l.1 g
Proof state after:
case h.mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
g : x ∈ H
h : π₁ (groupCover H) (basepoint H)
heq :
  x =
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h
⊢ ∃ x_1,
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        x_1 =
      x
Theorem: Graph.SubgroupCover.range_proj
Proof state before:
case h.mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
g : x ∈ H
h : π₁ (groupCover H) (basepoint H)
heq :
  x =
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h
⊢ ∃ x_1,
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        x_1 =
      x
Tactic:
use h
Proof state after:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
g : x ∈ H
h : π₁ (groupCover H) (basepoint H)
heq :
  x =
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h
⊢ (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h =
    x
Theorem: Graph.SubgroupCover.range_proj
Proof state before:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x : π₁ G x₀
l : x ∈ H ↔
  ∃ h',
    x =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h' :=
  proj_image H x
g : x ∈ H
h : π₁ (groupCover H) (basepoint H)
heq :
  x =
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h
⊢ (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h =
    x
Tactic:
rw [heq]
Proof state after:
no goals
Theorem: Graph.SubgroupCover.group_of_cover_is_subgroup
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₀)
⊢ π₁ (groupCover H) (basepoint H) ≃* ↥H
Tactic:
let hf :=
  cover_π₁injective (groupCoverProj H) (basepoint H) x₀ rfl
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₀)
hf : Function.Injective
  ⇑(Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) :=
  cover_π₁injective (groupCoverProj H) (basepoint H) x₀ rfl
⊢ π₁ (groupCover H) (basepoint H) ≃* ↥H
Theorem: Graph.SubgroupCover.group_of_cover_is_subgroup
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₀)
hf : Function.Injective
  ⇑(Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) :=
  cover_π₁injective (groupCoverProj H) (basepoint H) x₀ rfl
⊢ π₁ (groupCover H) (basepoint H) ≃* ↥H
Tactic:
let lem := MonoidHom.ofInjective hf
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₀)
hf : Function.Injective
  ⇑(Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) :=
  cover_π₁injective (groupCoverProj H) (basepoint H) x₀ rfl
lem : π₁ (groupCover H) (basepoint H) ≃*
  ↥(MonoidHom.range
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))) :=
  MonoidHom.ofInjective hf
⊢ π₁ (groupCover H) (basepoint H) ≃* ↥H
Theorem: Graph.SubgroupCover.group_of_cover_is_subgroup
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₀)
hf : Function.Injective
  ⇑(Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) :=
  cover_π₁injective (groupCoverProj H) (basepoint H) x₀ rfl
lem : π₁ (groupCover H) (basepoint H) ≃*
  ↥(MonoidHom.range
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))) :=
  MonoidHom.ofInjective hf
⊢ π₁ (groupCover H) (basepoint H) ≃* ↥H
Tactic:
apply MulEquiv.trans lem
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₀)
hf : Function.Injective
  ⇑(Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) :=
  cover_π₁injective (groupCoverProj H) (basepoint H) x₀ rfl
lem : π₁ (groupCover H) (basepoint H) ≃*
  ↥(MonoidHom.range
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))) :=
  MonoidHom.ofInjective hf
⊢ ↥(MonoidHom.range
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))) ≃*
    ↥H
Theorem: Graph.SubgroupCover.group_of_cover_is_subgroup
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₀)
hf : Function.Injective
  ⇑(Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) :=
  cover_π₁injective (groupCoverProj H) (basepoint H) x₀ rfl
lem : π₁ (groupCover H) (basepoint H) ≃*
  ↥(MonoidHom.range
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))) :=
  MonoidHom.ofInjective hf
⊢ ↥(MonoidHom.range
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))) ≃*
    ↥H
Tactic:
rw [range_proj]
Proof state after:
no goals
Theorem: self_inv_of_squares_id
Proof state before:
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x * x = 1) → ∀ (x : G), x⁻¹ = x
Tactic:
intro h
Proof state after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
⊢ ∀ (x : G), x⁻¹ = x
Theorem: self_inv_of_squares_id
Proof state before:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
⊢ ∀ (x : G), x⁻¹ = x
Tactic:
intro x
Proof state after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x : G
⊢ x⁻¹ = x
Theorem: self_inv_of_squares_id
Proof state before:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x : G
⊢ x⁻¹ = x
Tactic:
apply inv_eq_of_mul_eq_one_right
Proof state after:
case a
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x : G
⊢ x * x = 1
Theorem: self_inv_of_squares_id
Proof state before:
case a
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x : G
⊢ x * x = 1
Tactic:
apply h
Proof state after:
no goals
Theorem: commutative_of_squares_id
Proof state before:
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x * x = 1) → ∀ (x y : G), x * y = y * x
Tactic:
intro h
Proof state after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
⊢ ∀ (x y : G), x * y = y * x
Theorem: commutative_of_squares_id
Proof state before:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
⊢ ∀ (x y : G), x * y = y * x
Tactic:
intro x y
Proof state after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
⊢ x * y = y * x
Theorem: commutative_of_squares_id
Proof state before:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
⊢ x * y = y * x
Tactic:
have rel_xy := self_inv_of_squares_id h (y * x)
Proof state after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
rel_xy : (y * x)⁻¹ = y * x
⊢ x * y = y * x
Theorem: commutative_of_squares_id
Proof state before:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
rel_xy : (y * x)⁻¹ = y * x
⊢ x * y = y * x
Tactic:
simp only [mul_inv_rev] at rel_xy
Proof state after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
rel_xy : x⁻¹ * y⁻¹ = y * x
⊢ x * y = y * x
Theorem: commutative_of_squares_id
Proof state before:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
rel_xy : x⁻¹ * y⁻¹ = y * x
⊢ x * y = y * x
Tactic:
simp only [self_inv_of_squares_id h] at rel_xy
Proof state after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
rel_xy : x * y = y * x
⊢ x * y = y * x
Theorem: commutative_of_squares_id
Proof state before:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
rel_xy : x * y = y * x
⊢ x * y = y * x
Tactic:
assumption
Proof state after:
no goals
Theorem: self_inv_of_squares_id
Proof state before:
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x * x = 1) → ∀ (x : G), x⁻¹ = x
Tactic:
intro h x
Proof state after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x : G
⊢ x⁻¹ = x
Theorem: commutative_of_squares_id
Proof state before:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
rel_xy : (y * x)⁻¹ = y * x
⊢ x * y = y * x
Tactic:
simp at rel_xy
Proof state after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
rel_xy : x⁻¹ * y⁻¹ = y * x
⊢ x * y = y * x
Theorem: commutative_of_squares_id
Proof state before:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
rel_xy : x⁻¹ * y⁻¹ = y * x
⊢ x * y = y * x
Tactic:
simp [self_inv_of_squares_id h] at rel_xy
Proof state after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
rel_xy : x * y = y * x
⊢ x * y = y * x
Theorem: smallest_mem
Proof state before:
case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
lem : min head (smallest tail h) = smallest tail h
⊢ smallest tail h ∈ tail
Tactic:
exact smallest_mem tail h
Proof state after:
no goals
Theorem: ConcatenationTheory.TC3Lang.trivialStarts
Proof state before:
τ : Type
inst✝ : TC3Lang τ
x y : τ
⊢ x ⊑ₛ x ⌢ y
Tactic:
exists y
Proof state after:
no goals
Theorem: ConcatenationTheory.TC3Lang.trivialEnds
Proof state before:
τ : Type
inst✝ : TC3Lang τ
x y : τ
⊢ x ⊑ₑ y ⌢ x
Tactic:
exists y
Proof state after:
no goals
Theorem: Reactor.mem_ids_iff
Proof state before:
α : Type
cpt : Component
inst✝¹ : Hierarchical α
inst✝ : Finite α
rtr : α
i : Component.idType cpt
⊢ i ∈ Finite.ids rtr cpt ↔ ∃ o, rtr[cpt][i] = some o
Tactic:
simp [Finite.ids, ←Partial.mem_def, Partial.mem_iff]
Proof state after:
no goals
Theorem: Execution.Step.Exec.applied_rtr_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ (applied e).rtr = s₂.rtr
Tactic:
cases e
Proof state after:
case mk
α : Type
inst✝ : Hierarchical α
s₁ : State α
rcn✝ : ID
s₂✝ : State α
a✝² : Allows s₁ rcn✝
a✝¹ : Triggers s₁ rcn✝
a✝ : s₁ -[output s₁ rcn✝]→ s₂✝
⊢ (applied (mk a✝² a✝¹ a✝)).rtr = (record s₂✝ rcn✝).rtr
Theorem: Execution.Step.Exec.applied_rtr_eq
Proof state before:
case mk
α : Type
inst✝ : Hierarchical α
s₁ : State α
rcn✝ : ID
s₂✝ : State α
a✝² : Allows s₁ rcn✝
a✝¹ : Triggers s₁ rcn✝
a✝ : s₁ -[output s₁ rcn✝]→ s₂✝
⊢ (applied (mk a✝² a✝¹ a✝)).rtr = (record s₂✝ rcn✝).rtr
Tactic:
simp [applied, record_preserves_rtr]
Proof state after:
no goals
Theorem: Execution.Step.Exec.preserves_tag
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ s₁.tag = s₂.tag
Tactic:
simp [e.dst_eq, State.record_preserves_tag, e.apply.preserves_tag]
Proof state after:
no goals
Theorem: Execution.Step.Exec.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ s₁.rtr ≈ s₂.rtr
Tactic:
simp [e.dst_eq, State.record_preserves_rtr, e.apply.equiv]
Proof state after:
no goals
Theorem: Execution.Step.Exec.progress_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ s₂.progress = Set.insert (rcn e) s₁.progress
Tactic:
simp [e.dst_eq, State.record_progress_eq, e.apply.preserves_progress]
Proof state after:
no goals
Theorem: Execution.Step.Exec.indep_allows_iff
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ rcn e
⊢ Allows s₁ i ↔ Allows s₂ i
Tactic:
have a := e.apply
Proof state after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ rcn e
a : s₁ -[output s₁ (rcn e)]→ (applied e)
⊢ Allows s₁ i ↔ Allows s₂ i
Theorem: Execution.Step.Exec.indep_allows_iff
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ rcn e
a : s₁ -[output s₁ (rcn e)]→ (applied e)
⊢ Allows s₁ i ↔ Allows s₂ i
Tactic:
simp [e.dst_eq, ←Allows.iff_record_indep (a.preserves_independent hi).symm, a.allows_iff]
Proof state after:
no goals
Theorem: Execution.Step.Exec.unprocessed_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ unprocessed s₂ = unprocessed s₁ \ {rcn e}
Tactic:
ext i
Proof state after:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
⊢ i ∈ unprocessed s₂ ↔ i ∈ unprocessed s₁ \ {rcn e}