Theorem: Graph.SubgroupCover.relH_trans (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₁ v₂ v₃ : EdgePath G x₀ τ
⊢ relH H v₁ v₂ → relH H v₂ v₃ → relH H v₁ v₃
Tactic:
simp [relH]
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₁ v₂ v₃ : EdgePath G x₀ τ
⊢ [[v₁ ++ reverse v₂]] ∈ H → [[v₂ ++ reverse v₃]] ∈ H → [[v₁ ++ reverse v₃]] ∈ H

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₁ v₂ v₃ : EdgePath G x₀ τ
⊢ [[v₁ ++ reverse v₂]] ∈ H → [[v₂ ++ reverse v₃]] ∈ H → [[v₁ ++ reverse v₃]] ∈ H
Tactic:
intro h₁ 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₁ v₂ v₃ : EdgePath G x₀ τ
h₁ : [[v₁ ++ reverse v₂]] ∈ H
h₂ : [[v₂ ++ reverse v₃]] ∈ H
⊢ [[v₁ ++ reverse v₃]] ∈ H

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₁ v₂ v₃ : EdgePath G x₀ τ
h₁ : [[v₁ ++ reverse v₂]] ∈ H
h₂ : [[v₂ ++ reverse v₃]] ∈ H
⊢ [[v₁ ++ reverse v₃]] ∈ H
Tactic:
let h₃  := mul_mem h₁ 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₁ v₂ v₃ : EdgePath G x₀ τ
h₁ : [[v₁ ++ reverse v₂]] ∈ H
h₂ : [[v₂ ++ reverse v₃]] ∈ H
h₃ : [[v₁ ++ reverse v₂]] * [[v₂ ++ reverse v₃]] ∈ H := mul_mem h₁ h₂
⊢ [[v₁ ++ reverse v₃]] ∈ H

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₁ v₂ v₃ : EdgePath G x₀ τ
h₁ : [[v₁ ++ reverse v₂]] ∈ H
h₂ : [[v₂ ++ reverse v₃]] ∈ H
h₃ : [[v₁ ++ reverse v₂]] * [[v₂ ++ reverse v₃]] ∈ H := mul_mem h₁ h₂
⊢ [[v₁ ++ reverse v₃]] ∈ H
Tactic:
rw [mul_path_path, append_assoc,
  ← append_assoc v₂.reverse, ← mul_path_path,
  ← mul_path_path] 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₁ v₂ v₃ : EdgePath G x₀ τ
h₁ : [[v₁ ++ reverse v₂]] ∈ H
h₂ : [[v₂ ++ reverse v₃]] ∈ H
h₃ : [[v₁]] * ([[reverse v₂ ++ v₂]] * [[reverse v₃]]) ∈ H
⊢ [[v₁ ++ reverse v₃]] ∈ H

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₁ v₂ v₃ : EdgePath G x₀ τ
h₁ : [[v₁ ++ reverse v₂]] ∈ H
h₂ : [[v₂ ++ reverse v₃]] ∈ H
h₃ : [[v₁]] * ([[reverse v₂ ++ v₂]] * [[reverse v₃]]) ∈ H
⊢ [[v₁ ++ reverse v₃]] ∈ H
Tactic:
simp only [reverse_append_self] 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₁ v₂ v₃ : EdgePath G x₀ τ
h₁ : [[v₁ ++ reverse v₂]] ∈ H
h₂ : [[v₂ ++ reverse v₃]] ∈ H
h₃ : [[v₁]] * ([[nil τ]] * [[reverse v₃]]) ∈ H
⊢ [[v₁ ++ reverse v₃]] ∈ H

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₁ v₂ v₃ : EdgePath G x₀ τ
h₁ : [[v₁ ++ reverse v₂]] ∈ H
h₂ : [[v₂ ++ reverse v₃]] ∈ H
h₃ : [[v₁]] * ([[nil τ]] * [[reverse v₃]]) ∈ H
⊢ [[v₁ ++ reverse v₃]] ∈ H
Tactic:
rw [mul_path_path] 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₁ v₂ v₃ : EdgePath G x₀ τ
h₁ : [[v₁ ++ reverse v₂]] ∈ H
h₂ : [[v₂ ++ reverse v₃]] ∈ H
h₃ : [[v₁]] * [[nil τ ++ reverse v₃]] ∈ H
⊢ [[v₁ ++ reverse v₃]] ∈ H

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₁ v₂ v₃ : EdgePath G x₀ τ
h₁ : [[v₁ ++ reverse v₂]] ∈ H
h₂ : [[v₂ ++ reverse v₃]] ∈ H
h₃ : [[v₁]] * [[nil τ ++ reverse v₃]] ∈ H
⊢ [[v₁ ++ reverse v₃]] ∈ H
Tactic:
simp only [nil_append, reverse_class_eq_inv] 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₁ v₂ v₃ : EdgePath G x₀ τ
h₁ : [[v₁ ++ reverse v₂]] ∈ H
h₂ : [[v₂ ++ reverse v₃]] ∈ H
h₃ : [[v₁]] * PathClass.inv [[v₃]] ∈ H
⊢ [[v₁ ++ reverse v₃]] ∈ H

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₁ v₂ v₃ : EdgePath G x₀ τ
h₁ : [[v₁ ++ reverse v₂]] ∈ H
h₂ : [[v₂ ++ reverse v₃]] ∈ H
h₃ : [[v₁]] * PathClass.inv [[v₃]] ∈ H
⊢ [[v₁ ++ reverse v₃]] ∈ H
Tactic:
rw [← mul_path_path, ← inv_equiv_reverse]
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₁ v₂ v₃ : EdgePath G x₀ τ
h₁ : [[v₁ ++ reverse v₂]] ∈ H
h₂ : [[v₂ ++ reverse v₃]] ∈ H
h₃ : [[v₁]] * PathClass.inv [[v₃]] ∈ H
⊢ [[v₁]] * PathClass.inv [[v₃]] ∈ H

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₁ v₂ v₃ : EdgePath G x₀ τ
h₁ : [[v₁ ++ reverse v₂]] ∈ H
h₂ : [[v₂ ++ reverse v₃]] ∈ H
h₃ : [[v₁]] * PathClass.inv [[v₃]] ∈ H
⊢ [[v₁]] * PathClass.inv [[v₃]] ∈ H
Tactic:
exact h₃
State after:
no goals