-- Mathlib/Data/Nat/Digits.lean
theorem ofDigits_add_ofDigits_eq_ofDigits_zipWith_of_length_eq {b : ℕ} {l1 l2 : List ℕ}
    (h : l1.length = l2.length) :
    ofDigits b l1 + ofDigits b l2 = ofDigits b (l1.zipWith (· + ·) l2)

Proof state:
case cons.cons
b hd₁ hd₂ : ℕ
tl₂ tl₁ : List ℕ
ih₂ :
  ∀ (tl₁_1 : List ℕ),
    (∀ {l2 : List ℕ},
        tl₁_1.length = l2.length →
          ofDigits b tl₁_1 + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) tl₁_1 l2)) →
      tl₁.length = tl₁_1.length + 1 →
        hd₁ + b * ofDigits b tl₁_1 + ofDigits b tl₂ =
          ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) (hd₁ :: tl₁_1) tl₂)
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) tl₁ l2)
h : tl₂.length = tl₁.length
⊢ hd₁ + b * ofDigits b tl₁ + (hd₂ + b * ofDigits b tl₂) =
    hd₁ + hd₂ + b * ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) tl₁ tl₂)

Tactic:
rw [← ih₁ h.symm, mul_add]

Result:
case cons.cons
b hd₁ hd₂ : ℕ
tl₂ tl₁ : List ℕ
ih₂ :
  ∀ (tl₁_1 : List ℕ),
    (∀ {l2 : List ℕ},
        tl₁_1.length = l2.length →
          ofDigits b tl₁_1 + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) tl₁_1 l2)) →
      tl₁.length = tl₁_1.length + 1 →
        hd₁ + b * ofDigits b tl₁_1 + ofDigits b tl₂ =
          ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) (hd₁ :: tl₁_1) tl₂)
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) tl₁ l2)
h : tl₂.length = tl₁.length
⊢ hd₁ + b * ofDigits b tl₁ + (hd₂ + b * ofDigits b tl₂) = hd₁ + hd₂ + (b * ofDigits b tl₁ + b * ofDigits b tl₂)

Proof state:
case cons.cons
b hd₁ hd₂ : ℕ
tl₂ : List ℕ
ih₂ :
  ∀ (tl₁ : List ℕ),
    (∀ {l2 : List ℕ},
        tl₁.length = l2.length →
          ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) tl₁ l2)) →
      (hd₁ :: tl₁).length = tl₂.length →
        ofDigits b (hd₁ :: tl₁) + ofDigits b tl₂ = ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) (hd₁ :: tl₁) tl₂)
tl₁ : List ℕ
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) tl₁ l2)
h : (hd₁ :: tl₁).length = (hd₂ :: tl₂).length
⊢ ofDigits b (hd₁ :: tl₁) + ofDigits b (hd₂ :: tl₂) =
    ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) (hd₁ :: tl₁) (hd₂ :: tl₂))

Tactic:
simp_all only [List.length_cons, succ_eq_add_one, ofDigits_cons, add_left_inj,
  eq_comm, List.zipWith_cons_cons, add_eq]

Result:
case cons.cons
b hd₁ hd₂ : ℕ
tl₂ tl₁ : List ℕ
ih₂ :
  ∀ (tl₁_1 : List ℕ),
    (∀ {l2 : List ℕ},
        tl₁_1.length = l2.length →
          ofDigits b tl₁_1 + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) tl₁_1 l2)) →
      tl₁.length = tl₁_1.length + 1 →
        hd₁ + b * ofDigits b tl₁_1 + ofDigits b tl₂ =
          ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) (hd₁ :: tl₁_1) tl₂)
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) tl₁ l2)
h : tl₂.length = tl₁.length
⊢ hd₁ + b * ofDigits b tl₁ + (hd₂ + b * ofDigits b tl₂) =
    hd₁ + hd₂ + b * ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) tl₁ tl₂)

Proof state:
case cons
b hd₁ : ℕ
tl₁ : List ℕ
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) tl₁ l2)
l2 : List ℕ
h : (hd₁ :: tl₁).length = l2.length
⊢ ofDigits b (hd₁ :: tl₁) + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) (hd₁ :: tl₁) l2)

Tactic:
induction l2 generalizing tl₁ with
| nil => simp_all
| cons hd₂ tl₂ ih₂ =>
  simp_all only [List.length_cons, succ_eq_add_one, ofDigits_cons, add_left_inj,
    eq_comm, List.zipWith_cons_cons, add_eq]
  rw [← ih₁ h.symm, mul_add]
  ac_rfl

Result:
no goals

Proof state:
b : ℕ
l1 l2 : List ℕ
h : l1.length = l2.length
⊢ ofDigits b l1 + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) l1 l2)

Tactic:
induction l1 generalizing l2 with
| nil => simp_all [eq_comm, List.length_eq_zero, ofDigits]
| cons hd₁ tl₁ ih₁ =>
  induction l2 generalizing tl₁ with
  | nil => simp_all
  | cons hd₂ tl₂ ih₂ =>
    simp_all only [List.length_cons, succ_eq_add_one, ofDigits_cons, add_left_inj,
      eq_comm, List.zipWith_cons_cons, add_eq]
    rw [← ih₁ h.symm, mul_add]
    ac_rfl

Result:
no goals

Proof state:
case cons.nil
b hd₁ : ℕ
tl₁ : List ℕ
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) tl₁ l2)
h : (hd₁ :: tl₁).length = [].length
⊢ ofDigits b (hd₁ :: tl₁) + ofDigits b [] = ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) (hd₁ :: tl₁) [])

Tactic:
simp_all

Result:
no goals

Proof state:
case nil
b : ℕ
l2 : List ℕ
h : [].length = l2.length
⊢ ofDigits b [] + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) [] l2)

Tactic:
simp_all [eq_comm, List.length_eq_zero, ofDigits]

Result:
no goals

Proof state:
case cons.cons
b hd₁ hd₂ : ℕ
tl₂ tl₁ : List ℕ
ih₂ :
  ∀ (tl₁_1 : List ℕ),
    (∀ {l2 : List ℕ},
        tl₁_1.length = l2.length →
          ofDigits b tl₁_1 + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) tl₁_1 l2)) →
      tl₁.length = tl₁_1.length + 1 →
        hd₁ + b * ofDigits b tl₁_1 + ofDigits b tl₂ =
          ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) (hd₁ :: tl₁_1) tl₂)
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) tl₁ l2)
h : tl₂.length = tl₁.length
⊢ hd₁ + b * ofDigits b tl₁ + (hd₂ + b * ofDigits b tl₂) = hd₁ + hd₂ + (b * ofDigits b tl₁ + b * ofDigits b tl₂)

Tactic:
ac_rfl

Result:
no goals