Theorem: Array.recPush_push (Extra/Array.lean)

State before:
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
⊢ recPush empty push (xs.push x) = push xs x (recPush empty push xs)
Tactic:
let _ : Inhabited α := ⟨(xs.push x)[0]⟩
State after:
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ recPush empty push (xs.push x) = push xs x (recPush empty push xs)

State before:
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ recPush empty push (xs.push x) = push xs x (recPush empty push xs)
Tactic:
rw [recPush]
State after:
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ recPush.aux empty push (xs.push x) (xs.push x).size ⋯ = push xs x (recPush empty push xs)

State before:
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ recPush.aux empty push (xs.push x) (xs.push x).size ⋯ = push xs x (recPush empty push xs)
Tactic:
trans (recPush.aux empty push (xs.push x) (xs.size + 1) (size_push xs x))
State after:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ recPush.aux empty push (xs.push x) (xs.push x).size ⋯ = recPush.aux empty push (xs.push x) (xs.size + 1) ⋯

case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ recPush.aux empty push (xs.push x) (xs.size + 1) ⋯ = push xs x (recPush empty push xs)

State before:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ recPush.aux empty push (xs.push x) (xs.push x).size ⋯ = recPush.aux empty push (xs.push x) (xs.size + 1) ⋯
Tactic:
congr
State after:
case a.e_n
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (xs.push x).size = xs.size + 1

State before:
case a.e_n
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (xs.push x).size = xs.size + 1
Tactic:
exact size_push ..
State after:
no goals

State before:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ recPush.aux empty push (xs.push x) (xs.size + 1) ⋯ = push xs x (recPush empty push xs)
Tactic:
rw [recPush.aux]
State after:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (let_fun this := ⋯;
    let_fun x_1 := { default := (xs.push x)[0] };
    ⋯ ▸ push (xs.push x).pop (xs.push x).back (recPush.aux empty push (xs.push x).pop xs.size ⋯)) =
    push xs x (recPush empty push xs)

State before:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (let_fun this := ⋯;
    let_fun x_1 := { default := (xs.push x)[0] };
    ⋯ ▸ push (xs.push x).pop (xs.push x).back (recPush.aux empty push (xs.push x).pop xs.size ⋯)) =
    push xs x (recPush empty push xs)
Tactic:
simp
State after:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ ⋯ ▸ push (xs.push x).pop (xs.push x).back (recPush.aux empty push (xs.push x).pop xs.size ⋯) =
    push xs x (recPush empty push xs)

State before:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ ⋯ ▸ push (xs.push x).pop (xs.push x).back (recPush.aux empty push (xs.push x).pop xs.size ⋯) =
    push xs x (recPush empty push xs)
Tactic:
elim_cast
State after:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ HEq (push (xs.push x).pop (xs.push x).back (recPush.aux empty push (xs.push x).pop xs.size ⋯))
    (push xs x (recPush empty push xs))

State before:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ HEq (push (xs.push x).pop (xs.push x).back (recPush.aux empty push (xs.push x).pop xs.size ⋯))
    (push xs x (recPush empty push xs))
Tactic:
congr
State after:
case a.e_1
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (xs.push x).pop = xs

case a.e_2
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (xs.push x).back = x

case a.e_3.e_5.h
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (xs.push x).pop = xs

case a.e_3.e_7
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ HEq ⋯ ⋯

State before:
case a.e_1
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (xs.push x).pop = xs
Tactic:
exact pop_push ..
State after:
no goals

State before:
case a.e_2
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (xs.push x).back = x
Tactic:
exact back_push ..
State after:
no goals

State before:
case a.e_3.e_5.h
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (xs.push x).pop = xs
Tactic:
exact pop_push ..
State after:
no goals

State before:
case a.e_3.e_7
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ HEq ⋯ ⋯
Tactic:
exact proof_irrel_heq ..
State after:
no goals