-- Mathlib/Data/List/Indexes.lean
theorem oldMapIdxCore_append : ∀ (f : ℕ → α → β) (n : ℕ) (l₁ l₂ : List α),
    List.oldMapIdxCore f n (l₁ ++ l₂) =
    List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + l₁.length) l₂

Proof state:
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₂ : List α
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝ ++ l₂).length = 0
⊢ head✝ :: tail✝ = []

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
⊢ ∀ (n : ℕ) (l₁ l₂ : List α),
    (l₁ ++ l₂).length = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + l₁.length) l₂

Tactic:
induction' len with len ih <;> intros n l₁ l₂ h

Result:
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : (l₁ ++ l₂).length = 0
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + l₁.length) l₂

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

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

Tactic:
rw [this]

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

Proof state:
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : (l₁ ++ l₂).length = 0
l₁_nil : l₁ = []
⊢ l₂ = []

Tactic:
cases l₂

Result:
case nil
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
h : (l₁ ++ []).length = 0
⊢ [] = []

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

Proof state:
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (n : ℕ) (l₁ l₂ : List α),
    List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + l₁.length) l₂

Tactic:
intros f n l₁ l₂

Result:
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + l₁.length) l₂

Proof state:
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
len : ℕ
e : (l₁ ++ l₂).length = len
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + l₁.length) l₂

Tactic:
revert n l₁ l₂

Result:
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
⊢ ∀ (n : ℕ) (l₁ l₂ : List α),
    (l₁ ++ l₂).length = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + l₁.length) l₂

Proof state:
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : l₁.length + (head✝ :: tail✝).length = 0
⊢ head✝ :: tail✝ = []

Tactic:
contradiction

Result:
no goals

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

Tactic:
apply ih (n + 1) _ _ _

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

Proof state:
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : (l₁ ++ head✝ :: tail✝).length = 0
⊢ head✝ :: tail✝ = []

Tactic:
rw [List.length_append] at h

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

Proof state:
case nil
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
h : (l₁ ++ []).length = 0
⊢ [] = []

Tactic:
rfl

Result:
no goals

Proof state:
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : (l₁ ++ l₂).length = 0
l₁_nil : l₁ = []
l₂_nil : l₂ = []
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + l₁.length) l₂

Tactic:
simp only [l₁_nil, l₂_nil]

Result:
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : (l₁ ++ l₂).length = 0
l₁_nil : l₁ = []
l₂_nil : l₂ = []
⊢ List.oldMapIdxCore f n ([] ++ []) = List.oldMapIdxCore f n [] ++ List.oldMapIdxCore f (n + [].length) []

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

Tactic:
simp only [cons_append, length_cons, length_append, Nat.succ.injEq] at h

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

Proof state:
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + l₁.length) l₂

Tactic:
generalize e : (l₁ ++ l₂).length = len

Result:
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
len : ℕ
e : (l₁ ++ l₂).length = len
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + l₁.length) l₂

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

Tactic:
simp only [length_append, h]

Result:
no goals

Proof state:
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : (l₁ ++ l₂).length = 0
l₁_nil : l₁ = []
l₂_nil : l₂ = []
⊢ List.oldMapIdxCore f n ([] ++ []) = List.oldMapIdxCore f n [] ++ List.oldMapIdxCore f (n + [].length) []

Tactic:
rfl

Result:
no goals