internlm/Lean-Github huggingface dataset:
Theorem: Graph.eq_of_toList_eq
Proof state before:
case cons.cons
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
⊢ cons e₁ p₁' = cons e₂ p₂'
Tactic:
simp [h.2] at ih
Proof state after:
case cons.cons
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ cons e₁ p₁' = cons e₂ p₂'
Theorem: Graph.eq_of_toList_eq
Proof state before:
case cons.cons
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ cons e₁ p₁' = cons e₂ p₂'
Tactic:
apply cons_eq'
Proof state after:
case cons.cons.eq₁
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ e₂.edge = e₁.edge

case cons.cons.eq₃
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ (_ : w✝ = w✝¹) ▸ p₂' = p₁'

case cons.cons.eq₂
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ w✝¹ = w✝
Theorem: Graph.eq_of_toList_eq
Proof state before:
case cons.cons.eq₁
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ e₂.edge = e₁.edge
Tactic:
symm
Proof state after:
case cons.cons.eq₁
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ e₁.edge = e₂.edge
Theorem: Graph.eq_of_toList_eq
Proof state before:
case cons.cons.eq₁
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ e₁.edge = e₂.edge
Tactic:
exact h.1
Proof state after:
no goals
Theorem: Graph.eq_of_toList_eq
Proof state before:
case cons.cons.eq₃
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ (_ : w✝ = w✝¹) ▸ p₂' = p₁'
Tactic:
let step := ih (e2t ▸ p₂')
Proof state after:
case cons.cons.eq₃
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
⊢ (_ : w✝ = w✝¹) ▸ p₂' = p₁'
Theorem: Graph.eq_of_toList_eq
Proof state before:
case cons.cons.eq₃
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
⊢ (_ : w✝ = w✝¹) ▸ p₂' = p₁'
Tactic:
symm
Proof state after:
case cons.cons.eq₃
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
⊢ p₁' = (_ : w✝ = w✝¹) ▸ p₂'
Theorem: Graph.eq_of_toList_eq
Proof state before:
case cons.cons.eq₃
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
⊢ p₁' = (_ : w✝ = w✝¹) ▸ p₂'
Tactic:
have : p₁' = (e2t ▸ p₂')  := by
  apply step
  exact toList_cast_init p₂' (Eq.symm e2t)
Proof state after:
case cons.cons.eq₃
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
this : p₁' = (_ : w✝ = w✝¹) ▸ p₂'
⊢ p₁' = (_ : w✝ = w✝¹) ▸ p₂'
Theorem: Graph.eq_of_toList_eq
Proof state before:
case cons.cons.eq₃
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
this : p₁' = (_ : w✝ = w✝¹) ▸ p₂'
⊢ p₁' = (_ : w✝ = w✝¹) ▸ p₂'
Tactic:
rw [this]
Proof state after:
case cons.cons.eq₂
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ w✝¹ = w✝
Theorem: Graph.eq_of_toList_eq
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
⊢ p₁' = (_ : w✝ = w✝¹) ▸ p₂'
Tactic:
apply step
Proof state after:
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
⊢ toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂')
Theorem: Graph.eq_of_toList_eq
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
⊢ toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂')
Tactic:
exact toList_cast_init p₂' (Eq.symm e2t)
Proof state after:
no goals
Theorem: Graph.eq_of_toList_eq
Proof state before:
case cons.cons.eq₂
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ w✝¹ = w✝
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.terminal_eq_of_toList_eq
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₁ : EdgePath G v₁ w₁
p₂ : EdgePath G v₂ w₂
⊢ toList p₁ = toList p₂ → v₁ = v₂ → w₁ = w₂
Tactic:
induction p₁ with
| nil v₁' =>
  match p₂ with
  | EdgePath.nil v => 
    intro h heq
    rw [nil_toList] at h      
    exact heq
  | EdgePath.cons e₂ p₂  =>
    intro h
    simp [cons_toList, nil_toList] at h
| cons e p₁' ih =>    
  intro h heq
  match p₂ with
  | EdgePath.nil w =>
    simp [cons_toList, nil_toList] at h
  | EdgePath.cons e₂ p₂' =>
    simp [cons_toList] at h
    apply terminal_eq_of_toList_eq p₁' p₂' h.right
    rw [←e₂.term_eq, ←e.term_eq, h.left]
Proof state after:
no goals
Theorem: Graph.terminal_eq_of_toList_eq
Proof state before:
case nil
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' : V
⊢ toList (nil v₁') = toList p₂ → v₁' = v₂ → v₁' = w₂
Tactic:
match p₂ with
| EdgePath.nil v => 
  intro h heq
  rw [nil_toList] at h      
  exact heq
| EdgePath.cons e₂ p₂  =>
  intro h
  simp [cons_toList, nil_toList] at h
Proof state after:
no goals
Theorem: Graph.terminal_eq_of_toList_eq
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u v✝ w : V
e : EdgeBetween G✝ v✝ w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' v : V
⊢ toList (nil v₁') = toList (nil v) → v₁' = v → v₁' = v
Tactic:
intro h heq
Proof state after:
V : Type u
E : Type v
G✝ : Graph V E
u v✝ w : V
e : EdgeBetween G✝ v✝ w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' v : V
h : toList (nil v₁') = toList (nil v)
heq : v₁' = v
⊢ v₁' = v
Theorem: Graph.terminal_eq_of_toList_eq
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u v✝ w : V
e : EdgeBetween G✝ v✝ w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' v : V
h : toList (nil v₁') = toList (nil v)
heq : v₁' = v
⊢ v₁' = v
Tactic:
rw [nil_toList] at h
Proof state after:
V : Type u
E : Type v
G✝ : Graph V E
u v✝ w : V
e : EdgeBetween G✝ v✝ w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' v : V
h : [] = toList (nil v)
heq : v₁' = v
⊢ v₁' = v
Theorem: Graph.terminal_eq_of_toList_eq
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u v✝ w : V
e : EdgeBetween G✝ v✝ w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' v : V
h : [] = toList (nil v)
heq : v₁' = v
⊢ v₁' = v
Tactic:
exact heq
Proof state after:
no goals
Theorem: Graph.terminal_eq_of_toList_eq
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂✝ : EdgePath G v₂✝ w₂✝
v₁' w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂ : EdgePath G w✝ w₂
⊢ toList (nil v₁') = toList (cons e₂ p₂) → v₁' = v₂ → v₁' = w₂
Tactic:
intro h
Proof state after:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂✝ : EdgePath G v₂✝ w₂✝
v₁' w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂ : EdgePath G w✝ w₂
h : toList (nil v₁') = toList (cons e₂ p₂)
⊢ v₁' = v₂ → v₁' = w₂
Theorem: Graph.terminal_eq_of_toList_eq
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂✝ : EdgePath G v₂✝ w₂✝
v₁' w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂ : EdgePath G w✝ w₂
h : toList (nil v₁') = toList (cons e₂ p₂)
⊢ v₁' = v₂ → v₁' = w₂
Tactic:
simp [cons_toList, nil_toList] at h
Proof state after:
no goals
Theorem: Graph.terminal_eq_of_toList_eq
Proof state before:
case cons
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
ih : toList p₁' = toList p₂ → w✝ = v₂ → u✝ = w₂
⊢ toList (cons e p₁') = toList p₂ → v✝ = v₂ → u✝ = w₂
Tactic:
intro h heq
Proof state after:
case cons
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
ih : toList p₁' = toList p₂ → w✝ = v₂ → u✝ = w₂
h : toList (cons e p₁') = toList p₂
heq : v✝ = v₂
⊢ u✝ = w₂
Theorem: Graph.terminal_eq_of_toList_eq
Proof state before:
case cons
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
ih : toList p₁' = toList p₂ → w✝ = v₂ → u✝ = w₂
h : toList (cons e p₁') = toList p₂
heq : v✝ = v₂
⊢ u✝ = w₂
Tactic:
match p₂ with
| EdgePath.nil w =>
  simp [cons_toList, nil_toList] at h
| EdgePath.cons e₂ p₂' =>
  simp [cons_toList] at h
  apply terminal_eq_of_toList_eq p₁' p₂' h.right
  rw [←e₂.term_eq, ←e.term_eq, h.left]
Proof state after:
no goals
Theorem: Graph.terminal_eq_of_toList_eq
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u v w✝¹ : V
e✝ : EdgeBetween G✝ v w✝¹
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
w : V
ih : toList p₁' = toList (nil w) → w✝ = w → u✝ = w
h : toList (cons e p₁') = toList (nil w)
heq : v✝ = w
⊢ u✝ = w
Tactic:
simp [cons_toList, nil_toList] at h
Proof state after:
no goals
Theorem: Graph.terminal_eq_of_toList_eq
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂ : EdgePath G v₂✝ w₂✝
v✝ w✝¹ u✝ : V
e : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂' : EdgePath G w✝ w₂
ih : toList p₁' = toList (cons e₂ p₂') → w✝¹ = v₂ → u✝ = w₂
h : toList (cons e p₁') = toList (cons e₂ p₂')
heq : v✝ = v₂
⊢ u✝ = w₂
Tactic:
simp [cons_toList] at h
Proof state after:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂ : EdgePath G v₂✝ w₂✝
v✝ w✝¹ u✝ : V
e : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂' : EdgePath G w✝ w₂
ih : toList p₁' = toList (cons e₂ p₂') → w✝¹ = v₂ → u✝ = w₂
heq : v✝ = v₂
h : e.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ u✝ = w₂
Theorem: Graph.terminal_eq_of_toList_eq
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂ : EdgePath G v₂✝ w₂✝
v✝ w✝¹ u✝ : V
e : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂' : EdgePath G w✝ w₂
ih : toList p₁' = toList (cons e₂ p₂') → w✝¹ = v₂ → u✝ = w₂
heq : v✝ = v₂
h : e.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ u✝ = w₂
Tactic:
apply terminal_eq_of_toList_eq p₁' p₂' h.right
Proof state after:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂ : EdgePath G v₂✝ w₂✝
v✝ w✝¹ u✝ : V
e : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂' : EdgePath G w✝ w₂
ih : toList p₁' = toList (cons e₂ p₂') → w✝¹ = v₂ → u✝ = w₂
heq : v✝ = v₂
h : e.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ w✝¹ = w✝
Theorem: Graph.terminal_eq_of_toList_eq
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂ : EdgePath G v₂✝ w₂✝
v✝ w✝¹ u✝ : V
e : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂' : EdgePath G w✝ w₂
ih : toList p₁' = toList (cons e₂ p₂') → w✝¹ = v₂ → u✝ = w₂
heq : v✝ = v₂
h : e.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ w✝¹ = w✝
Tactic:
rw [←e₂.term_eq, ←e.term_eq, h.left]
Proof state after:
no goals
Theorem: Graph.PathLift.toFuncV_init
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : CoveringMap G₁ G₂
v₁ : V₁
v₂ w₂ : V₂
h : p.toMorphism.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
lift : PathLift p v₁ v₂ w₂ h e
⊢ Morphism.pathMap p.toMorphism v₁ lift.w₁ lift.path v₂ w₂ h (_ : p.toMorphism.toFuncV lift.w₁ = w₂) = e
Tactic:
apply eq_of_toList_eq
Proof state after:
case a
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : CoveringMap G₁ G₂
v₁ : V₁
v₂ w₂ : V₂
h : p.toMorphism.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
lift : PathLift p v₁ v₂ w₂ h e
⊢ toList (Morphism.pathMap p.toMorphism v₁ lift.w₁ lift.path v₂ w₂ h (_ : p.toMorphism.toFuncV lift.w₁ = w₂)) = toList e
Theorem: Graph.PathLift.toFuncV_init
Proof state before:
case a
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : CoveringMap G₁ G₂
v₁ : V₁
v₂ w₂ : V₂
h : p.toMorphism.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
lift : PathLift p v₁ v₂ w₂ h e
⊢ toList (Morphism.pathMap p.toMorphism v₁ lift.w₁ lift.path v₂ w₂ h (_ : p.toMorphism.toFuncV lift.w₁ = w₂)) = toList e
Tactic:
rw [pathMap_toList, lift.list_pushdown]
Proof state after:
no goals
Theorem: sum_formula
Proof state before:
n : ℕ
⊢ ↑(sum n) = ↑n * (↑n + 1) / 2
Tactic:
induction n with
| zero => rfl
| succ n ih => 
  simp [sum]
  linarith
Proof state after:
no goals
Theorem: sum_formula
Proof state before:
case zero

⊢ ↑(sum Nat.zero) = ↑Nat.zero * (↑Nat.zero + 1) / 2
Tactic:
rfl
Proof state after:
no goals