lean4 のコード例と(日本語)解説を作成する

import Mathlib.Init.Set

-- Set α は α の部分集合全体を表す
#check Set Nat -- Set Nat : Type

-- 関数 f の値域 range f を定義する
def range (f : α → β) : Set β := { b : β | ∃ a : α, f a = b }

-- 関数 f が全射であるとは， f の値域が全体集合(Set.univ)であることをいう
def surjective (f : α → β) : Prop := range f = Set.univ

-- Cantor の定理: 全射 f : α → Set α は存在しない
theorem cantor : ¬ ∃ f : α → Set α, surjective f := by
  -- 全射 f : α → Set α が存在すると仮定して矛盾(False)を示せばよい
  intro (h : ∃ f, surjective f)
  show False
  -- 仮定 h から関数 f と仮定 hf :surjective f を取り出す
  cases h with | intro f hf =>
  -- ここから対角線論法で矛盾を導く
  -- 集合 S を，元 a : α で集合 f a が自分自身を含まないものの集合と定義する
  let S : Set α := { a : α | a ∉ f a }
  -- f は全射なので S ∈ range f である
  have hS₀ : S ∈ range f := by
    -- surjective の定義を展開する
    simp [surjective] at hf
    -- すると hf : range f = Set.univ となる
    -- これで結論を書き換える
    rw [hf]
    show S ∈ Set.univ
    -- 全体集合は全ての要素を含むので，結論は明らかに成り立つ
    trivial
  -- 従ってある a : α が存在して f a = S である
  have hS : ∃ a : α, f a = S := by
    -- さきほど示した hS₀ : S ∈ range f における range の定義を展開する
    unfold range at hS₀
    -- すると hS₀ : S ∈ { b | ∃ a, f a = b } となり，結論が得られる
    exact hS₀
  -- 再び存在の仮定 hS から元 a と仮定 haS : f a = S を取り出す
  cases hS with | intro a haS =>
  -- 取り出した a について，a ∈ f a の場合と a ∉ f a の場合に場合分けして，それぞれで矛盾を導く
  by_cases ha : a ∈ f a
  case inl => -- a ∈ f a の場合
    -- 仮定 a ∈ f a および haS : f a = S より a ∈ S である
    have : a ∈ S := by rw [haS] at ha; exact ha
    -- すると S の定義より a ∉ f a である
    have : a ∉ f a := by
      exact this
    -- 従って矛盾する
    contradiction
  case inr => -- a ∉ f a の場合
    -- 仮定 a ∉ f a および haS : f a = S より a ∉ S である
    have : a ∉ S := by rw [haS] at ha; exact ha
    -- すると S の定義より a ∉ f a ではない，すなわち a ∈ f a である
    have : a ∈ f a := by
      exact Classical.byContradiction this
    -- 従って矛盾する
    contradiction
  -- QED

import Mathlib.Data.Nat.Basic

-- Fibonacci 数列の定義
def fib : ℕ → ℕ
| 0 => 0 -- 0 番目の要素は 0
| 1 => 1 -- 1 番目の要素は 1
| n + 2 => fib n + fib (n + 1)
  -- (n+2) 番目の要素は n 番目の要素と (n+1) 番目の要素の和

-- 上の定義の本来の形は以下のようになる
-- match の文脈では n+2 を自動的に .succ (.succ n) と見做してくれる(頭がいい)
def _fibExpl : ℕ → ℕ := λ n ↦ match n with
| .zero => .zero
| .succ .zero => .succ .zero
| .succ (.succ n) => _fibExpl n + _fibExpl (.succ n)

#eval fib 10 -- 55
-- 現在の定義は無駄な再帰を行うので少し数が大きくなるだけで遅くなる
#eval fib 30 -- 832040
-- #eval fib 35

-- 以下のように書き換えてみる
-- まず，n 番目の要素と (n+1) 番目の要素をペアで表し，次のペアを計算する関数 fib'Step を定義する
def fib'Step : ℕ × ℕ → ℕ × ℕ
| (a, b) => (b, a + b)

-- fib'Step を n 回繰り返す関数 fib'Inner を定義する
def fib'Inner : ℕ → ℕ × ℕ → ℕ × ℕ
| 0, p => p
| n + 1, p => fib'Inner n (fib'Step p)

-- 最後に，(0, 1) を初期値として fib'Inner を計算し，結果のペアの1つ目の値を返す
def fib' : ℕ → ℕ
| n => (fib'Inner n (0, 1)).1

-- こちらは大きい数でも高速に計算できる
#eval fib' 10 -- 55
#eval fib' 35 -- 9227465
#eval fib' 100 -- 354224848179261915075
#eval fib' 1000 -- 4346655768693743...

-- これらの定義が同じ数列を定めることを証明する
-- まずは，fib'Inner の定義を反転させても結果が等しいことを示す
-- (初めからこうしないのは末尾再帰にするため)
lemma fib'Inner_rev : fib'Inner (n + 1) p = fib'Step (fib'Inner n p) := by
  induction n generalizing p
  case zero => simp [fib'Inner]
  case succ n ih =>
    -- ih : ∀ {p}, fib'Inner (n + 1) p = fib'Step (fib'Inner n p)
    calc
    fib'Inner (n + 1 + 1) p
      = fib'Inner (n + 1) (fib'Step p) := by rw [fib'Inner]
    _ = fib'Step (fib'Inner n (fib'Step p)) := ih
    _ = fib'Step (fib'Inner (n + 1) p) := by rw [fib'Inner]

theorem fib_eq_fib' : fib = fib' := by
  -- 2つの関数 Fib, FaseFib が等しいことを示すために，任意の n に対して fib n = fib' n が成り立つことを証明する
  funext n
  show fib n = fib' n
  -- n に関する帰納法で示す
  -- Nat.two_step_induction を使い，n=0, n=1 の場合を示した後，n=k, n=k+1 の場合を仮定して n=k+2 の場合を示す
  induction n using Nat.two_step_induction
  case H1 | H2 => -- n = 0 または n = 1 の場合
    -- これらの場合は実際に両辺を計算すれば証明できる
    simp [fib, fib']
  case H3 k ih₀ ih₁ => -- n = k + 2 の場合
    -- ih₀ : fib k = fib' k
    -- ih₁ : fib (k + 1) = fib' (k + 1)
    show fib (k + 2) = fib' (k + 2)
    -- 名前が長いので省略
    let i := fib'Inner; let s := fib'Step
    -- 左辺を式変形して右辺に書き換える
    -- (p.1 はペアの1つ目の要素，p.2 は2つ目の要素を表す)
    calc
      fib (k + 2)
        = fib k + fib (k + 1)                   := by simp [fib]
                                                -- fib の定義より
      _ = fib' k + fib' (k + 1)                 := by simp [ih₀, ih₁]
                                                -- 帰納法の仮定より
      _ = (i k (0, 1)).1 + (i (k + 1) (0, 1)).1 := by simp [fib', fib'Inner]
                                                -- fib', fib'Inner の定義より
      _ = (i k (0, 1)).1 + (s (i k (0, 1))).1   := by simp [fib'Inner_rev]
                                                -- 補題 fib'Inner_rev より
      _ = (i k (0, 1)).1 + (i k (0, 1)).2       := by simp [fib'Step]
                                                -- fib'Step の定義より
      _ = (s (i k (0, 1))).2                    := by simp [fib'Step]
                                                -- fib'Step の定義より
      _ = (s (s (i k (0, 1)))).1                := by simp [fib'Step]
                                                -- fib'Step の定義より
      _ = (i (k + 2) (0, 1)).1                  := by simp [fib'Inner_rev]
                                                -- 補題 fib'Inner_rev より
      _ = fib' (k + 2)                          := by simp [fib']
                                                -- fib' の定義より

import Std.Data.Rat.Basic
import Mathlib.Data.Nat.Prime
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Qify

/-
有理数 r : ℚ は以下の4つのフィールドからなる構造体である：

  r.num : ℤ -- 分子；
  r.den : ℕ -- 分母；
  r.den_nz : r.den ≠ 0 -- 分母は0でない；
  r.reduced : Nat.coprime (r.num.natAbs) (r.den) -- 分子の絶対値と分母は互いに素．

Lean では，ℤ 型の期待される場所に ℕ 型の値が現れた場合などに自動的に型強制(type coercion)を行う機能が備わっているが，それでも ℕ 型と ℤ 型と ℚ 型の値が入り乱れると明示的な型変換を挟む必要があるなどやや面倒がある．
そのため，分母を単に ℤ 型に変換して返す関数 Rat.den' と，Rat.num と Rat.den' の絶対値が互いに素であるという仮定 Rat.reduced' を定義して用いる．

なお，有理数をそのまま cases すると上記の4つのフィールドを直に取り出せるが，有理数型の生のコンストラクタに対する操作はかなり複雑で関連する lemma も少なく詰みやすいため，後に行うようにフィールドは let で束縛した上で本体に対しては Std.Data.Rat.Lemmas の補題などを用いていくほうがよいと思われる．
-/

@[simp]
def Rat.den' (r : ℚ) : ℤ := r.den

lemma Rat.reduced' (r : ℚ) : r.num.natAbs.coprime r.den'.natAbs := by
  simp; exact r.reduced

/-
さらに補題を一つ示しておく：a, b, c : ℕ について，a * b と a * c が互いに素ならば a = 1 .
-/
lemma Nat.coprime_mul_imp_one (a b c : ℕ) : (a * b).coprime (a * c) → a = 1 := by
  --　a * b と a * c が互いに素と仮定する
  intro (h : (a * b).coprime (a * c))
  show a = 1
  -- a * b と a * c が互いに素より a と a * c は互いに素
  have : a.coprime (a * c) := by
    exact Nat.coprime.coprime_mul_right h
  -- a と a * c が互いに素より a と a は互いに素
  have : a.coprime a := by
    rw [Nat.coprime_comm] at this
    exact Nat.coprime.coprime_mul_right this
  -- ゆえに a = 1
  exact a.coprime_self.mp this

/-
定理: 任意の有理数は二乗して2にはならない．
-/
theorem rat_not_sqrt2 (r : ℚ) : r * r ≠ 2 := by
  -- r * r = 2 と仮定して矛盾を導く
  intro (h : r * r = 2)
  show False
  -- p/q := r (p,q : ℤ, q ≠ 0 かつ h_red : p, q は互いに素) とおく
  let p : ℤ := r.num
  let q : ℤ := r.den'
  have h_red : p.natAbs.coprime q.natAbs := r.reduced'
  -- p,q の定義より p = r * q
  have : p = r * q := by simp
  -- r * r = 2 より p * p = 2 * q * q
  have hpq : p * p = 2 * q * q := by
    -- 主張を ℤ におけるものから ℚ におけるものに変換する
    qify
    -- あとは計算
    calc p * p
        = (r * q) * (r * q) := by rw [this] -- p = r * q より
      _ = (r * r) * q * q   := by linarith  -- 適切に変形する
      _ = 2 * q * q         := by rw [h]
  -- 2 ∣ p を示す
  have : 2 ∣ p * p := by
    -- hpq で p * p を 2 * q * q に置き換える
    rw [hpq, Int.mul_assoc]
    show 2 ∣ 2 * (q * q)
    -- 結論が a ∣ a * b の形なので成り立つ
    exact dvd_mul_right 2 (q * q)
  have : 2 ∣ p := by
    -- 2 ∣ p * p より 2 ∣ p または 2 ∣ p，
    have : 2 ∣ p ∨ 2 ∣ p := Int.prime_two.dvd_or_dvd this
    -- よっていずれの場合も 2 ∣ p
    cases this; repeat assumption
  -- よってある p' が存在して p = 2 * p' である
  cases this with | intro p' hp' =>
  -- hp' : p = 2 * p'
  -- 同様に 2 ∣ q を示していく
  have : q * q = 2 * (p' * p') := by
    -- 2 ≠ 0 かつ 2 * (q * q) = 2 * (2 * (p' * p')) より
    -- q * q = 2 * (p' * p') がいえる
    have h₀ : (2 : ℤ) ≠ 0 := by simp
    have h₁ : 2 * (q * q) = 2 * (2 * (p' * p')) := calc
      2 * (q * q)
        = 2 * q * q           := by rw [Int.mul_assoc]
      _ = p * p               := by rw [hpq]
      _ = (2 * p') * (2 * p') := by rw [hp']
      _ = 2 * (2 * (p' * p')) := by linarith
    exact Int.eq_of_mul_eq_mul_left h₀ h₁
  -- あとは p の場合と同様
  have : 2 ∣ q * q := by
    rw [this]
    exact dvd_mul_right 2 (p' * p')
  have : 2 ∣ q := by
    have : 2 ∣ q ∨ 2 ∣ q := Int.prime_two.dvd_or_dvd this
    cases this; repeat assumption
  -- よってある q' が存在して q = 2 * q' である
  cases this with | intro q' hq' =>
  -- hq' : q = 2 * q'
  -- すると 2 * |p'| と 2 * |q'| が互いに素であることになる
  have : (2 * p'.natAbs).coprime (2 * q'.natAbs) := by
    have : ∀ x : ℤ, (2 * x).natAbs = 2 * x.natAbs := by
      intro x
      calc (2 * x).natAbs
        = (2 : ℤ).natAbs * x.natAbs := Int.natAbs_mul 2 x
      _ = 2 * x.natAbs              := by simp
    rw [←this p', ←this q', ←hp', ←hq']
    show p.natAbs.coprime q.natAbs
    exact h_red
  -- よって補題 Nat.coprime_mul_imp_one から矛盾が導かれる
  have : 2 = 1 := by
    exact Nat.coprime_mul_imp_one 2 p'.natAbs q'.natAbs this
  contradiction

import Mathlib.Logic.Basic

-- (中略)

/-
  選択公理を使うと排中律 p ∨ ¬ p が証明できる．
  参考: https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
-/

def ac := ∀ {α : Type} {β : Type} (r : α → β → Prop), (∀ x, ∃ y, r x y) → ∃ f : α → β, ∀ x, r x (f x)

def lem := ∀ p, p ∨ ¬ p

-- 2つの要素 t, f からなる型 T を定義する
inductive T := | t | f

-- 選択公理を用いて排中律を証明する
theorem ac_implies_lem : ac → lem := by
  -- 選択公理を仮定
  intro (hac : ac)
  -- 命題 p を任意に取る
  intro p

  -- まず，2つの関数 U, V : T → Prop を定義する
  let U : T → Prop := λ x ↦ x = .f ∨ p
  let V : T → Prop := λ x ↦ x = .t ∨ p
  -- 関数 χ : T → Prop に対して命題 Φ χ を定義する
  let Φ (χ : T → Prop) : Prop := χ = U ∨ χ = V

  -- 命題 Φ χ が成り立つような χ : T → Prop からなる部分型を TPΦ とおく
  let TPΦ := {χ : T → Prop // Φ χ}
  -- (部分型(Subtype) {x : T // p x} は値 val : T と条件 property : p val の組 ⟨ val, property ⟩ からなる型)
  -- Φ, U, V の定義より Φ (U) と Φ (V) は明らかに成り立つ
  have hU : Φ (U) := by left; rfl
  have hV : Φ (V) := by right; rfl
  -- よって U, V を TPΦ の元にできる
  let U' : TPΦ := ⟨ U, hU ⟩
  let V' : TPΦ := ⟨ V, hV ⟩

  -- ⟨χ, hχ⟩ : TPΦ に対して χ x が真となるような x : T を選ぶ関数を作るために選択公理を用いる
  -- そのためにまず関数 r : TPΦ → T → Prop を定義する
  let r (χ_hχ : TPΦ) (x : T) : Prop := χ_hχ.val x
  -- 選択公理の仮定が成り立つことを示す
  have : ∀ χ_hχ : TPΦ, ∃ x, r χ_hχ x := by
    -- χ_hχ を値 χ : T → Prop と条件 hχ : Φ χ に分解する
    intro ⟨ χ, (hχ : Φ χ) ⟩
    show ∃ x, χ x
    -- Φ の定義を展開すると hχ : χ = U ∨ χ = V となる
    have : χ = U ∨ χ = V := hχ
    cases this
    case inl hχₗ => -- χ = U の場合
      -- hχₗ ; χ = U
      -- U x := x = .f ∨ p なので，x = .f とすれば明らか
      exists .f
      rw [hχₗ]; simp
    case inr hχᵣ => -- χ = V の場合
      -- hχᵣ ; χ = V
      -- この場合も同様で，今度は x = .t とする
      exists .t
      rw [hχᵣ]; simp
  -- r に関する選択公理を使う
  cases hac r this with | intro x hx =>
  -- 以下を得る：
  -- x : { χ // Φ χ } → T
  -- hx : ∀ (χ_hχ : { χ // Φ χ }), r χ_hχ (x χ_hχ)

  -- hx を整理する
  simp at hx
  -- hx : ∀ (χ_hχ : { χ // Φ χ }), χ.val (x χ hχ)
  -- hx を U', V' に適用して以下を得る
  have hxU : U (x U') := hx U'
  have hxV : V (x V') := hx V'
  -- 整理すると以下のようになる
  have hxU' : x U' = .f ∨ p := hxU
  have hxV' : x V' = .t ∨ p := hxV

  -- hxU', hxV' それぞれについて，左右どちらが成り立つかで場合分け
  cases hxU'
  case inr => left; assumption -- p が成り立つ場合(明らかに p ∨ ¬ p)
  case inl h₁ => -- x U' = .f の場合
    cases hxV'
    case inr => left; assumption -- p が成り立つ場合(明らかに p ∨ ¬ p)
    case inl h₂ => -- x U' = .t の場合
      -- h₁ : x U' = .f
      -- h₂ : x V' = .t
      -- このとき，¬ p を示すことができる
      right; show ¬ p
      -- p と仮定して矛盾を導く
      intro (hp : p)
      show False
      -- いま，p が成り立つので任意の x に対して U x が成り立つ
      have hU' : ∀ x, U x = True := by
        intros; simp; right; assumption
      -- 同様に任意の x に対して V x が成り立つ
      have hV' : ∀ x, V x = True := by
        intros; simp; right; assumption
      -- よって U = V が成り立つ
      have : U = V := by
        funext x; rw [hU' x, hV' x]
      -- ゆえに U' = V' も成り立つ
      have : U' = V' := by
        simp only [this]
      -- 従って，x U' hU = x V' hV が成り立つ
      have : x U' = x V' := by
        simp only [this]
      -- よって h₁, h₂ より T.t = T.f が示される
      have : T.t = T.f := by
        rw [← h₁, ← h₂, this]
      -- これは矛盾
      contradiction

-- 仮定した選択公理以外の公理を使っていないか確認
#print axioms ac_implies_lem
-- => 'lem' depends on axioms: [propext, Quot.sound]

/-
  Classical.choice は現れていないが，2つの公理が必要になっていることがわかる
  この2つの公理は以下の要請で，ロジックの観点では重要な代物だが，通常の数学をやる上ではそれほど気にしなくていいと思われる
  
  - propext ... 同値な2つの命題は「等しい」: (a ↔ b) → a = b
  - Quot.sound ... 商型(Quotient type)の要素の等しさを定める: r a b → Quot.mk r a = Quot.mk r b
-/

#print propext
#print Quot.sound

-- (前略)

-- 二項定理
theorem binomial_thm {R} [CommRing R] (a b : R) (n : ℕ)
  : (a + b)^n = ∑ k  ≤ n, C' n k * a^k * b^(n - k)
  := by
  -- n に関する帰納法で示す
  induction n
  case zero => -- n = 0 の場合
    show (a + b)^0 = ∑ k ≤ 0, C' 0 k * a^k * b^(0 - k)
    -- 計算すればわかる
    simp
  case succ n' ih => -- n = n' + 1 の場合
    -- ih : (a + b) ^ n' = ∑ k in .range n', C' n' k * a ^ k * b ^ (n' - k)
    -- ひたすら計算する
    -- ところどころ強いタクティクを使ってはいるが，一つ一つの式変形は難しいものではない
    calc
        (a + b) ^ (n' + 1)
        -- (a + b) をひとつ取り出す
      = (a + b) ^ n' * (a + b)
        := pow_succ' (a + b) n'
        -- 帰納法の仮定により (a + b) ^ n' を置き換える
    _ = (∑ k ≤ n', C' n' k * a ^ k * b ^ (n' - k)) * (a + b)
        := by simp [ih]
        -- (∑ f) * (a + b) = ∑ (f * (a + b))
    _ = ∑ k ≤ n',
          C' n' k * a ^ k * b ^ (n' - k) * (a + b)
        := by apply Finset.sum_mul
        -- 分配法則で展開したのち整理する
        -- (ring_nf: 等式の左辺を環の公理で整理する)
    _ = ∑ k ≤ n',
          ( C' n' k * a ^ (k + 1) * b ^ (n' - k)
          + C' n' k * a ^ k * b ^ (n' - k + 1) )
        := by ring_nf; apply Eq.symm; ring_nf
        -- 指数の部分を変形
    _ = ∑ k ≤ n',
          ( C' n' k * a ^ (k + 1) * b ^ ((n' + 1) - (k + 1))
          + C' n' k * a ^ k * b ^ ((n' + 1) - k) )
        := by
          apply Finset.sum_congr rfl
          intro k h; simp at h
          have h' : k ≤ n' := Nat.le_of_lt_succ h
          congr 3
          rw [Nat.succ_sub_succ_eq_sub]
          rw [Nat.sub_add_comm h']
        -- ∑ (f + g) = (∑ f) + (∑ g)
    _ = ( ∑ k ≤ n',
            C' n' k * a ^ (k + 1) * b ^ ((n' + 1) - (k + 1)) )
        + ∑ k ≤ n',
            C' n' k * a ^ k * b ^ ((n' + 1) - k)
          := by apply Finset.sum_add_distrib
        -- 和の一つ目を変形
    _ = ( ∑ k ≤ n',
            C' n' ((1 + k) - 1) * a^(1 + k) * b^((n' + 1) - (1 + k)) )
        + ∑ k ≤ n',
            C' n' k * a^k * b^((n' + 1) - k)
          := by
            congr 1
            . apply Finset.sum_congr rfl
              intro k h; simp at h
              simp
              congr 2
              . congr 1
                show k + 1 = 1 + k
                simp [add_comm]
              . show n' - k = n' + 1 - (1 + k)
                apply Eq.symm
                calc
                    n' + 1 - (1 + k)
                  = n' + 1 - (k + 1) := by simp [add_comm]
                _ = n' - k           := by rw [Nat.succ_sub_succ_eq_sub]
        -- 一つ目の和の先頭に 0 と等しい項を追加して一つの和にまとめる
    _ = ( ∑ k ≤ 0,
            C' n' (k - 1) * a^k * b^((n' + 1) - k)
        + ∑ k ≤ n',
            C' n' ((1 + k) - 1) * a^(1 + k) * b^((n' + 1) - (1 + k)) )
        + ∑ k ≤ n', C' n' k * a^k * b^((n' + 1) - k)
          := by simp [c_n_k_eq_zero_of_k_neg n' (-1)]
    _ = ( ∑ k ≤ n' + 1, C' n' (k - 1) * a^k * b^((n' + 1) - k) )
        + ∑ k ≤ n', C' n' k * a^k * b^((n' + 1) - k)
          := by
            let f := λ k : ℕ ↦ C' n' (k - 1) * a^k * b^((n' + 1) - k)
            have :
              ( ∑ k ≤ 0, C' n' (k - 1) * a^k * b^((n' + 1) - k)
              + ∑ k ≤ n', C' n' ((1 + k) - 1) * a^(1 + k) * b^((n' + 1) - (1 + k)) )
              = ∑ k ≤ n' + 1, C' n' (k - 1) * a^k * b^((n' + 1) - k)
              := calc
                  (∑ k ≤ 0, f k) + ∑ k ≤ n', f (1 + k)
                = ∑ k in .range (1 + (n' + 1)), f k
                  := by simp only [Finset.sum_range_add f 1 (n' + 1)]
              _ = ∑ k ≤ n' + 1, f k
                  := by congr 2; simp [Nat.add_comm]
            rw [this]
        -- 二つ目の和の末尾に 0 と等しい項を追加して一つの和にまとめる
    _ = ( ∑ k  ≤ n' + 1, C' n' (k - 1) * a^k * b^((n' + 1) - k) )
        + ( ∑ k  ≤ n', C' n' k * a^k * b^((n' + 1) - k)
          + C' n' (n' + 1) * a^(n' + 1) * b ^((n' + 1) - (n' + 1)) )
          := by simp [c_n_k_eq_zero_of_k_gt_n n' (n' + 1) (by simp)]
    _ = ( ∑ k  ≤ n' + 1, C' n' (k - 1) * a^k * b^((n' + 1) - k) )
        + ∑ k  ≤ n' + 1, C' n' k * a^k * b^((n' + 1) - k)
          := by simp [Finset.sum_range_succ]
        -- (∑ f) + (∑ g) = ∑ (f + g)
    _ = ∑ k  ≤ n' + 1,
          ( C' n' (k - 1) * a^k * b^((n' + 1) - k)
          + C' n' k * a^k * b^((n' + 1) - k) )
          := by simp [Finset.sum_add_distrib]
        -- 分配法則
    _ = ∑ k  ≤ n' + 1,
          (C' n' (k - 1) + C' n' k) * a^k * b^((n' + 1) - k)
          := by simp [add_mul]
        -- C' n' (k - 1) + C' n' k = C' (n' + 1) k
    _ = ∑ k  ≤ n' + 1,
          C' (n' + 1) k * a^k * b^((n' + 1) - k)
          := by simp
-- QED

example (n : ℕ) : ∑ k ≤ n, C' n k = 2^n := by
  calc
      ∑ k ≤ n, C' n k
    = ∑ k ≤ n, C' n k * 1^k * 1^(n-k) := by simp
  _ = (1 + 1)^n := by simp [binomial_thm 1 1 n]
  _ = 2^n := by congr

example (n : ℕ) : n > 0 → ∑ k ≤ n, (-1 : ℤ)^k * C' n k = 0 := by
  intro (h : 0 < n)
  calc
      ∑ k ≤ n, (-1 : ℤ)^k * C' n k
    = ∑ k ≤ n, C' n k * (-1 : ℤ)^k * 1^(n-k)  := by simp [mul_comm]
  _ = ((-1 : ℤ) + 1)^n                        := by rw [← binomial_thm (-1) 1 n]
  _ = 0                                       := by simp [zero_pow h]