[GOAL]
tm : FinTM2
s : List (FinTM2.Γ tm tm.k₀)
k : tm.K
h : k = tm.k₀
⊢ List (FinTM2.Γ tm k)
[PROOFSTEP]
rw [h]
[GOAL]
tm : FinTM2
s : List (FinTM2.Γ tm tm.k₀)
k : tm.K
h : k = tm.k₀
⊢ List (FinTM2.Γ tm tm.k₀)
[PROOFSTEP]
exact s
[GOAL]
tm : FinTM2
s : List (FinTM2.Γ tm tm.k₁)
k : tm.K
h : k = tm.k₁
⊢ List (FinTM2.Γ tm k)
[PROOFSTEP]
rw [h]
[GOAL]
tm : FinTM2
s : List (FinTM2.Γ tm tm.k₁)
k : tm.K
h : k = tm.k₁
⊢ List (FinTM2.Γ tm tm.k₁)
[PROOFSTEP]
exact s
[GOAL]
σ : Type u_1
f : σ → Option σ
a b : σ
c : Option σ
h₁ : EvalsTo f a (some b)
h₂ : EvalsTo f b c
⊢ (flip bind f)^[h₂.steps + h₁.steps] (some a) = c
[PROOFSTEP]
rw [Function.iterate_add_apply, h₁.evals_in_steps, h₂.evals_in_steps]
[GOAL]
α : Type
ea : FinEncoding α
x✝ : α
⊢ { steps := 1,
        evals_in_steps :=
          (_ :
            (flip bind
                    (FinTM2.step
                      { tm := idComputer ea,
                          inputAlphabet :=
                            Equiv.cast
                              (_ :
                                FinTM2.Γ (idComputer ea) (idComputer ea).k₀ =
                                  FinTM2.Γ (idComputer ea) (idComputer ea).k₀),
                          outputAlphabet :=
                            Equiv.cast
                              (_ :
                                FinTM2.Γ (idComputer ea) (idComputer ea).k₁ =
                                  FinTM2.Γ (idComputer ea) (idComputer ea).k₁) }.tm))^[1]
                (some
                  (initList
                    { tm := idComputer ea,
                        inputAlphabet :=
                          Equiv.cast
                            (_ :
                              FinTM2.Γ (idComputer ea) (idComputer ea).k₀ =
                                FinTM2.Γ (idComputer ea) (idComputer ea).k₀),
                        outputAlphabet :=
                          Equiv.cast
                            (_ :
                              FinTM2.Γ (idComputer ea) (idComputer ea).k₁ =
                                FinTM2.Γ (idComputer ea) (idComputer ea).k₁) }.tm
                    (List.map
                      { tm := idComputer ea,
                            inputAlphabet :=
                              Equiv.cast
                                (_ :
                                  FinTM2.Γ (idComputer ea) (idComputer ea).k₀ =
                                    FinTM2.Γ (idComputer ea) (idComputer ea).k₀),
                            outputAlphabet :=
                              Equiv.cast
                                (_ :
                                  FinTM2.Γ (idComputer ea) (idComputer ea).k₁ =
                                    FinTM2.Γ (idComputer ea) (idComputer ea).k₁) }.inputAlphabet.invFun
                      (Encoding.encode ea.toEncoding x✝)))) =
              (flip bind
                    (FinTM2.step
                      { tm := idComputer ea,
                          inputAlphabet :=
                            Equiv.cast
                              (_ :
                                FinTM2.Γ (idComputer ea) (idComputer ea).k₀ =
                                  FinTM2.Γ (idComputer ea) (idComputer ea).k₀),
                          outputAlphabet :=
                            Equiv.cast
                              (_ :
                                FinTM2.Γ (idComputer ea) (idComputer ea).k₁ =
                                  FinTM2.Γ (idComputer ea) (idComputer ea).k₁) }.tm))^[1]
                (some
                  (initList
                    { tm := idComputer ea,
                        inputAlphabet :=
                          Equiv.cast
                            (_ :
                              FinTM2.Γ (idComputer ea) (idComputer ea).k₀ =
                                FinTM2.Γ (idComputer ea) (idComputer ea).k₀),
                        outputAlphabet :=
                          Equiv.cast
                            (_ :
                              FinTM2.Γ (idComputer ea) (idComputer ea).k₁ =
                                FinTM2.Γ (idComputer ea) (idComputer ea).k₁) }.tm
                    (List.map
                      { tm := idComputer ea,
                            inputAlphabet :=
                              Equiv.cast
                                (_ :
                                  FinTM2.Γ (idComputer ea) (idComputer ea).k₀ =
                                    FinTM2.Γ (idComputer ea) (idComputer ea).k₀),
                            outputAlphabet :=
                              Equiv.cast
                                (_ :
                                  FinTM2.Γ (idComputer ea) (idComputer ea).k₁ =
                                    FinTM2.Γ (idComputer ea) (idComputer ea).k₁) }.inputAlphabet.invFun
                      (Encoding.encode ea.toEncoding x✝))))) }.steps ≤
    Polynomial.eval (List.length (Encoding.encode ea.toEncoding x✝)) 1
[PROOFSTEP]
simp only [Polynomial.eval_one]


[GOAL]
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x : List α
s✝ : σ
a : α
s : σ
hs : s ∈ εClosure M ∅
⊢ False
[PROOFSTEP]
induction hs
[GOAL]
case base
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x : List α
s✝¹ : σ
a : α
s s✝ : σ
a✝ : s✝ ∈ ∅
⊢ False
[PROOFSTEP]
assumption
[GOAL]
case step
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x : List α
s✝¹ : σ
a : α
s s✝ t✝ : σ
a✝¹ : t✝ ∈ step M s✝ none
a✝ : εClosure M ∅ s✝
a_ih✝ : False
⊢ False
[PROOFSTEP]
assumption
[GOAL]
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
⊢ s ∈ stepSet M S a ↔ ∃ t, t ∈ S ∧ s ∈ εClosure M (step M t (some a))
[PROOFSTEP]
simp_rw [stepSet, mem_iUnion₂, exists_prop]
[GOAL]
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x : List α
s : σ
a✝ a : α
⊢ stepSet M ∅ a = ∅
[PROOFSTEP]
simp_rw [stepSet, mem_empty_iff_false, iUnion_false, iUnion_empty]
[GOAL]
α : Type u
σ σ' : Type v
M : εNFA α σ
S✝ : Set σ
x✝ : List α
s : σ
a✝ : α
S : Set σ
x : List α
a : α
⊢ evalFrom M S (x ++ [a]) = stepSet M (evalFrom M S x) a
[PROOFSTEP]
rw [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]
[GOAL]
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x✝ : List α
s : σ
a : α
x : List α
⊢ evalFrom M ∅ x = ∅
[PROOFSTEP]
induction' x using List.reverseRecOn with x a ih
[GOAL]
case H0
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
⊢ evalFrom M ∅ [] = ∅
[PROOFSTEP]
rw [evalFrom_nil, εClosure_empty]
[GOAL]
case H1
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x✝ : List α
s : σ
a✝ : α
x : List α
a : α
ih : evalFrom M ∅ x = ∅
⊢ evalFrom M ∅ (x ++ [a]) = ∅
[PROOFSTEP]
rw [evalFrom_append_singleton, ih, stepSet_empty]
[GOAL]
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a : α
M : NFA α σ
S : Set σ
⊢ εNFA.εClosure (toεNFA M) S = S
[PROOFSTEP]
ext a
[GOAL]
case h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a✝ : α
M : NFA α σ
S : Set σ
a : σ
⊢ a ∈ εNFA.εClosure (toεNFA M) S ↔ a ∈ S
[PROOFSTEP]
refine' ⟨_, εNFA.εClosure.base _⟩
[GOAL]
case h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a✝ : α
M : NFA α σ
S : Set σ
a : σ
⊢ a ∈ εNFA.εClosure (toεNFA M) S → a ∈ S
[PROOFSTEP]
rintro (⟨_, h⟩ | ⟨_, _, h, _⟩)
[GOAL]
case h.base
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a✝ : α
M : NFA α σ
S : Set σ
a : σ
h : a ∈ S
⊢ a ∈ S
[PROOFSTEP]
exact h
[GOAL]
case h.step
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a✝¹ : α
M : NFA α σ
S : Set σ
a s✝ : σ
a✝ : εNFA.εClosure (toεNFA M) S s✝
h : a ∈ εNFA.step (toεNFA M) s✝ none
⊢ a ∈ S
[PROOFSTEP]
cases h
[GOAL]
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
start : Set σ
⊢ εNFA.evalFrom (toεNFA M) start = evalFrom M start
[PROOFSTEP]
rw [evalFrom, εNFA.evalFrom, toεNFA_εClosure]
[GOAL]
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
start : Set σ
⊢ List.foldl (εNFA.stepSet (toεNFA M)) start = List.foldl (stepSet M) start
[PROOFSTEP]
suffices εNFA.stepSet (toεNFA M) = stepSet M by rw [this]
[GOAL]
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
start : Set σ
this : εNFA.stepSet (toεNFA M) = stepSet M
⊢ List.foldl (εNFA.stepSet (toεNFA M)) start = List.foldl (stepSet M) start
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
start : Set σ
⊢ εNFA.stepSet (toεNFA M) = stepSet M
[PROOFSTEP]
ext S s
[GOAL]
case h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ x✝ ∈ εNFA.stepSet (toεNFA M) S s ↔ x✝ ∈ stepSet M S s
[PROOFSTEP]
simp only [stepSet, εNFA.stepSet, exists_prop, Set.mem_iUnion]
[GOAL]
case h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ (∃ i, i ∈ S ∧ x✝ ∈ εNFA.εClosure (toεNFA M) (εNFA.step (toεNFA M) i (some s))) ↔ ∃ i, i ∈ S ∧ x✝ ∈ step M i s
[PROOFSTEP]
apply exists_congr
[GOAL]
case h.h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ ∀ (a : σ), a ∈ S ∧ x✝ ∈ εNFA.εClosure (toεNFA M) (εNFA.step (toεNFA M) a (some s)) ↔ a ∈ S ∧ x✝ ∈ step M a s
[PROOFSTEP]
simp only [and_congr_right_iff]
[GOAL]
case h.h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ : σ
⊢ ∀ (a : σ), a ∈ S → (x✝ ∈ εNFA.εClosure (toεNFA M) (εNFA.step (toεNFA M) a (some s)) ↔ x✝ ∈ step M a s)
[PROOFSTEP]
intro _ _
[GOAL]
case h.h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ a✝¹ : σ
a✝ : a✝¹ ∈ S
⊢ x✝ ∈ εNFA.εClosure (toεNFA M) (εNFA.step (toεNFA M) a✝¹ (some s)) ↔ x✝ ∈ step M a✝¹ s
[PROOFSTEP]
rw [M.toεNFA_εClosure]
[GOAL]
case h.h.h.h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s✝ : σ
a : α
M : NFA α σ
start S : Set σ
s : α
x✝ a✝¹ : σ
a✝ : a✝¹ ∈ S
⊢ x✝ ∈ εNFA.step (toεNFA M) a✝¹ (some s) ↔ x✝ ∈ step M a✝¹ s
[PROOFSTEP]
rfl
[GOAL]
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
⊢ εNFA.accepts (toεNFA M) = accepts M
[PROOFSTEP]
rw [εNFA.accepts, εNFA.eval, toεNFA_evalFrom_match]
[GOAL]
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
M : NFA α σ
⊢ {x | ∃ S, S ∈ (toεNFA M).accept ∧ S ∈ evalFrom M (toεNFA M).start x} = accepts M
[PROOFSTEP]
rfl


[GOAL]
n : ℕ
⊢ ack 0 n = n + 1
[PROOFSTEP]
rw [ack]
[GOAL]
m : ℕ
⊢ ack (m + 1) 0 = ack m 1
[PROOFSTEP]
rw [ack]
[GOAL]
m n : ℕ
⊢ ack (m + 1) (n + 1) = ack m (ack (m + 1) n)
[PROOFSTEP]
rw [ack]
[GOAL]
n : ℕ
⊢ ack 1 n = n + 2
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
⊢ ack 1 zero = zero + 2
[PROOFSTEP]
rfl
[GOAL]
case succ
n : ℕ
IH : ack 1 n = n + 2
⊢ ack 1 (succ n) = succ n + 2
[PROOFSTEP]
simp [IH]
[GOAL]
n : ℕ
⊢ ack 2 n = 2 * n + 3
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
⊢ ack 2 zero = 2 * zero + 3
[PROOFSTEP]
rfl
[GOAL]
case succ
n : ℕ
IH : ack 2 n = 2 * n + 3
⊢ ack 2 (succ n) = 2 * succ n + 3
[PROOFSTEP]
simpa [mul_succ]
[GOAL]
n : ℕ
⊢ ack 3 n = 2 ^ (n + 3) - 3
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
⊢ ack 3 zero = 2 ^ (zero + 3) - 3
[PROOFSTEP]
rfl
[GOAL]
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ ack 3 (succ n) = 2 ^ (succ n + 3) - 3
[PROOFSTEP]
rw [ack_succ_succ, IH, ack_two, Nat.succ_add, Nat.pow_succ 2 (n + 3), mul_comm _ 2, Nat.mul_sub_left_distrib, ←
  Nat.sub_add_comm, two_mul 3, Nat.add_sub_add_right]
[GOAL]
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 3 ≤ 2 * 2 ^ (n + 3)
[PROOFSTEP]
have H : 2 * 3 ≤ 2 * 2 ^ 3 := by norm_num
[GOAL]
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 3 ≤ 2 * 2 ^ 3
[PROOFSTEP]
norm_num
[GOAL]
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
H : 2 * 3 ≤ 2 * 2 ^ 3
⊢ 2 * 3 ≤ 2 * 2 ^ (n + 3)
[PROOFSTEP]
apply H.trans
[GOAL]
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
H : 2 * 3 ≤ 2 * 2 ^ 3
⊢ 2 * 2 ^ 3 ≤ 2 * 2 ^ (n + 3)
[PROOFSTEP]
simp [pow_le_pow]
[GOAL]
n : ℕ
⊢ 0 < ack 0 n
[PROOFSTEP]
simp
[GOAL]
m : ℕ
⊢ 0 < ack (m + 1) 0
[PROOFSTEP]
rw [ack_succ_zero]
[GOAL]
m : ℕ
⊢ 0 < ack m 1
[PROOFSTEP]
apply ack_pos
[GOAL]
m n : ℕ
⊢ 0 < ack (m + 1) (n + 1)
[PROOFSTEP]
rw [ack_succ_succ]
[GOAL]
m n : ℕ
⊢ 0 < ack m (ack (m + 1) n)
[PROOFSTEP]
apply ack_pos
[GOAL]
n : ℕ
⊢ 1 < ack (0 + 1) n
[PROOFSTEP]
simp
[GOAL]
m : ℕ
⊢ 1 < ack (m + 1 + 1) 0
[PROOFSTEP]
rw [ack_succ_zero]
[GOAL]
m : ℕ
⊢ 1 < ack (m + 1) 1
[PROOFSTEP]
apply one_lt_ack_succ_left
[GOAL]
m n : ℕ
⊢ 1 < ack (m + 1 + 1) (n + 1)
[PROOFSTEP]
rw [ack_succ_succ]
[GOAL]
m n : ℕ
⊢ 1 < ack (m + 1) (ack (m + 1 + 1) n)
[PROOFSTEP]
apply one_lt_ack_succ_left
[GOAL]
n : ℕ
⊢ 1 < ack 0 (n + 1)
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
⊢ 1 < ack (m + 1) (n + 1)
[PROOFSTEP]
rw [ack_succ_succ]
[GOAL]
m n : ℕ
⊢ 1 < ack m (ack (m + 1) n)
[PROOFSTEP]
cases' exists_eq_succ_of_ne_zero (ack_pos (m + 1) n).ne' with h h
[GOAL]
case intro
m n h✝ : ℕ
h : ack (m + 1) n = succ h✝
⊢ 1 < ack m (ack (m + 1) n)
[PROOFSTEP]
rw [h]
[GOAL]
case intro
m n h✝ : ℕ
h : ack (m + 1) n = succ h✝
⊢ 1 < ack m (succ h✝)
[PROOFSTEP]
apply one_lt_ack_succ_right
[GOAL]
n₁ n₂ : ℕ
h : n₁ < n₂
⊢ ack 0 n₁ < ack 0 n₂
[PROOFSTEP]
simpa using h
[GOAL]
m n : ℕ
_h : 0 < n + 1
⊢ ack (m + 1) 0 < ack (m + 1) (n + 1)
[PROOFSTEP]
rw [ack_succ_zero, ack_succ_succ]
[GOAL]
m n : ℕ
_h : 0 < n + 1
⊢ ack m 1 < ack m (ack (m + 1) n)
[PROOFSTEP]
exact ack_strictMono_right _ (one_lt_ack_succ_left m n)
[GOAL]
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack (m + 1) (n₁ + 1) < ack (m + 1) (n₂ + 1)
[PROOFSTEP]
rw [ack_succ_succ, ack_succ_succ]
[GOAL]
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack m (ack (m + 1) n₁) < ack m (ack (m + 1) n₂)
[PROOFSTEP]
apply ack_strictMono_right _ (ack_strictMono_right _ _)
[GOAL]
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ n₁ < n₂
[PROOFSTEP]
rwa [add_lt_add_iff_right] at h
[GOAL]
n : ℕ
⊢ 0 + n < ack 0 n
[PROOFSTEP]
simp
[GOAL]
m : ℕ
⊢ m + 1 + 0 < ack (m + 1) 0
[PROOFSTEP]
simpa using add_lt_ack m 1
[GOAL]
m n : ℕ
⊢ m + 1 + n + 1 ≤ m + (m + n + 2)
[PROOFSTEP]
linarith
[GOAL]
m n : ℕ
⊢ m + n + 2 = succ (m + 1 + n)
[PROOFSTEP]
rw [succ_eq_add_one]
[GOAL]
m n : ℕ
⊢ m + n + 2 = m + 1 + n + 1
[PROOFSTEP]
ring_nf
[GOAL]
m : ℕ
_h : 0 < m + 1
⊢ ack 0 0 < ack (m + 1) 0
[PROOFSTEP]
simpa using one_lt_ack_succ_right m 0
[GOAL]
m n : ℕ
h : 0 < m + 1
⊢ ack 0 (n + 1) < ack (m + 1) (n + 1)
[PROOFSTEP]
rw [ack_zero, ack_succ_succ]
[GOAL]
m n : ℕ
h : 0 < m + 1
⊢ n + 1 + 1 < ack m (ack (m + 1) n)
[PROOFSTEP]
apply lt_of_le_of_lt (le_trans _ <| add_le_add_left (add_add_one_le_ack _ _) m) (add_lt_ack _ _)
[GOAL]
m n : ℕ
h : 0 < m + 1
⊢ n + 1 + 1 ≤ m + (m + 1 + n + 1)
[PROOFSTEP]
linarith
[GOAL]
m₁ m₂ : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack (m₁ + 1) 0 < ack (m₂ + 1) 0
[PROOFSTEP]
simpa using ack_strict_mono_left' 1 ((add_lt_add_iff_right 1).1 h)
[GOAL]
m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack (m₁ + 1) (n + 1) < ack (m₂ + 1) (n + 1)
[PROOFSTEP]
rw [ack_succ_succ, ack_succ_succ]
[GOAL]
m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack m₁ (ack (m₁ + 1) n) < ack m₂ (ack (m₂ + 1) n)
[PROOFSTEP]
exact
  (ack_strict_mono_left' _ <| (add_lt_add_iff_right 1).1 h).trans (ack_strictMono_right _ <| ack_strict_mono_left' n h)
[GOAL]
m n : ℕ
⊢ ack m (n + 1) ≤ ack (m + 1) n
[PROOFSTEP]
cases' n with n n
[GOAL]
case zero
m : ℕ
⊢ ack m (zero + 1) ≤ ack (m + 1) zero
[PROOFSTEP]
simp
[GOAL]
case succ
m n : ℕ
⊢ ack m (succ n + 1) ≤ ack (m + 1) (succ n)
[PROOFSTEP]
rw [ack_succ_succ, succ_eq_add_one]
[GOAL]
case succ
m n : ℕ
⊢ ack m (n + 1 + 1) ≤ ack m (ack (m + 1) n)
[PROOFSTEP]
apply ack_mono_right m (le_trans _ <| add_add_one_le_ack _ n)
[GOAL]
m n : ℕ
⊢ n + 1 + 1 ≤ m + 1 + n + 1
[PROOFSTEP]
linarith
[GOAL]
n : ℕ
⊢ n ^ 2 ≤ 2 ^ (n + 1) - 3
[PROOFSTEP]
induction' n with k hk
[GOAL]
case zero
⊢ zero ^ 2 ≤ 2 ^ (zero + 1) - 3
[PROOFSTEP]
norm_num
[GOAL]
case succ
k : ℕ
hk : k ^ 2 ≤ 2 ^ (k + 1) - 3
⊢ succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
[PROOFSTEP]
cases' k with k k
[GOAL]
case succ.zero
hk : zero ^ 2 ≤ 2 ^ (zero + 1) - 3
⊢ succ zero ^ 2 ≤ 2 ^ (succ zero + 1) - 3
[PROOFSTEP]
norm_num
[GOAL]
case succ.succ
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ succ (succ k) ^ 2 ≤ 2 ^ (succ (succ k) + 1) - 3
[PROOFSTEP]
rw [succ_eq_add_one, add_sq, Nat.pow_succ 2, mul_comm _ 2, two_mul (2 ^ _), add_tsub_assoc_of_le, add_comm (2 ^ _),
  add_assoc]
[GOAL]
case succ.succ
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ (k + 1) ^ 2 + (2 * (k + 1) * 1 + 1 ^ 2) ≤ 2 ^ (k + 2) - 3 + 2 ^ (k + 2)
[PROOFSTEP]
apply Nat.add_le_add hk
[GOAL]
case succ.succ
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ 2 * (k + 1) * 1 + 1 ^ 2 ≤ 2 ^ (k + 2)
[PROOFSTEP]
norm_num
[GOAL]
case succ.succ
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ 2 * (k + 1) + 1 ≤ 2 ^ (k + 2)
[PROOFSTEP]
apply succ_le_of_lt
[GOAL]
case succ.succ.h
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ 2 * (k + 1) < 2 ^ (k + 2)
[PROOFSTEP]
rw [Nat.pow_succ, mul_comm _ 2, mul_lt_mul_left (zero_lt_two' ℕ)]
[GOAL]
case succ.succ.h
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ k + 1 < 2 ^ (k + 1)
[PROOFSTEP]
apply lt_two_pow
[GOAL]
case succ.succ.h
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ 3 ≤ 2 ^ (k + 2)
[PROOFSTEP]
rw [Nat.pow_succ, Nat.pow_succ]
[GOAL]
case succ.succ.h
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ 3 ≤ 2 ^ k * 2 * 2
[PROOFSTEP]
linarith [one_le_pow k 2 zero_lt_two]
[GOAL]
n : ℕ
⊢ (ack 0 n + 1) ^ 2 ≤ ack (0 + 3) n
[PROOFSTEP]
simpa using sq_le_two_pow_add_one_minus_three (n + 2)
[GOAL]
m : ℕ
⊢ (ack (m + 1) 0 + 1) ^ 2 ≤ ack (m + 1 + 3) 0
[PROOFSTEP]
rw [ack_succ_zero, ack_succ_zero]
[GOAL]
m : ℕ
⊢ (ack m 1 + 1) ^ 2 ≤ ack (m + 3) 1
[PROOFSTEP]
apply ack_add_one_sq_lt_ack_add_three
[GOAL]
m n : ℕ
⊢ (ack (m + 1) (n + 1) + 1) ^ 2 ≤ ack (m + 1 + 3) (n + 1)
[PROOFSTEP]
rw [ack_succ_succ, ack_succ_succ]
[GOAL]
m n : ℕ
⊢ (ack m (ack (m + 1) n) + 1) ^ 2 ≤ ack (m + 3) (ack (m + 3 + 1) n)
[PROOFSTEP]
apply (ack_add_one_sq_lt_ack_add_three _ _).trans (ack_mono_right _ <| ack_mono_left _ _)
[GOAL]
m n : ℕ
⊢ m + 1 ≤ m + 3 + 1
[PROOFSTEP]
linarith
[GOAL]
m n : ℕ
⊢ m ≤ m + 2
[PROOFSTEP]
linarith
[GOAL]
f : ℕ → ℕ
hf : Nat.Primrec f
⊢ ∃ m, ∀ (n : ℕ), f n < ack m n
[PROOFSTEP]
induction' hf with f g hf hg IHf IHg f g hf hg IHf IHg f g hf hg IHf IHg
[GOAL]
case zero
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), (fun x => 0) n < ack m n
[PROOFSTEP]
exact
  ⟨0, ack_pos 0⟩
    -- Successor function:
[GOAL]
case succ
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), succ n < ack m n
[PROOFSTEP]
refine' ⟨1, fun n => _⟩
[GOAL]
case succ
f : ℕ → ℕ
n : ℕ
⊢ succ n < ack 1 n
[PROOFSTEP]
rw [succ_eq_one_add]
[GOAL]
case succ
f : ℕ → ℕ
n : ℕ
⊢ 1 + n < ack 1 n
[PROOFSTEP]
apply add_lt_ack
[GOAL]
case left
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), (fun n => (unpair n).fst) n < ack m n
[PROOFSTEP]
refine' ⟨0, fun n => _⟩
[GOAL]
case left
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).fst) n < ack 0 n
[PROOFSTEP]
rw [ack_zero, lt_succ_iff]
[GOAL]
case left
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).fst) n ≤ n
[PROOFSTEP]
exact unpair_left_le n
[GOAL]
case right
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), (fun n => (unpair n).snd) n < ack m n
[PROOFSTEP]
refine' ⟨0, fun n => _⟩
[GOAL]
case right
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).snd) n < ack 0 n
[PROOFSTEP]
rw [ack_zero, lt_succ_iff]
[GOAL]
case right
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).snd) n ≤ n
[PROOFSTEP]
exact unpair_right_le n
[GOAL]
case pair
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHf : ∃ m, ∀ (n : ℕ), f n < ack m n
IHg : ∃ m, ∀ (n : ℕ), g n < ack m n
⊢ ∃ m, ∀ (n : ℕ), (fun n => pair (f n) (g n)) n < ack m n
case comp
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHf : ∃ m, ∀ (n : ℕ), f n < ack m n
IHg : ∃ m, ∀ (n : ℕ), g n < ack m n
⊢ ∃ m, ∀ (n : ℕ), (fun n => f (g n)) n < ack m n
case prec
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHf : ∃ m, ∀ (n : ℕ), f n < ack m n
IHg : ∃ m, ∀ (n : ℕ), g n < ack m n
⊢ ∃ m, ∀ (n : ℕ), unpaired (fun z n => rec (f z) (fun y IH => g (pair z (pair y IH))) n) n < ack m n
[PROOFSTEP]
all_goals cases' IHf with a ha; cases' IHg with b hb
[GOAL]
case pair
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHf : ∃ m, ∀ (n : ℕ), f n < ack m n
IHg : ∃ m, ∀ (n : ℕ), g n < ack m n
⊢ ∃ m, ∀ (n : ℕ), (fun n => pair (f n) (g n)) n < ack m n
[PROOFSTEP]
cases' IHf with a ha
[GOAL]
case pair.intro
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHg : ∃ m, ∀ (n : ℕ), g n < ack m n
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
⊢ ∃ m, ∀ (n : ℕ), (fun n => pair (f n) (g n)) n < ack m n
[PROOFSTEP]
cases' IHg with b hb
[GOAL]
case comp
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHf : ∃ m, ∀ (n : ℕ), f n < ack m n
IHg : ∃ m, ∀ (n : ℕ), g n < ack m n
⊢ ∃ m, ∀ (n : ℕ), (fun n => f (g n)) n < ack m n
[PROOFSTEP]
cases' IHf with a ha
[GOAL]
case comp.intro
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHg : ∃ m, ∀ (n : ℕ), g n < ack m n
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
⊢ ∃ m, ∀ (n : ℕ), (fun n => f (g n)) n < ack m n
[PROOFSTEP]
cases' IHg with b hb
[GOAL]
case prec
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHf : ∃ m, ∀ (n : ℕ), f n < ack m n
IHg : ∃ m, ∀ (n : ℕ), g n < ack m n
⊢ ∃ m, ∀ (n : ℕ), unpaired (fun z n => rec (f z) (fun y IH => g (pair z (pair y IH))) n) n < ack m n
[PROOFSTEP]
cases' IHf with a ha
[GOAL]
case prec.intro
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHg : ∃ m, ∀ (n : ℕ), g n < ack m n
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
⊢ ∃ m, ∀ (n : ℕ), unpaired (fun z n => rec (f z) (fun y IH => g (pair z (pair y IH))) n) n < ack m n
[PROOFSTEP]
cases' IHg with b hb
[GOAL]
case pair.intro.intro
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
⊢ ∃ m, ∀ (n : ℕ), (fun n => pair (f n) (g n)) n < ack m n
[PROOFSTEP]
refine'
  ⟨max a b + 3, fun n =>
    (pair_lt_max_add_one_sq _ _).trans_le <|
      (pow_le_pow_of_le_left (add_le_add_right _ _) 2).trans <| ack_add_one_sq_lt_ack_add_three _ _⟩
[GOAL]
case pair.intro.intro
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
n : ℕ
⊢ max (f n) (g n) ≤ ack (max a b) n
[PROOFSTEP]
rw [max_ack_left]
[GOAL]
case pair.intro.intro
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
n : ℕ
⊢ max (f n) (g n) ≤ max (ack a n) (ack b n)
[PROOFSTEP]
exact max_le_max (ha n).le (hb n).le
[GOAL]
case comp.intro.intro
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
⊢ ∃ m, ∀ (n : ℕ), (fun n => f (g n)) n < ack m n
[PROOFSTEP]
exact
  ⟨max a b + 2, fun n => (ha _).trans <| (ack_strictMono_right a <| hb n).trans <| ack_ack_lt_ack_max_add_two a b n⟩
    -- Primitive recursion operator:
[GOAL]
case prec.intro.intro
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
⊢ ∃ m, ∀ (n : ℕ), unpaired (fun z n => rec (f z) (fun y IH => g (pair z (pair y IH))) n) n < ack m n
[PROOFSTEP]
have : ∀ {m n}, rec (f m) (fun y IH => g <| pair m <| pair y IH) n < ack (max a b + 9) (m + n) :=
  by
  intro m n
  induction' n with n IH
  · apply (ha m).trans (ack_strictMono_left m <| (le_max_left a b).trans_lt _)
    linarith
  ·
    -- We get rid of the first `pair`.
    simp only [ge_iff_le]
    apply
      (hb _).trans
        ((ack_pair_lt _ _ _).trans_le _)
          -- If m is the maximum, we get a very weak inequality.
    cases' lt_or_le _ m with h₁ h₁
    · rw [max_eq_left h₁.le]
      exact ack_le_ack (Nat.add_le_add (le_max_right a b) <| by norm_num) (self_le_add_right m _)
    rw [max_eq_right h₁]
      -- We get rid of the second `pair`.
    apply (ack_pair_lt _ _ _).le.trans
    cases' lt_or_le _ n with h₂ h₂
    · rw [max_eq_left h₂.le, add_assoc]
      exact ack_le_ack (Nat.add_le_add (le_max_right a b) <| by norm_num) ((le_succ n).trans <| self_le_add_left _ _)
    rw [max_eq_right h₂]
      -- We now use the inductive hypothesis, and some simple algebraic manipulation.
    apply (ack_strictMono_right _ IH).le.trans
    rw [add_succ m, add_succ _ 8, succ_eq_add_one, succ_eq_add_one, ack_succ_succ (_ + 8), add_assoc]
    exact
      ack_mono_left _
        (Nat.add_le_add (le_max_right a b) le_rfl)
          -- The proof is now simple.
[GOAL]
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
⊢ ∀ {m n : ℕ}, rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
[PROOFSTEP]
intro m n
[GOAL]
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
⊢ rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m : ℕ
⊢ rec (f m) (fun y IH => g (pair m (pair y IH))) zero < ack (max a b + 9) (m + zero)
[PROOFSTEP]
apply (ha m).trans (ack_strictMono_left m <| (le_max_left a b).trans_lt _)
[GOAL]
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m : ℕ
⊢ max a b < max a b + 9
[PROOFSTEP]
linarith
[GOAL]
case succ
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
⊢ rec (f m) (fun y IH => g (pair m (pair y IH))) (succ n) < ack (max a b + 9) (m + succ n)
[PROOFSTEP]
simp only [ge_iff_le]
[GOAL]
case succ
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
⊢ g (pair m (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n))) < ack (max a b + 9) (m + succ n)
[PROOFSTEP]
apply
  (hb _).trans
    ((ack_pair_lt _ _ _).trans_le _)
      -- If m is the maximum, we get a very weak inequality.
[GOAL]
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
⊢ ack (b + 4) (max m (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n))) ≤ ack (max a b + 9) (m + succ n)
[PROOFSTEP]
cases' lt_or_le _ m with h₁ h₁
[GOAL]
case inl
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : ?m.127608 < m
⊢ ack (b + 4) (max m (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n))) ≤ ack (max a b + 9) (m + succ n)
[PROOFSTEP]
rw [max_eq_left h₁.le]
[GOAL]
case inl
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n) < m
⊢ ack (b + 4) m ≤ ack (max a b + 9) (m + succ n)
[PROOFSTEP]
exact ack_le_ack (Nat.add_le_add (le_max_right a b) <| by norm_num) (self_le_add_right m _)
[GOAL]
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n) < m
⊢ 4 ≤ 9
[PROOFSTEP]
norm_num
[GOAL]
case inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
⊢ ack (b + 4) (max m (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n))) ≤ ack (max a b + 9) (m + succ n)
[PROOFSTEP]
rw [max_eq_right h₁]
  -- We get rid of the second `pair`.
[GOAL]
case inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
⊢ ack (b + 4) (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (max a b + 9) (m + succ n)
[PROOFSTEP]
apply (ack_pair_lt _ _ _).le.trans
[GOAL]
case inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
⊢ ack (b + 4 + 4) (max n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (max a b + 9) (m + succ n)
[PROOFSTEP]
cases' lt_or_le _ n with h₂ h₂
[GOAL]
case inr.inl
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : ?m.127977 < n
⊢ ack (b + 4 + 4) (max n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (max a b + 9) (m + succ n)
[PROOFSTEP]
rw [max_eq_left h₂.le, add_assoc]
[GOAL]
case inr.inl
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : rec (f m) (fun y IH => g (pair m (pair y IH))) n < n
⊢ ack (b + (4 + 4)) n ≤ ack (max a b + 9) (m + succ n)
[PROOFSTEP]
exact ack_le_ack (Nat.add_le_add (le_max_right a b) <| by norm_num) ((le_succ n).trans <| self_le_add_left _ _)
[GOAL]
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : rec (f m) (fun y IH => g (pair m (pair y IH))) n < n
⊢ 4 + 4 ≤ 9
[PROOFSTEP]
norm_num
[GOAL]
case inr.inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH => g (pair m (pair y IH))) n
⊢ ack (b + 4 + 4) (max n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (max a b + 9) (m + succ n)
[PROOFSTEP]
rw [max_eq_right h₂]
  -- We now use the inductive hypothesis, and some simple algebraic manipulation.
[GOAL]
case inr.inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH => g (pair m (pair y IH))) n
⊢ ack (b + 4 + 4) (rec (f m) (fun y IH => g (pair m (pair y IH))) n) ≤ ack (max a b + 9) (m + succ n)
[PROOFSTEP]
apply (ack_strictMono_right _ IH).le.trans
[GOAL]
case inr.inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH => g (pair m (pair y IH))) n
⊢ ack (b + 4 + 4) (ack (max a b + 9) (m + n)) ≤ ack (max a b + 9) (m + succ n)
[PROOFSTEP]
rw [add_succ m, add_succ _ 8, succ_eq_add_one, succ_eq_add_one, ack_succ_succ (_ + 8), add_assoc]
[GOAL]
case inr.inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH => g (pair m (pair y IH))) n
⊢ ack (b + (4 + 4)) (ack (max a b + 8 + 1) (m + n)) ≤ ack (max a b + 8) (ack (max a b + 8 + 1) (m + n))
[PROOFSTEP]
exact
  ack_mono_left _
    (Nat.add_le_add (le_max_right a b) le_rfl)
      -- The proof is now simple.
[GOAL]
case prec.intro.intro
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
this : ∀ {m n : ℕ}, rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
⊢ ∃ m, ∀ (n : ℕ), unpaired (fun z n => rec (f z) (fun y IH => g (pair z (pair y IH))) n) n < ack m n
[PROOFSTEP]
exact ⟨max a b + 9, fun n => this.trans_le <| ack_mono_right _ <| unpair_add_le n⟩
[GOAL]
h : Nat.Primrec fun n => ack n n
⊢ False
[PROOFSTEP]
cases' exists_lt_ack_of_nat_primrec h with m hm
[GOAL]
case intro
h : Nat.Primrec fun n => ack n n
m : ℕ
hm : ∀ (n : ℕ), ack n n < ack m n
⊢ False
[PROOFSTEP]
exact (hm m).false
[GOAL]
⊢ ¬Primrec fun n => ack n n
[PROOFSTEP]
rw [Primrec.nat_iff]
[GOAL]
⊢ ¬Nat.Primrec fun n => ack n n
[PROOFSTEP]
exact not_nat_primrec_ack_self


[GOAL]
Ω : Type u_1
inst✝ : MeasurableSpace Ω
⊢ condCount ∅ = 0
[PROOFSTEP]
simp [condCount]
[GOAL]
Ω : Type u_1
inst✝ : MeasurableSpace Ω
s : Set Ω
⊢ ↑↑(condCount s) ∅ = 0
[PROOFSTEP]
simp
[GOAL]
Ω : Type u_1
inst✝ : MeasurableSpace Ω
s t : Set Ω
h : ↑↑(condCount s) t ≠ 0
⊢ Set.Finite s
[PROOFSTEP]
by_contra hs'
[GOAL]
Ω : Type u_1
inst✝ : MeasurableSpace Ω
s t : Set Ω
h : ↑↑(condCount s) t ≠ 0
hs' : ¬Set.Finite s
⊢ False
[PROOFSTEP]
simp [condCount, cond, Measure.count_apply_infinite hs'] at h
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ ↑↑(condCount Set.univ) s = ↑↑Measure.count s / ↑(Fintype.card Ω)
[PROOFSTEP]
rw [condCount, cond_apply _ MeasurableSet.univ, ← ENNReal.div_eq_inv_mul, Set.univ_inter]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ ↑↑Measure.count s / ↑↑Measure.count Set.univ = ↑↑Measure.count s / ↑(Fintype.card Ω)
[PROOFSTEP]
congr
[GOAL]
case e_a
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ ↑↑Measure.count Set.univ = ↑(Fintype.card Ω)
[PROOFSTEP]
rw [← Finset.coe_univ, Measure.count_apply, Finset.univ.tsum_subtype' fun _ => (1 : ENNReal)]
[GOAL]
case e_a
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ (Finset.sum Finset.univ fun x => 1) = ↑(Fintype.card Ω)
[PROOFSTEP]
simp [Finset.card_univ]
[GOAL]
case e_a
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : Fintype Ω
s : Set Ω
⊢ MeasurableSet ↑Finset.univ
[PROOFSTEP]
exact (@Finset.coe_univ Ω _).symm ▸ MeasurableSet.univ
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑(condCount s) Set.univ = 1
[PROOFSTEP]
rw [condCount, cond_apply _ hs.measurableSet, Set.inter_univ, ENNReal.inv_mul_cancel]
[GOAL]
case h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑Measure.count s ≠ 0
[PROOFSTEP]
exact fun h => hs'.ne_empty <| Measure.empty_of_count_eq_zero h
[GOAL]
case ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑Measure.count s ≠ ⊤
[PROOFSTEP]
exact (Measure.count_apply_lt_top.2 hs).ne
[GOAL]
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
⊢ ↑↑(condCount {ω}) t = if ω ∈ t then 1 else 0
[PROOFSTEP]
rw [condCount, cond_apply _ (measurableSet_singleton ω), Measure.count_singleton, inv_one, one_mul]
[GOAL]
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
⊢ ↑↑Measure.count ({ω} ∩ t) = if ω ∈ t then 1 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ω ∈ t
⊢ ↑↑Measure.count ({ω} ∩ t) = 1
[PROOFSTEP]
rw [(by simpa : ({ ω } : Set Ω) ∩ t = { ω }), Measure.count_singleton]
[GOAL]
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ω ∈ t
⊢ {ω} ∩ t = {ω}
[PROOFSTEP]
simpa
[GOAL]
case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ¬ω ∈ t
⊢ ↑↑Measure.count ({ω} ∩ t) = 0
[PROOFSTEP]
rw [(by simpa : ({ ω } : Set Ω) ∩ t = ∅), Measure.count_empty]
[GOAL]
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ¬ω ∈ t
⊢ {ω} ∩ t = ∅
[PROOFSTEP]
simpa
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount s) (s ∩ t) = ↑↑(condCount s) t
[PROOFSTEP]
rw [condCount, cond_inter_self _ hs.measurableSet]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑(condCount s) s = 1
[PROOFSTEP]
rw [condCount, cond_apply _ hs.measurableSet, Set.inter_self, ENNReal.inv_mul_cancel]
[GOAL]
case h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑Measure.count s ≠ 0
[PROOFSTEP]
exact fun h => hs'.ne_empty <| Measure.empty_of_count_eq_zero h
[GOAL]
case ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑Measure.count s ≠ ⊤
[PROOFSTEP]
exact (Measure.count_apply_lt_top.2 hs).ne
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
ht : s ⊆ t
⊢ ↑↑(condCount s) t = 1
[PROOFSTEP]
haveI := condCount_isProbabilityMeasure hs hs'
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
ht : s ⊆ t
this : IsProbabilityMeasure (condCount s)
⊢ ↑↑(condCount s) t = 1
[PROOFSTEP]
refine' eq_of_le_of_not_lt prob_le_one _
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
ht : s ⊆ t
this : IsProbabilityMeasure (condCount s)
⊢ ¬↑↑(condCount s) t < 1
[PROOFSTEP]
rw [not_lt, ← condCount_self hs hs']
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
ht : s ⊆ t
this : IsProbabilityMeasure (condCount s)
⊢ ↑↑(condCount s) s ≤ ↑↑(condCount s) t
[PROOFSTEP]
exact measure_mono ht
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑(condCount s) t = 1
⊢ s ⊆ t
[PROOFSTEP]
have hsf := finite_of_condCount_ne_zero (by rw [h]; exact one_ne_zero)
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑(condCount s) t = 1
⊢ ↑↑(condCount ?m.9273) ?m.9274 ≠ 0
[PROOFSTEP]
rw [h]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑(condCount s) t = 1
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑(condCount s) t = 1
hsf : Set.Finite s
⊢ s ⊆ t
[PROOFSTEP]
rw [condCount, cond_apply _ hsf.measurableSet, mul_comm] at h
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑Measure.count (s ∩ t) * (↑↑Measure.count s)⁻¹ = 1
hsf : Set.Finite s
⊢ s ⊆ t
[PROOFSTEP]
replace h := ENNReal.eq_inv_of_mul_eq_one_left h
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : ↑↑Measure.count (s ∩ t) = (↑↑Measure.count s)⁻¹⁻¹
⊢ s ⊆ t
[PROOFSTEP]
rw [inv_inv, Measure.count_apply_finite _ hsf, Measure.count_apply_finite _ (hsf.inter_of_left _), Nat.cast_inj] at h
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : Finset.card (Set.Finite.toFinset (_ : Set.Finite (s ∩ t))) = Finset.card (Set.Finite.toFinset hsf)
⊢ s ⊆ t
[PROOFSTEP]
suffices s ∩ t = s by exact this ▸ fun x hx => hx.2
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : Finset.card (Set.Finite.toFinset (_ : Set.Finite (s ∩ t))) = Finset.card (Set.Finite.toFinset hsf)
this : s ∩ t = s
⊢ s ⊆ t
[PROOFSTEP]
exact this ▸ fun x hx => hx.2
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : Finset.card (Set.Finite.toFinset (_ : Set.Finite (s ∩ t))) = Finset.card (Set.Finite.toFinset hsf)
⊢ s ∩ t = s
[PROOFSTEP]
rw [← @Set.Finite.toFinset_inj _ _ _ (hsf.inter_of_left _) hsf]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : Finset.card (Set.Finite.toFinset (_ : Set.Finite (s ∩ t))) = Finset.card (Set.Finite.toFinset hsf)
⊢ Set.Finite.toFinset (_ : Set.Finite (s ∩ t)) = Set.Finite.toFinset hsf
[PROOFSTEP]
exact Finset.eq_of_subset_of_card_le (Set.Finite.toFinset_mono <| s.inter_subset_left t) h.ge
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount s) t = 0 ↔ s ∩ t = ∅
[PROOFSTEP]
simp [condCount, cond_apply _ hs.measurableSet, Measure.count_apply_eq_top, Set.not_infinite.2 hs,
  Measure.count_apply_finite _ (hs.inter_of_left _)]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount s) (t ∩ u) = ↑↑(condCount (s ∩ t)) u * ↑↑(condCount s) t
[PROOFSTEP]
by_cases hst : s ∩ t = ∅
[GOAL]
case pos
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hst : s ∩ t = ∅
⊢ ↑↑(condCount s) (t ∩ u) = ↑↑(condCount (s ∩ t)) u * ↑↑(condCount s) t
[PROOFSTEP]
rw [hst, condCount_empty_meas, Measure.coe_zero, Pi.zero_apply, zero_mul, condCount_eq_zero_iff hs, ← Set.inter_assoc,
  hst, Set.empty_inter]
[GOAL]
case neg
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hst : ¬s ∩ t = ∅
⊢ ↑↑(condCount s) (t ∩ u) = ↑↑(condCount (s ∩ t)) u * ↑↑(condCount s) t
[PROOFSTEP]
rw [condCount, condCount, cond_apply _ hs.measurableSet, cond_apply _ hs.measurableSet,
  cond_apply _ (hs.inter_of_left _).measurableSet, mul_comm _ (Measure.count (s ∩ t)), ← mul_assoc,
  mul_comm _ (Measure.count (s ∩ t)), ← mul_assoc, ENNReal.mul_inv_cancel, one_mul, mul_comm, Set.inter_assoc]
[GOAL]
case neg.h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hst : ¬s ∩ t = ∅
⊢ ↑↑Measure.count (s ∩ t) ≠ 0
[PROOFSTEP]
rwa [← Measure.count_eq_zero_iff] at hst
[GOAL]
case neg.ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
hst : ¬s ∩ t = ∅
⊢ ↑↑Measure.count (s ∩ t) ≠ ⊤
[PROOFSTEP]
exact (Measure.count_apply_lt_top.2 <| hs.inter_of_left _).ne
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount s) (t ∩ u) = ↑↑(condCount (s ∩ u)) t * ↑↑(condCount s) u
[PROOFSTEP]
rw [← Set.inter_comm]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount s) (u ∩ t) = ↑↑(condCount (s ∩ u)) t * ↑↑(condCount s) u
[PROOFSTEP]
exact condCount_inter hs
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
htu : Disjoint t u
⊢ ↑↑(condCount s) (t ∪ u) = ↑↑(condCount s) t + ↑↑(condCount s) u
[PROOFSTEP]
rw [condCount, cond_apply _ hs.measurableSet, cond_apply _ hs.measurableSet, cond_apply _ hs.measurableSet,
  Set.inter_union_distrib_left, measure_union, mul_add]
[GOAL]
case hd
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
htu : Disjoint t u
⊢ Disjoint (s ∩ t) (s ∩ u)
case h
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
htu : Disjoint t u
⊢ MeasurableSet (s ∩ u)
[PROOFSTEP]
exacts [htu.mono inf_le_right inf_le_right, (hs.inter_of_left _).measurableSet]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t✝ u t : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
⊢ ↑↑(condCount s) t + ↑↑(condCount s) tᶜ = 1
[PROOFSTEP]
rw [← condCount_union hs disjoint_compl_right, Set.union_compl_self,
  (condCount_isProbabilityMeasure hs hs').measure_univ]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
⊢ ↑↑(condCount s) u * ↑↑(condCount (s ∪ t)) s + ↑↑(condCount t) u * ↑↑(condCount (s ∪ t)) t = ↑↑(condCount (s ∪ t)) u
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | hs')
[GOAL]
case inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
t u : Set Ω
ht : Set.Finite t
hs : Set.Finite ∅
hst : Disjoint ∅ t
⊢ ↑↑(condCount ∅) u * ↑↑(condCount (∅ ∪ t)) ∅ + ↑↑(condCount t) u * ↑↑(condCount (∅ ∪ t)) t = ↑↑(condCount (∅ ∪ t)) u
[PROOFSTEP]
rcases t.eq_empty_or_nonempty with (rfl | ht')
[GOAL]
case inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
⊢ ↑↑(condCount s) u * ↑↑(condCount (s ∪ t)) s + ↑↑(condCount t) u * ↑↑(condCount (s ∪ t)) t = ↑↑(condCount (s ∪ t)) u
[PROOFSTEP]
rcases t.eq_empty_or_nonempty with (rfl | ht')
[GOAL]
case inl.inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
u : Set Ω
hs ht : Set.Finite ∅
hst : Disjoint ∅ ∅
⊢ ↑↑(condCount ∅) u * ↑↑(condCount (∅ ∪ ∅)) ∅ + ↑↑(condCount ∅) u * ↑↑(condCount (∅ ∪ ∅)) ∅ = ↑↑(condCount (∅ ∪ ∅)) u
[PROOFSTEP]
simp
[GOAL]
case inl.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
t u : Set Ω
ht : Set.Finite t
hs : Set.Finite ∅
hst : Disjoint ∅ t
ht' : Set.Nonempty t
⊢ ↑↑(condCount ∅) u * ↑↑(condCount (∅ ∪ t)) ∅ + ↑↑(condCount t) u * ↑↑(condCount (∅ ∪ t)) t = ↑↑(condCount (∅ ∪ t)) u
[PROOFSTEP]
simp [condCount_self ht ht']
[GOAL]
case inr.inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u : Set Ω
hs : Set.Finite s
hs' : Set.Nonempty s
ht : Set.Finite ∅
hst : Disjoint s ∅
⊢ ↑↑(condCount s) u * ↑↑(condCount (s ∪ ∅)) s + ↑↑(condCount ∅) u * ↑↑(condCount (s ∪ ∅)) ∅ = ↑↑(condCount (s ∪ ∅)) u
[PROOFSTEP]
simp [condCount_self hs hs']
[GOAL]
case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ ↑↑(condCount s) u * ↑↑(condCount (s ∪ t)) s + ↑↑(condCount t) u * ↑↑(condCount (s ∪ t)) t = ↑↑(condCount (s ∪ t)) u
[PROOFSTEP]
rw [condCount, condCount, condCount, cond_apply _ hs.measurableSet, cond_apply _ ht.measurableSet,
  cond_apply _ (hs.union ht).measurableSet, cond_apply _ (hs.union ht).measurableSet,
  cond_apply _ (hs.union ht).measurableSet]
[GOAL]
case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ (↑↑Measure.count s)⁻¹ * ↑↑Measure.count (s ∩ u) * ((↑↑Measure.count (s ∪ t))⁻¹ * ↑↑Measure.count ((s ∪ t) ∩ s)) +
      (↑↑Measure.count t)⁻¹ * ↑↑Measure.count (t ∩ u) * ((↑↑Measure.count (s ∪ t))⁻¹ * ↑↑Measure.count ((s ∪ t) ∩ t)) =
    (↑↑Measure.count (s ∪ t))⁻¹ * ↑↑Measure.count ((s ∪ t) ∩ u)
[PROOFSTEP]
conv_lhs =>
  rw [Set.union_inter_cancel_left, Set.union_inter_cancel_right, mul_comm (Measure.count (s ∪ t))⁻¹,
    mul_comm (Measure.count (s ∪ t))⁻¹, ← mul_assoc, ← mul_assoc, mul_comm _ (Measure.count s),
    mul_comm _ (Measure.count t), ← mul_assoc, ← mul_assoc]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
| (↑↑Measure.count s)⁻¹ * ↑↑Measure.count (s ∩ u) * ((↑↑Measure.count (s ∪ t))⁻¹ * ↑↑Measure.count ((s ∪ t) ∩ s)) +
    (↑↑Measure.count t)⁻¹ * ↑↑Measure.count (t ∩ u) * ((↑↑Measure.count (s ∪ t))⁻¹ * ↑↑Measure.count ((s ∪ t) ∩ t))
[PROOFSTEP]
rw [Set.union_inter_cancel_left, Set.union_inter_cancel_right, mul_comm (Measure.count (s ∪ t))⁻¹,
    mul_comm (Measure.count (s ∪ t))⁻¹, ← mul_assoc, ← mul_assoc, mul_comm _ (Measure.count s),
    mul_comm _ (Measure.count t), ← mul_assoc, ← mul_assoc]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
| (↑↑Measure.count s)⁻¹ * ↑↑Measure.count (s ∩ u) * ((↑↑Measure.count (s ∪ t))⁻¹ * ↑↑Measure.count ((s ∪ t) ∩ s)) +
    (↑↑Measure.count t)⁻¹ * ↑↑Measure.count (t ∩ u) * ((↑↑Measure.count (s ∪ t))⁻¹ * ↑↑Measure.count ((s ∪ t) ∩ t))
[PROOFSTEP]
rw [Set.union_inter_cancel_left, Set.union_inter_cancel_right, mul_comm (Measure.count (s ∪ t))⁻¹,
    mul_comm (Measure.count (s ∪ t))⁻¹, ← mul_assoc, ← mul_assoc, mul_comm _ (Measure.count s),
    mul_comm _ (Measure.count t), ← mul_assoc, ← mul_assoc]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
| (↑↑Measure.count s)⁻¹ * ↑↑Measure.count (s ∩ u) * ((↑↑Measure.count (s ∪ t))⁻¹ * ↑↑Measure.count ((s ∪ t) ∩ s)) +
    (↑↑Measure.count t)⁻¹ * ↑↑Measure.count (t ∩ u) * ((↑↑Measure.count (s ∪ t))⁻¹ * ↑↑Measure.count ((s ∪ t) ∩ t))
[PROOFSTEP]
rw [Set.union_inter_cancel_left, Set.union_inter_cancel_right, mul_comm (Measure.count (s ∪ t))⁻¹,
  mul_comm (Measure.count (s ∪ t))⁻¹, ← mul_assoc, ← mul_assoc, mul_comm _ (Measure.count s),
  mul_comm _ (Measure.count t), ← mul_assoc, ← mul_assoc]
[GOAL]
case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ ↑↑Measure.count s * (↑↑Measure.count s)⁻¹ * ↑↑Measure.count (s ∩ u) * (↑↑Measure.count (s ∪ t))⁻¹ +
      ↑↑Measure.count t * (↑↑Measure.count t)⁻¹ * ↑↑Measure.count (t ∩ u) * (↑↑Measure.count (s ∪ t))⁻¹ =
    (↑↑Measure.count (s ∪ t))⁻¹ * ↑↑Measure.count ((s ∪ t) ∩ u)
[PROOFSTEP]
rw [ENNReal.mul_inv_cancel, ENNReal.mul_inv_cancel, one_mul, one_mul, ← add_mul, ← measure_union,
  Set.union_inter_distrib_right, mul_comm]
[GOAL]
case inr.inr.hd
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ Disjoint (s ∩ u) (t ∩ u)
case inr.inr.h
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ MeasurableSet (t ∩ u)
case inr.inr.h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ ↑↑Measure.count t ≠ 0
case inr.inr.ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ ↑↑Measure.count t ≠ ⊤
case inr.inr.h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ ↑↑Measure.count s ≠ 0
case inr.inr.ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : Set.Finite s
ht : Set.Finite t
hst : Disjoint s t
hs' : Set.Nonempty s
ht' : Set.Nonempty t
⊢ ↑↑Measure.count s ≠ ⊤
[PROOFSTEP]
exacts [hst.mono inf_le_left inf_le_left, (ht.inter_of_left _).measurableSet, Measure.count_ne_zero ht',
  (Measure.count_apply_lt_top.2 ht).ne, Measure.count_ne_zero hs', (Measure.count_apply_lt_top.2 hs).ne]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t✝ u✝ u t : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount (s ∩ u)) t * ↑↑(condCount s) u + ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount s) uᶜ = ↑↑(condCount s) t
[PROOFSTEP]
have :
  condCount s t =
    (condCount (s ∩ u) t * condCount (s ∩ u ∪ s ∩ uᶜ) (s ∩ u) +
      condCount (s ∩ uᶜ) t * condCount (s ∩ u ∪ s ∩ uᶜ) (s ∩ uᶜ)) :=
  by
  rw [condCount_disjoint_union (hs.inter_of_left _) (hs.inter_of_left _)
      (disjoint_compl_right.mono inf_le_right inf_le_right),
    Set.inter_union_compl]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t✝ u✝ u t : Set Ω
hs : Set.Finite s
⊢ ↑↑(condCount s) t =
    ↑↑(condCount (s ∩ u)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
[PROOFSTEP]
rw [condCount_disjoint_union (hs.inter_of_left _) (hs.inter_of_left _)
    (disjoint_compl_right.mono inf_le_right inf_le_right),
  Set.inter_union_compl]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t✝ u✝ u t : Set Ω
hs : Set.Finite s
this :
  ↑↑(condCount s) t =
    ↑↑(condCount (s ∩ u)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
⊢ ↑↑(condCount (s ∩ u)) t * ↑↑(condCount s) u + ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount s) uᶜ = ↑↑(condCount s) t
[PROOFSTEP]
rw [this]
[GOAL]
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t✝ u✝ u t : Set Ω
hs : Set.Finite s
this :
  ↑↑(condCount s) t =
    ↑↑(condCount (s ∩ u)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
⊢ ↑↑(condCount (s ∩ u)) t * ↑↑(condCount s) u + ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount s) uᶜ =
    ↑↑(condCount (s ∩ u)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ u) +
      ↑↑(condCount (s ∩ uᶜ)) t * ↑↑(condCount (s ∩ u ∪ s ∩ uᶜ)) (s ∩ uᶜ)
[PROOFSTEP]
simp [condCount_inter_self hs]