α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (n : ℕ) (l₁ l₂ : List α),
    List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
intros f n l₁ l₂
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
len : ℕ
e : length (l₁ ++ l₂) = len
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
generalize e : (l₁ ++ l₂).length = len
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
⊢ ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
len : ℕ
e : length (l₁ ++ l₂) = len
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
revert n l₁ l₂
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂

case succ
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.succ len
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
⊢ ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
induction' len with len ih <;> intros n l₁ l₂ h
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
have l₁_nil : l₁ = [] := by cases l₁; rfl; contradiction
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
l₂_nil : l₂ = []
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
have l₂_nil : l₂ = [] := by cases l₂; rfl; rw [List.length_append] at h; contradiction
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
l₂_nil : l₂ = []
⊢ List.oldMapIdxCore f n ([] ++ []) = List.oldMapIdxCore f n [] ++ List.oldMapIdxCore f (n + length []) []
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
l₂_nil : l₂ = []
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
simp only [l₁_nil, l₂_nil]
no goals
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
l₂_nil : l₂ = []
⊢ List.oldMapIdxCore f n ([] ++ []) = List.oldMapIdxCore f n [] ++ List.oldMapIdxCore f (n + length []) []
rfl
case nil
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₂ : List α
h : length ([] ++ l₂) = Nat.zero
⊢ [] = []

case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₂ : List α
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝ ++ l₂) = Nat.zero
⊢ head✝ :: tail✝ = []
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
⊢ l₁ = []
cases l₁
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₂ : List α
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝ ++ l₂) = Nat.zero
⊢ head✝ :: tail✝ = []
case nil
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₂ : List α
h : length ([] ++ l₂) = Nat.zero
⊢ [] = []

case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₂ : List α
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝ ++ l₂) = Nat.zero
⊢ head✝ :: tail✝ = []
rfl
no goals
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₂ : List α
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝ ++ l₂) = Nat.zero
⊢ head✝ :: tail✝ = []
contradiction
case nil
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
h : length (l₁ ++ []) = Nat.zero
⊢ [] = []

case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length (l₁ ++ head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
⊢ l₂ = []
cases l₂
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length (l₁ ++ head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
case nil
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
h : length (l₁ ++ []) = Nat.zero
⊢ [] = []

case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length (l₁ ++ head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
rfl
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length l₁ + length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length (l₁ ++ head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
rw [List.length_append] at h
no goals
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length l₁ + length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
contradiction
case succ.nil
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
h : length ([] ++ l₂) = Nat.succ len
⊢ List.oldMapIdxCore f n ([] ++ l₂) = List.oldMapIdxCore f n [] ++ List.oldMapIdxCore f (n + length []) l₂

case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ List.oldMapIdxCore f n (head :: tail ++ l₂) =
    List.oldMapIdxCore f n (head :: tail) ++ List.oldMapIdxCore f (n + length (head :: tail)) l₂
case succ
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.succ len
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
cases' l₁ with head tail
no goals
case succ.nil
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
h : length ([] ++ l₂) = Nat.succ len
⊢ List.oldMapIdxCore f n ([] ++ l₂) = List.oldMapIdxCore f n [] ++ List.oldMapIdxCore f (n + length []) l₂
rfl
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ List.oldMapIdxCore f (n + 1) (tail ++ l₂) =
    List.oldMapIdxCore f (n + 1) tail ++ List.oldMapIdxCore f (n + Nat.succ (length tail)) l₂
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ List.oldMapIdxCore f n (head :: tail ++ l₂) =
    List.oldMapIdxCore f n (head :: tail) ++ List.oldMapIdxCore f (n + length (head :: tail)) l₂
simp only [List.oldMapIdxCore, List.append_eq, length_cons, cons_append,cons.injEq, true_and]
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
this : n + Nat.succ (length tail) = n + 1 + length tail
⊢ List.oldMapIdxCore f (n + 1) (tail ++ l₂) =
    List.oldMapIdxCore f (n + 1) tail ++ List.oldMapIdxCore f (n + Nat.succ (length tail)) l₂

case this
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ n + Nat.succ (length tail) = n + 1 + length tail
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ List.oldMapIdxCore f (n + 1) (tail ++ l₂) =
    List.oldMapIdxCore f (n + 1) tail ++ List.oldMapIdxCore f (n + Nat.succ (length tail)) l₂
suffices : n + Nat.succ (length tail) = n + 1 + tail.length
case this
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ n + Nat.succ (length tail) = n + 1 + length tail
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
this : n + Nat.succ (length tail) = n + 1 + length tail
⊢ List.oldMapIdxCore f (n + 1) (tail ++ l₂) =
    List.oldMapIdxCore f (n + 1) tail ++ List.oldMapIdxCore f (n + Nat.succ (length tail)) l₂

case this
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ n + Nat.succ (length tail) = n + 1 + length tail
{ rw [this]
  apply ih (n + 1) _ _ _
  simp only [cons_append, length_cons, length_append, Nat.succ.injEq] at h
  simp only [length_append, h] }
no goals
case this
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ n + Nat.succ (length tail) = n + 1 + length tail
{ rw [Nat.add_assoc]; simp only [Nat.add_comm] }