internlm/Lean-Github huggingface dataset:
Theorem: sum_formula
Proof state before:
case succ
n : ℕ
ih : ↑(sum n) = ↑n * (↑n + 1) / 2
⊢ ↑(sum (Nat.succ n)) = ↑(Nat.succ n) * (↑(Nat.succ n) + 1) / 2
Tactic:
simp [sum]
Proof state after:
case succ
n : ℕ
ih : ↑(sum n) = ↑n * (↑n + 1) / 2
⊢ ↑n + 1 + ↑(sum n) = (↑n + 1) * (↑n + 1 + 1) / 2
Theorem: sum_formula
Proof state before:
case succ
n : ℕ
ih : ↑(sum n) = ↑n * (↑n + 1) / 2
⊢ ↑n + 1 + ↑(sum n) = (↑n + 1) * (↑n + 1 + 1) / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
a b c : ℤ
⊢ (∃ x y, a * x + b * y = c) ↔ ↑(Int.gcd a b) ∣ c
Tactic:
apply Iff.intro
Proof state after:
case mp
a b c : ℤ
⊢ (∃ x y, a * x + b * y = c) → ↑(Int.gcd a b) ∣ c

case mpr
a b c : ℤ
⊢ ↑(Int.gcd a b) ∣ c → ∃ x y, a * x + b * y = c
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
case mp
a b c : ℤ
⊢ (∃ x y, a * x + b * y = c) → ↑(Int.gcd a b) ∣ c
Tactic:
intro ⟨x, y, h⟩
Proof state after:
case mp
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ c
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
case mp
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ c
Tactic:
rw [← h]
Proof state after:
case mp
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a * x + b * y
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
case mp
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a * x + b * y
Tactic:
apply dvd_add
Proof state after:
case mp.h₁
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a * x

case mp.h₂
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ b * y
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
case mp.h₁
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a * x
Tactic:
trans a
Proof state after:
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a

a b c x y : ℤ
h : a * x + b * y = c
⊢ a ∣ a * x
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ a
Tactic:
apply Int.gcd_dvd_left
Proof state after:
no goals
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
a b c x y : ℤ
h : a * x + b * y = c
⊢ a ∣ a * x
Tactic:
apply Int.dvd_mul_right
Proof state after:
no goals
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
case mp.h₂
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ b * y
Tactic:
trans b
Proof state after:
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ b

a b c x y : ℤ
h : a * x + b * y = c
⊢ b ∣ b * y
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
a b c x y : ℤ
h : a * x + b * y = c
⊢ ↑(Int.gcd a b) ∣ b
Tactic:
apply Int.gcd_dvd_right
Proof state after:
no goals
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
a b c x y : ℤ
h : a * x + b * y = c
⊢ b ∣ b * y
Tactic:
apply Int.dvd_mul_right
Proof state after:
no goals
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
case mpr
a b c : ℤ
⊢ ↑(Int.gcd a b) ∣ c → ∃ x y, a * x + b * y = c
Tactic:
intro h
Proof state after:
case mpr
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
⊢ ∃ x y, a * x + b * y = c
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
case mpr
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
⊢ ∃ x y, a * x + b * y = c
Tactic:
let d := c / Int.gcd a b
Proof state after:
case mpr
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
⊢ ∃ x y, a * x + b * y = c
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
case mpr
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
⊢ ∃ x y, a * x + b * y = c
Tactic:
let h' : Int.gcd a b * d = c := by 
  apply Int.mul_ediv_cancel_of_emod_eq_zero
  apply Int.emod_eq_zero_of_dvd
  assumption
Proof state after:
case mpr
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
h' : ↑(Int.gcd a b) * d = c := Int.mul_ediv_cancel_of_emod_eq_zero (Int.emod_eq_zero_of_dvd h)
⊢ ∃ x y, a * x + b * y = c
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
case mpr
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
h' : ↑(Int.gcd a b) * d = c := Int.mul_ediv_cancel_of_emod_eq_zero (Int.emod_eq_zero_of_dvd h)
⊢ ∃ x y, a * x + b * y = c
Tactic:
use d * (Int.gcdA a b), d * (Int.gcdB a b)
Proof state after:
case h
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
h' : ↑(Int.gcd a b) * d = c := Int.mul_ediv_cancel_of_emod_eq_zero (Int.emod_eq_zero_of_dvd h)
⊢ a * (d * Int.gcdA a b) + b * (d * Int.gcdB a b) = c
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
case h
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
h' : ↑(Int.gcd a b) * d = c := Int.mul_ediv_cancel_of_emod_eq_zero (Int.emod_eq_zero_of_dvd h)
⊢ a * (d * Int.gcdA a b) + b * (d * Int.gcdB a b) = c
Tactic:
rw [← h', Int.gcd_eq_gcd_ab]
Proof state after:
case h
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
h' : ↑(Int.gcd a b) * d = c := Int.mul_ediv_cancel_of_emod_eq_zero (Int.emod_eq_zero_of_dvd h)
⊢ a * (d * Int.gcdA a b) + b * (d * Int.gcdB a b) = (a * Int.gcdA a b + b * Int.gcdB a b) * d
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
case h
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
h' : ↑(Int.gcd a b) * d = c := Int.mul_ediv_cancel_of_emod_eq_zero (Int.emod_eq_zero_of_dvd h)
⊢ a * (d * Int.gcdA a b) + b * (d * Int.gcdB a b) = (a * Int.gcdA a b + b * Int.gcdB a b) * d
Tactic:
linarith
Proof state after:
no goals
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
⊢ ↑(Int.gcd a b) * d = c
Tactic:
apply Int.mul_ediv_cancel_of_emod_eq_zero
Proof state after:
case H
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
⊢ c % ↑(Int.gcd a b) = 0
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
case H
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
⊢ c % ↑(Int.gcd a b) = 0
Tactic:
apply Int.emod_eq_zero_of_dvd
Proof state after:
case H.a
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
⊢ ↑(Int.gcd a b) ∣ c
Theorem: eqn_solvable_iff_divides_gcd
Proof state before:
case H.a
a b c : ℤ
h : ↑(Int.gcd a b) ∣ c
d : ℤ := c / ↑(Int.gcd a b)
⊢ ↑(Int.gcd a b) ∣ c
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.SubgroupCover.relH_refl
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
v : EdgePath G x₀ τ
⊢ relH H v v
Tactic:
simp [relH]
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
v : EdgePath G x₀ τ
⊢ CategoryTheory.CategoryStruct.id x₀ ∈ H
Theorem: Graph.SubgroupCover.relH_refl
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
v : EdgePath G x₀ τ
⊢ CategoryTheory.CategoryStruct.id x₀ ∈ H
Tactic:
apply one_mem
Proof state after:
no goals
Theorem: Graph.SubgroupCover.relH_symm
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
v₁ v₂ : EdgePath G x₀ τ
⊢ relH H v₁ v₂ → relH H v₂ v₁
Tactic:
simp [relH]
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
v₁ v₂ : EdgePath G x₀ τ
⊢ [[v₁ ++ reverse v₂]] ∈ H → [[v₂ ++ reverse v₁]] ∈ H
Theorem: Graph.SubgroupCover.relH_symm
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
v₁ v₂ : EdgePath G x₀ τ
⊢ [[v₁ ++ reverse v₂]] ∈ H → [[v₂ ++ reverse v₁]] ∈ H
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₀)
τ : V
v₁ v₂ : EdgePath G x₀ τ
h : [[v₁ ++ reverse v₂]] ∈ H
⊢ [[v₂ ++ reverse v₁]] ∈ H
Theorem: Graph.SubgroupCover.relH_symm
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
v₁ v₂ : EdgePath G x₀ τ
h : [[v₁ ++ reverse v₂]] ∈ H
⊢ [[v₂ ++ reverse v₁]] ∈ H
Tactic:
let h': [[v₁ ++ v₂.reverse]].inv ∈ H := inv_mem 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₀)
τ : V
v₁ v₂ : EdgePath G x₀ τ
h : [[v₁ ++ reverse v₂]] ∈ H
h' : PathClass.inv [[v₁ ++ reverse v₂]] ∈ H := inv_mem h
⊢ [[v₂ ++ reverse v₁]] ∈ H
Theorem: Graph.SubgroupCover.relH_symm
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
v₁ v₂ : EdgePath G x₀ τ
h : [[v₁ ++ reverse v₂]] ∈ H
h' : PathClass.inv [[v₁ ++ reverse v₂]] ∈ H := inv_mem h
⊢ [[v₂ ++ reverse v₁]] ∈ H
Tactic:
rw [inv_equiv_reverse,
  reverse_append,  reverse_reverse] 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₀)
τ : V
v₁ v₂ : EdgePath G x₀ τ
h : [[v₁ ++ reverse v₂]] ∈ H
h' : [[v₂ ++ reverse v₁]] ∈ H
⊢ [[v₂ ++ reverse v₁]] ∈ H
Theorem: Graph.SubgroupCover.relH_symm
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
v₁ v₂ : EdgePath G x₀ τ
h : [[v₁ ++ reverse v₂]] ∈ H
h' : [[v₂ ++ reverse v₁]] ∈ H
⊢ [[v₂ ++ reverse v₁]] ∈ H
Tactic:
exact h'
Proof state after:
no goals
Theorem: Graph.SubgroupCover.relH_trans
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
v₁ v₂ v₃ : EdgePath G x₀ τ
⊢ relH H v₁ v₂ → relH H v₂ v₃ → relH H v₁ v₃
Tactic:
simp [relH]
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
v₁ v₂ v₃ : EdgePath G x₀ τ
⊢ [[v₁ ++ reverse v₂]] ∈ H → [[v₂ ++ reverse v₃]] ∈ H → [[v₁ ++ reverse v₃]] ∈ H
Theorem: Graph.SubgroupCover.relH_trans
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
v₁ v₂ v₃ : EdgePath G x₀ τ
⊢ [[v₁ ++ reverse v₂]] ∈ H → [[v₂ ++ reverse v₃]] ∈ H → [[v₁ ++ reverse v₃]] ∈ H
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₀)
τ : V
v₁ v₂ v₃ : EdgePath G x₀ τ
h₁ : [[v₁ ++ reverse v₂]] ∈ H
h₂ : [[v₂ ++ reverse v₃]] ∈ H
⊢ [[v₁ ++ reverse v₃]] ∈ H
Theorem: Graph.SubgroupCover.relH_trans
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
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₂
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
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
Theorem: Graph.SubgroupCover.relH_trans
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
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₃
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
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
Theorem: Graph.SubgroupCover.relH_trans
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
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₃
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
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
Theorem: Graph.SubgroupCover.relH_trans
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
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₃
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
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
Theorem: Graph.SubgroupCover.relH_trans
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
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₃
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
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
Theorem: Graph.SubgroupCover.relH_trans
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
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]
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
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
Theorem: Graph.SubgroupCover.relH_trans
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
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₃
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₀)
v₁ v₂ : Vert G x₀
⊢ Setoid.r v₁ v₂ → v₁.τ = v₂.τ
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₀)
v₁ v₂ : Vert G x₀
h : Setoid.r v₁ v₂
⊢ v₁.τ = v₂.τ
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₀)
v₁ v₂ : Vert G x₀
h : Setoid.r v₁ v₂
⊢ v₁.τ = v₂.τ
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₀)
v₁ v₂ : Vert G x₀
h :
  if h : v₁.τ = v₂.τ then
    Eq.rec (motive := fun a t => v₂.τ = a → HEq (_ : v₁.τ = v₂.τ) t → Prop)
      (fun h_1 =>
        Eq.rec (motive := fun x x_1 =>
          (v₂ : EdgePath G x₀ x) → reduced v₂ → (c : v₁.τ = x) → HEq c (_ : v₁.τ = v₁.τ) → Prop)
          (fun v₂ is_reduced c h => relH H v₁.p v₂) (_ : v₁.τ = v₂.τ) v₂.p (_ : reduced v₂.p) (_ : v₁.τ = v₂.τ))
      (_ : v₁.τ = v₂.τ) (_ : v₂.τ = v₂.τ) (_ : HEq (_ : v₁.τ = v₂.τ) (_ : v₁.τ = v₂.τ))
  else False
⊢ v₁.τ = v₂.τ
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₀)
v₁ v₂ : Vert G x₀
h :
  if h : v₁.τ = v₂.τ then
    Eq.rec (motive := fun a t => v₂.τ = a → HEq (_ : v₁.τ = v₂.τ) t → Prop)
      (fun h_1 =>
        Eq.rec (motive := fun x x_1 =>
          (v₂ : EdgePath G x₀ x) → reduced v₂ → (c : v₁.τ = x) → HEq c (_ : v₁.τ = v₁.τ) → Prop)
          (fun v₂ is_reduced c h => relH H v₁.p v₂) (_ : v₁.τ = v₂.τ) v₂.p (_ : reduced v₂.p) (_ : v₁.τ = v₂.τ))
      (_ : v₁.τ = v₂.τ) (_ : v₂.τ = v₂.τ) (_ : HEq (_ : v₁.τ = v₂.τ) (_ : v₁.τ = v₂.τ))
  else False
⊢ v₁.τ = v₂.τ
Tactic:
by_cases c:v₁.τ=v₂.τ <;> 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₀)
v₁ v₂ : Vert G x₀
c : v₁.τ = v₂.τ
h :
  Eq.rec (motive := fun a t => v₂.τ = a → HEq (_ : v₁.τ = v₂.τ) t → Prop)
    (fun h =>
      Eq.rec (motive := fun x x_1 =>
        (v₂ : EdgePath G x₀ x) → reduced v₂ → (c : v₁.τ = x) → HEq c (_ : v₁.τ = v₁.τ) → Prop)
        (fun v₂ is_reduced c h => relH H v₁.p v₂) (_ : v₁.τ = v₂.τ) v₂.p (_ : reduced v₂.p) (_ : v₁.τ = v₂.τ))
    (_ : v₁.τ = v₂.τ) (_ : v₂.τ = v₂.τ) (_ : HEq (_ : v₁.τ = v₂.τ) (_ : v₁.τ = v₂.τ))
⊢ v₁.τ = v₂.τ
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₀)
v₁ v₂ : Vert G x₀
c : v₁.τ = v₂.τ
h :
  Eq.rec (motive := fun a t => v₂.τ = a → HEq (_ : v₁.τ = v₂.τ) t → Prop)
    (fun h =>
      Eq.rec (motive := fun x x_1 =>
        (v₂ : EdgePath G x₀ x) → reduced v₂ → (c : v₁.τ = x) → HEq c (_ : v₁.τ = v₁.τ) → Prop)
        (fun v₂ is_reduced c h => relH H v₁.p v₂) (_ : v₁.τ = v₂.τ) v₂.p (_ : reduced v₂.p) (_ : v₁.τ = v₂.τ))
    (_ : v₁.τ = v₂.τ) (_ : v₂.τ = v₂.τ) (_ : HEq (_ : v₁.τ = v₂.τ) (_ : v₁.τ = v₂.τ))
⊢ v₁.τ = v₂.τ
Tactic:
simp [c]
Proof state after:
no goals
Theorem: Graph.SubgroupCover.path_eq_iff_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
p₁ p₂ : EdgePath G x₀ τ
red₁ : reduced p₁
red₂ : reduced p₂
⊢ Setoid.r { τ := τ, p := p₁, is_reduced := red₁ } { τ := τ, p := p₂, is_reduced := red₂ } ↔ [[p₁ ++ reverse p₂]] ∈ H
Tactic:
simp [Setoid.r, relH]
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₂.τ₁