Theorem: ReflTransGen.from_finitelyManySteps (Pdl/Star.lean)

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
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

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]
State after:
no goals

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, _⟩
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

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]
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

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]
State after:
no goals

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
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

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]
State after:
no goals

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⟩
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

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
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

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]
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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)

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]
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)

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
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)

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
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

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
sameLast : ys.tail.last = ys.last
⊢ z = ys.tail.last
Tactic:
rw [sameLast]
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.last

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
sameLast : ys.tail.last = ys.last
⊢ z = ys.last
Tactic:
exact z_is_last
State after:
no goals

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_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
⊢ ys.tail.last = ys.last
Tactic:
cases ys using Vector.inductionOn
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 x✝ : α
w✝ : Vector α (n + 1)
x_is_head : x = (x✝ ::ᵥ w✝).head
z_is_last : z = (x✝ ::ᵥ w✝).last
steprel : ∀ (i : Fin (n + 1)), r ((x✝ ::ᵥ w✝).get i.castSucc) ((x✝ ::ᵥ w✝).get i.succ)
y : α := (x✝ ::ᵥ w✝).tail.head
a✝ : (n + 1).succ = n + 1 → HEq (x✝ ::ᵥ w✝) w✝ → (x✝ ::ᵥ w✝).tail.last = (x✝ ::ᵥ w✝).last
⊢ (x✝ ::ᵥ w✝).tail.last = (x✝ ::ᵥ w✝).last

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
steprel : ∀ (i : Fin (n + 1)), r ((y✝ ::ᵥ ys).get i.castSucc) ((y✝ ::ᵥ ys).get i.succ)
y : α := (y✝ ::ᵥ ys).tail.head
hyp : (n + 1).succ = n + 1 → HEq (y✝ ::ᵥ ys) ys → (y✝ ::ᵥ ys).tail.last = (y✝ ::ᵥ ys).last
⊢ (y✝ ::ᵥ ys).tail.last = (y✝ ::ᵥ ys).last
Tactic:
case h_cons y ys hyp =>
  cases ys using Vector.inductionOn
  rfl
State after:
no goals

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
steprel : ∀ (i : Fin (n + 1)), r ((y✝ ::ᵥ ys).get i.castSucc) ((y✝ ::ᵥ ys).get i.succ)
y : α := (y✝ ::ᵥ ys).tail.head
hyp : (n + 1).succ = n + 1 → HEq (y✝ ::ᵥ ys) ys → (y✝ ::ᵥ ys).tail.last = (y✝ ::ᵥ ys).last
⊢ (y✝ ::ᵥ ys).tail.last = (y✝ ::ᵥ ys).last
Tactic:
cases ys using Vector.inductionOn
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
steprel : ∀ (i : Fin (n + 1)), r ((y✝ ::ᵥ x✝ ::ᵥ w✝).get i.castSucc) ((y✝ ::ᵥ x✝ ::ᵥ w✝).get i.succ)
y : α := (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.head
hyp : (n + 1).succ = n + 1 → HEq (y✝ ::ᵥ x✝ ::ᵥ w✝) (x✝ ::ᵥ w✝) → (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.last = (y✝ ::ᵥ x✝ ::ᵥ w✝).last
a✝ : n + 1 = n → HEq (x✝ ::ᵥ w✝) w✝ → (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.last = (y✝ ::ᵥ x✝ ::ᵥ w✝).last
⊢ (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.last = (y✝ ::ᵥ x✝ ::ᵥ w✝).last

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
steprel : ∀ (i : Fin (n + 1)), r ((y✝ ::ᵥ x✝ ::ᵥ w✝).get i.castSucc) ((y✝ ::ᵥ x✝ ::ᵥ w✝).get i.succ)
y : α := (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.head
hyp : (n + 1).succ = n + 1 → HEq (y✝ ::ᵥ x✝ ::ᵥ w✝) (x✝ ::ᵥ w✝) → (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.last = (y✝ ::ᵥ x✝ ::ᵥ w✝).last
a✝ : n + 1 = n → HEq (x✝ ::ᵥ w✝) w✝ → (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.last = (y✝ ::ᵥ x✝ ::ᵥ w✝).last
⊢ (y✝ ::ᵥ x✝ ::ᵥ w✝).tail.last = (y✝ ::ᵥ x✝ ::ᵥ w✝).last
Tactic:
rfl
State after:
no goals

State before:
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)
Tactic:
intro i
State after:
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)

State before:
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)
Tactic:
specialize steprel i.succ
State after:
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
y : α := ys.tail.head
i : Fin n
steprel : r (ys.get i.succ.castSucc) (ys.get i.succ.succ)
⊢ r (ys.get i.castSucc.succ) (ys.get i.succ.succ)

State before:
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
y : α := ys.tail.head
i : Fin n
steprel : r (ys.get i.succ.castSucc) (ys.get i.succ.succ)
⊢ r (ys.get i.castSucc.succ) (ys.get i.succ.succ)
Tactic:
induction i
State after:
case h.right.right.mk
α : 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
val✝ : ℕ
isLt✝ : val✝ < n
steprel : r (ys.get ⟨val✝, isLt✝⟩.succ.castSucc) (ys.get ⟨val✝, isLt✝⟩.succ.succ)
⊢ r (ys.get ⟨val✝, isLt✝⟩.castSucc.succ) (ys.get ⟨val✝, isLt✝⟩.succ.succ)

State before:
case h.right.right.mk
α : 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
val✝ : ℕ
isLt✝ : val✝ < n
steprel : r (ys.get ⟨val✝, isLt✝⟩.succ.castSucc) (ys.get ⟨val✝, isLt✝⟩.succ.succ)
⊢ r (ys.get ⟨val✝, isLt✝⟩.castSucc.succ) (ys.get ⟨val✝, isLt✝⟩.succ.succ)
Tactic:
all_goals aesop
State after:
no goals

State before:
case h.right.right.mk
α : 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
val✝ : ℕ
isLt✝ : val✝ < n
steprel : r (ys.get ⟨val✝, isLt✝⟩.succ.castSucc) (ys.get ⟨val✝, isLt✝⟩.succ.succ)
⊢ r (ys.get ⟨val✝, isLt✝⟩.castSucc.succ) (ys.get ⟨val✝, isLt✝⟩.succ.succ)
Tactic:
aesop
State after:
no goals