internlm/Lean-Github huggingface dataset:
Theorem: ReflTransGen.to_finitelyManySteps
Proof state before:
case h.right
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
i : Fin (m + 1)
⊢ r ((a ::ᵥ zs).get i.castSucc) (zs.get i)
Tactic:
induction i using Fin.induction
Proof state after:
case h.right.zero
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ r ((a ::ᵥ zs).get (Fin.castSucc 0)) (zs.get 0)

case h.right.succ
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
i✝ : Fin m
a✝ : r ((a ::ᵥ zs).get i✝.castSucc.castSucc) (zs.get i✝.castSucc)
⊢ r ((a ::ᵥ zs).get i✝.succ.castSucc) (zs.get i✝.succ)
Theorem: ReflTransGen.to_finitelyManySteps
Proof state before:
case h.right.zero
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
⊢ r ((a ::ᵥ zs).get (Fin.castSucc 0)) (zs.get 0)

case h.right.succ
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
i✝ : Fin m
a✝ : r ((a ::ᵥ zs).get i✝.castSucc.castSucc) (zs.get i✝.castSucc)
⊢ r ((a ::ᵥ zs).get i✝.succ.castSucc) (zs.get i✝.succ)
Tactic:
all_goals aesop
Proof state after:
no goals
Theorem: ReflTransGen.to_finitelyManySteps
Proof state before:
case h.right.succ
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_rS_z : Relation.ReflTransGen r b z
m : ℕ
zs : Vector α m.succ
b_is_head_zs : b = zs.head
z_is_last_zs : z = zs.last
zs_steps : ∀ (i : Fin m), r (zs.get i.castSucc) (zs.get i.succ)
i✝ : Fin m
a✝ : r ((a ::ᵥ zs).get i✝.castSucc.castSucc) (zs.get i✝.castSucc)
⊢ r ((a ::ᵥ zs).get i✝.succ.castSucc) (zs.get i✝.succ)
Tactic:
aesop
Proof state after:
no goals
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
α : Type u_1
r : α → α → Prop
n : ℕ
⊢ ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
Tactic:
induction n
Proof state after:
case zero
α : Type u_1
r : α → α → Prop
⊢ ∀ (x z : α) (ys : Vector α (Nat.succ 0)),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin 0), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z

case succ
α : Type u_1
r : α → α → Prop
n✝ : ℕ
a✝ :
  ∀ (x z : α) (ys : Vector α n✝.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n✝), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
⊢ ∀ (x z : α) (ys : Vector α (n✝ + 1).succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin (n✝ + 1)), r (ys.get i.castSucc) (ys.get i.succ)) →
      Relation.ReflTransGen r x z
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
α : Type u_1
r : α → α → Prop
⊢ ∀ (x z : α) (ys : Vector α (Nat.succ 0)),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin 0), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
Tactic:
case zero =>
  rintro x z ys ⟨x_is_head, z_is_last, _⟩
  have : x = z := by
    subst_eqs
    simp_all [Vector.head, Vector.last, Fin.last]
  rw [this]
Proof state after:
no goals
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
α : Type u_1
r : α → α → Prop
⊢ ∀ (x z : α) (ys : Vector α (Nat.succ 0)),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin 0), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
Tactic:
rintro x z ys ⟨x_is_head, z_is_last, _⟩
Proof state after:
case intro.intro
α : Type u_1
r : α → α → Prop
x z : α
ys : Vector α (Nat.succ 0)
x_is_head : x = ys.head
z_is_last : z = ys.last
right✝ : ∀ (i : Fin 0), r (ys.get i.castSucc) (ys.get i.succ)
⊢ Relation.ReflTransGen r x z
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case intro.intro
α : Type u_1
r : α → α → Prop
x z : α
ys : Vector α (Nat.succ 0)
x_is_head : x = ys.head
z_is_last : z = ys.last
right✝ : ∀ (i : Fin 0), r (ys.get i.castSucc) (ys.get i.succ)
⊢ Relation.ReflTransGen r x z
Tactic:
have : x = z := by
  subst_eqs
  simp_all [Vector.head, Vector.last, Fin.last]
Proof state after:
case intro.intro
α : Type u_1
r : α → α → Prop
x z : α
ys : Vector α (Nat.succ 0)
x_is_head : x = ys.head
z_is_last : z = ys.last
right✝ : ∀ (i : Fin 0), r (ys.get i.castSucc) (ys.get i.succ)
this : x = z
⊢ Relation.ReflTransGen r x z
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case intro.intro
α : Type u_1
r : α → α → Prop
x z : α
ys : Vector α (Nat.succ 0)
x_is_head : x = ys.head
z_is_last : z = ys.last
right✝ : ∀ (i : Fin 0), r (ys.get i.castSucc) (ys.get i.succ)
this : x = z
⊢ Relation.ReflTransGen r x z
Tactic:
rw [this]
Proof state after:
no goals
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
α : Type u_1
r : α → α → Prop
x z : α
ys : Vector α (Nat.succ 0)
x_is_head : x = ys.head
z_is_last : z = ys.last
right✝ : ∀ (i : Fin 0), r (ys.get i.castSucc) (ys.get i.succ)
⊢ x = z
Tactic:
subst_eqs
Proof state after:
case refl.refl
α : Type u_1
r : α → α → Prop
ys : Vector α (Nat.succ 0)
right✝ : ∀ (i : Fin 0), r (ys.get i.castSucc) (ys.get i.succ)
⊢ ys.head = ys.last
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case refl.refl
α : Type u_1
r : α → α → Prop
ys : Vector α (Nat.succ 0)
right✝ : ∀ (i : Fin 0), r (ys.get i.castSucc) (ys.get i.succ)
⊢ ys.head = ys.last
Tactic:
simp_all [Vector.head, Vector.last, Fin.last]
Proof state after:
no goals
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
⊢ ∀ (x z : α) (ys : Vector α (n + 1).succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)) →
      Relation.ReflTransGen r x z
Tactic:
rintro x z ys ⟨x_is_head, z_is_last, steprel⟩
Proof state after:
case intro.intro
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
⊢ Relation.ReflTransGen r x z
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case intro.intro
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
⊢ Relation.ReflTransGen r x z
Tactic:
let y := ys.tail.head
Proof state after:
case intro.intro
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ Relation.ReflTransGen r x z
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case intro.intro
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ Relation.ReflTransGen r x z
Tactic:
rw [Relation.ReflTransGen.cases_head_iff]
Proof state after:
case intro.intro
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ x = z ∨ ∃ c, r x c ∧ Relation.ReflTransGen r c z
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case intro.intro
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ x = z ∨ ∃ c, r x c ∧ Relation.ReflTransGen r c z
Tactic:
right
Proof state after:
case intro.intro.h
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ ∃ c, r x c ∧ Relation.ReflTransGen r c z
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case intro.intro.h
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ ∃ c, r x c ∧ Relation.ReflTransGen r c z
Tactic:
use y
Proof state after:
case h
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ r x y ∧ Relation.ReflTransGen r y z
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ r x y ∧ Relation.ReflTransGen r y z
Tactic:
constructor
Proof state after:
case h.left
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ r x y

case h.right
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ Relation.ReflTransGen r y z
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h.left
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ r x y
Tactic:
specialize steprel 0
Proof state after:
case h.left
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
y : α := ys.tail.head
steprel : r (ys.get (Fin.castSucc 0)) (ys.get (Fin.succ 0))
⊢ r x y
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h.left
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
y : α := ys.tail.head
steprel : r (ys.get (Fin.castSucc 0)) (ys.get (Fin.succ 0))
⊢ r x y
Tactic:
simp only [Fin.castSucc_zero, Vector.get_zero, Fin.succ_zero_eq_one] at steprel
Proof state after:
case h.left
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
y : α := ys.tail.head
steprel : r ys.head (ys.get 1)
⊢ r x y
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h.left
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
y : α := ys.tail.head
steprel : r ys.head (ys.get 1)
⊢ r x y
Tactic:
rw [← x_is_head] at steprel
Proof state after:
case h.left
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
y : α := ys.tail.head
steprel : r x (ys.get 1)
⊢ r x y
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h.left
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
y : α := ys.tail.head
steprel : r x (ys.get 1)
⊢ r x y
Tactic:
convert steprel
Proof state after:
case h.e'_2
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
y : α := ys.tail.head
steprel : r x (ys.get 1)
⊢ y = ys.get 1
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h.e'_2
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
y : α := ys.tail.head
steprel : r x (ys.get 1)
⊢ y = ys.get 1
Tactic:
cases ys using Vector.inductionOn
Proof state after:
case h.e'_2.h_cons
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z x✝ : α
w✝ : Vector α (n + 1)
x_is_head : x = (x✝ ::ᵥ w✝).head
z_is_last : z = (x✝ ::ᵥ w✝).last
y : α := (x✝ ::ᵥ w✝).tail.head
steprel : r x ((x✝ ::ᵥ w✝).get 1)
a✝ : (n + 1).succ = n + 1 → HEq (x✝ ::ᵥ w✝) w✝ → y = (x✝ ::ᵥ w✝).get 1
⊢ y = (x✝ ::ᵥ w✝).get 1
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z y✝ : α
ys : Vector α (n + 1)
x_is_head : x = (y✝ ::ᵥ ys).head
z_is_last : z = (y✝ ::ᵥ ys).last
y : α := (y✝ ::ᵥ ys).tail.head
steprel : r x ((y✝ ::ᵥ ys).get 1)
hyp : (n + 1).succ = n + 1 → HEq (y✝ ::ᵥ ys) ys → y = (y✝ ::ᵥ ys).get 1
⊢ y = (y✝ ::ᵥ ys).get 1
Tactic:
case h_cons y ys hyp =>
  cases ys using Vector.inductionOn
  rfl
Proof state after:
no goals
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z y✝ : α
ys : Vector α (n + 1)
x_is_head : x = (y✝ ::ᵥ ys).head
z_is_last : z = (y✝ ::ᵥ ys).last
y : α := (y✝ ::ᵥ ys).tail.head
steprel : r x ((y✝ ::ᵥ ys).get 1)
hyp : (n + 1).succ = n + 1 → HEq (y✝ ::ᵥ ys) ys → y = (y✝ ::ᵥ ys).get 1
⊢ y = (y✝ ::ᵥ ys).get 1
Tactic:
cases ys using Vector.inductionOn
Proof state after:
case h_cons
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z y✝ x✝ : α
w✝ : Vector α n
x_is_head : x = (y✝ ::ᵥ x✝ ::ᵥ w✝).head
z_is_last : z = (y✝ ::ᵥ x✝ ::ᵥ w✝).last
y : α := (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.head
steprel : r x ((y✝ ::ᵥ x✝ ::ᵥ w✝).get 1)
hyp : (n + 1).succ = n + 1 → HEq (y✝ ::ᵥ x✝ ::ᵥ w✝) (x✝ ::ᵥ w✝) → y = (y✝ ::ᵥ x✝ ::ᵥ w✝).get 1
a✝ : n + 1 = n → HEq (x✝ ::ᵥ w✝) w✝ → y = (y✝ ::ᵥ x✝ ::ᵥ w✝).get 1
⊢ y = (y✝ ::ᵥ x✝ ::ᵥ w✝).get 1
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h_cons
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z y✝ x✝ : α
w✝ : Vector α n
x_is_head : x = (y✝ ::ᵥ x✝ ::ᵥ w✝).head
z_is_last : z = (y✝ ::ᵥ x✝ ::ᵥ w✝).last
y : α := (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.head
steprel : r x ((y✝ ::ᵥ x✝ ::ᵥ w✝).get 1)
hyp : (n + 1).succ = n + 1 → HEq (y✝ ::ᵥ x✝ ::ᵥ w✝) (x✝ ::ᵥ w✝) → y = (y✝ ::ᵥ x✝ ::ᵥ w✝).get 1
a✝ : n + 1 = n → HEq (x✝ ::ᵥ w✝) w✝ → y = (y✝ ::ᵥ x✝ ::ᵥ w✝).get 1
⊢ y = (y✝ ::ᵥ x✝ ::ᵥ w✝).get 1
Tactic:
rfl
Proof state after:
no goals
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h.right
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ Relation.ReflTransGen r y z
Tactic:
apply IH y z ys.tail
Proof state after:
case h.right
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ y = ys.tail.head ∧ z = ys.tail.last ∧ ∀ (i : Fin n), r (ys.tail.get i.castSucc) (ys.tail.get i.succ)
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h.right
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ y = ys.tail.head ∧ z = ys.tail.last ∧ ∀ (i : Fin n), r (ys.tail.get i.castSucc) (ys.tail.get i.succ)
Tactic:
simp only [Vector.get_tail_succ, true_and]
Proof state after:
case h.right
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ z = ys.tail.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc.succ) (ys.get i.succ.succ)
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h.right
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ z = ys.tail.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc.succ) (ys.get i.succ.succ)
Tactic:
constructor
Proof state after:
case h.right.left
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ z = ys.tail.last

case h.right.right
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ ∀ (i : Fin n), r (ys.get i.castSucc.succ) (ys.get i.succ.succ)
Theorem: ReflTransGen.from_finitelyManySteps
Proof state before:
case h.right.left
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ z = ys.tail.last
Tactic:
have sameLast : ys.tail.last = ys.last := by
  cases ys using Vector.inductionOn
  case h_cons y ys hyp =>
    cases ys using Vector.inductionOn
    rfl
Proof state after:
case h.right.left
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
sameLast : ys.tail.last = ys.last
⊢ z = ys.tail.last