[GOAL]
α : Type u
inst✝ : LinearOrder α
⊢ IsTotalPreorder α fun x x_1 => x ≤ x_1
[PROOFSTEP]
infer_instance
  -- porting note: added
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ a < b
[PROOFSTEP]
rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.lt ↔ a < b
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : a < b
⊢ Ordering.lt = Ordering.lt ↔ a < b
[PROOFSTEP]
simp only [*, lt_irrefl]
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ False ↔ a < b
[PROOFSTEP]
simp only [*, lt_irrefl]
[GOAL]
case neg
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a < b
[PROOFSTEP]
simp only [*, lt_irrefl]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b
[PROOFSTEP]
rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.gt ↔ a > b
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : a < b
⊢ False ↔ a > b
[PROOFSTEP]
simp only [*, lt_irrefl, not_lt_of_gt]
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ False ↔ a > b
[PROOFSTEP]
simp only [*, lt_irrefl, not_lt_of_gt]
[GOAL]
case neg
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ Ordering.gt = Ordering.gt ↔ a > b
[PROOFSTEP]
simp only [*, lt_irrefl, not_lt_of_gt]
[GOAL]
case neg
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ True ↔ a > b
[PROOFSTEP]
case _ h₁ h₂ =>
  have h : b < a := lt_trichotomy a b |>.resolve_left h₁ |>.resolve_left h₂
  exact true_iff_iff.2 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
⊢ True ↔ a > b
[PROOFSTEP]
case _ h₁ h₂ =>
  have h : b < a := lt_trichotomy a b |>.resolve_left h₁ |>.resolve_left h₂
  exact true_iff_iff.2 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
⊢ True ↔ a > b
[PROOFSTEP]
have h : b < a := lt_trichotomy a b |>.resolve_left h₁ |>.resolve_left h₂
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
h : b < a
⊢ True ↔ a > b
[PROOFSTEP]
exact true_iff_iff.2 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b
[PROOFSTEP]
rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.eq ↔ a = b
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : a < b
⊢ False ↔ a = b
[PROOFSTEP]
try simp only []
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : a < b
⊢ False ↔ a = b
[PROOFSTEP]
simp only []
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ Ordering.eq = Ordering.eq ↔ a = b
[PROOFSTEP]
try simp only []
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ Ordering.eq = Ordering.eq ↔ a = b
[PROOFSTEP]
simp only []
[GOAL]
case neg
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b
[PROOFSTEP]
try simp only []
[GOAL]
case neg
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b
[PROOFSTEP]
simp only []
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : a < b
⊢ False ↔ a = b
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ True ↔ a = b
case neg α : Type u inst✝ : LinearOrder α a b : α h✝¹ : ¬a < b h✝ : ¬a = b ⊢ False ↔ a = b
[PROOFSTEP]
case _ h => exact false_iff_iff.2 <| ne_iff_lt_or_gt.2 <| .inl h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ False ↔ a = b
[PROOFSTEP]
case _ h => exact false_iff_iff.2 <| ne_iff_lt_or_gt.2 <| .inl h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ False ↔ a = b
[PROOFSTEP]
exact false_iff_iff.2 <| ne_iff_lt_or_gt.2 <| .inl h
[GOAL]
case pos
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ True ↔ a = b
case neg α : Type u inst✝ : LinearOrder α a b : α h✝¹ : ¬a < b h✝ : ¬a = b ⊢ False ↔ a = b
[PROOFSTEP]
case _ _ h => exact true_iff_iff.2 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : ¬a < b
h : a = b
⊢ True ↔ a = b
[PROOFSTEP]
case _ _ h => exact true_iff_iff.2 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : ¬a < b
h : a = b
⊢ True ↔ a = b
[PROOFSTEP]
exact true_iff_iff.2 h
[GOAL]
case neg
α : Type u
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b
[PROOFSTEP]
case _ _ h => exact false_iff_iff.2 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : ¬a < b
h : ¬a = b
⊢ False ↔ a = b
[PROOFSTEP]
case _ _ h => exact false_iff_iff.2 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : ¬a < b
h : ¬a = b
⊢ False ↔ a = b
[PROOFSTEP]
exact false_iff_iff.2 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b ≠ Ordering.gt ↔ a ≤ b
[PROOFSTEP]
cases h : compare a b
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.lt ≠ Ordering.gt ↔ a ≤ b
[PROOFSTEP]
simp only []
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.eq ≠ Ordering.gt ↔ a ≤ b
[PROOFSTEP]
simp only []
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.gt ↔ a ≤ b
[PROOFSTEP]
simp only []
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ True ↔ a ≤ b
[PROOFSTEP]
exact true_iff_iff.2 <| le_of_lt <| compare_lt_iff_lt.1 h
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ True ↔ a ≤ b
[PROOFSTEP]
exact true_iff_iff.2 <| le_of_eq <| compare_eq_iff_eq.1 h
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ False ↔ a ≤ b
[PROOFSTEP]
exact false_iff_iff.2 <| not_le_of_gt <| compare_gt_iff_gt.1 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b ≠ Ordering.lt ↔ a ≥ b
[PROOFSTEP]
cases h : compare a b
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.lt ≠ Ordering.lt ↔ a ≥ b
[PROOFSTEP]
simp only []
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.eq ≠ Ordering.lt ↔ a ≥ b
[PROOFSTEP]
simp only []
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.lt ↔ a ≥ b
[PROOFSTEP]
simp only []
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ False ↔ a ≥ b
[PROOFSTEP]
exact false_iff_iff.2 <| (lt_iff_not_ge a b).1 <| compare_lt_iff_lt.1 h
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ True ↔ a ≥ b
[PROOFSTEP]
exact true_iff_iff.2 <| le_of_eq <| (·.symm) <| compare_eq_iff_eq.1 h
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ True ↔ a ≥ b
[PROOFSTEP]
exact true_iff_iff.2 <| le_of_lt <| compare_gt_iff_gt.1 h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
o : Ordering
⊢ compare a b = o ↔ Ordering.toRel o a b
[PROOFSTEP]
cases o
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ Ordering.toRel Ordering.lt a b
[PROOFSTEP]
simp only [Ordering.toRel]
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ Ordering.toRel Ordering.eq a b
[PROOFSTEP]
simp only [Ordering.toRel]
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ Ordering.toRel Ordering.gt a b
[PROOFSTEP]
simp only [Ordering.toRel]
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ a < b
[PROOFSTEP]
exact compare_lt_iff_lt
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b
[PROOFSTEP]
exact compare_eq_iff_eq
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b
[PROOFSTEP]
exact compare_gt_iff_gt
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ Ordering.swap (compare a b) = compare b a
[PROOFSTEP]
cases h : compare a b
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.swap Ordering.lt = compare b a
[PROOFSTEP]
simp only [Ordering.swap]
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.swap Ordering.eq = compare b a
[PROOFSTEP]
simp only [Ordering.swap]
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.swap Ordering.gt = compare b a
[PROOFSTEP]
simp only [Ordering.swap]
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.gt = compare b a
[PROOFSTEP]
symm
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.eq = compare b a
[PROOFSTEP]
symm
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.lt = compare b a
[PROOFSTEP]
symm
[GOAL]
case lt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ compare b a = Ordering.gt
[PROOFSTEP]
exact compare_gt_iff_gt.2 <| compare_lt_iff_lt.1 h
[GOAL]
case eq
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ compare b a = Ordering.eq
[PROOFSTEP]
exact compare_eq_iff_eq.2 <| compare_eq_iff_eq.1 h |>.symm
[GOAL]
case gt
α : Type u
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ compare b a = Ordering.lt
[PROOFSTEP]
exact compare_lt_iff_lt.2 <| compare_gt_iff_gt.1 h


[GOAL]
α : Type u_1
inst✝ : Encodable α
l : List α
⊢ decodeList (encodeList l) = some l
[PROOFSTEP]
induction' l with a l IH
[GOAL]
case nil
α : Type u_1
inst✝ : Encodable α
⊢ decodeList (encodeList []) = some []
[PROOFSTEP]
simp [encodeList, decodeList, unpair_pair, encodek, *]
[GOAL]
case cons
α : Type u_1
inst✝ : Encodable α
a : α
l : List α
IH : decodeList (encodeList l) = some l
⊢ decodeList (encodeList (a :: l)) = some (a :: l)
[PROOFSTEP]
simp [encodeList, decodeList, unpair_pair, encodek, *]
[GOAL]
α✝ : Type u_1
inst✝¹ : Encodable α✝
α : Type u_2
inst✝ : Countable α
⊢ Countable (List α)
[PROOFSTEP]
haveI := Encodable.ofCountable α
[GOAL]
α✝ : Type u_1
inst✝¹ : Encodable α✝
α : Type u_2
inst✝ : Countable α
this : Encodable α
⊢ Countable (List α)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝ : Encodable α
⊢ decodeList 0 = some []
[PROOFSTEP]
rw [decodeList]
[GOAL]
α : Type u_1
inst✝ : Encodable α
v : ℕ
⊢ decodeList (succ v) = Seq.seq ((fun x x_1 => x :: x_1) <$> decode (unpair v).fst) fun x => decode (unpair v).snd
[PROOFSTEP]
cases' e : unpair v with v₁ v₂
[GOAL]
case mk
α : Type u_1
inst✝ : Encodable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ decodeList (succ v) = Seq.seq ((fun x x_1 => x :: x_1) <$> decode (v₁, v₂).fst) fun x => decode (v₁, v₂).snd
[PROOFSTEP]
simp [decodeList, e]
[GOAL]
case mk
α : Type u_1
inst✝ : Encodable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ (Seq.seq (Option.map (fun x x_1 => x :: x_1) (decode v₁)) fun x => decodeList v₂) =
    Seq.seq (Option.map (fun x x_1 => x :: x_1) (decode v₁)) fun x => decode v₂
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : Encodable α
a b : α
⊢ Decidable (Encodable.enle a b)
[PROOFSTEP]
unfold enle Order.Preimage
[GOAL]
α : Type u_1
inst✝ : Encodable α
a b : α
⊢ Decidable ((fun x x_1 => x ≤ x_1) (encode a) (encode b))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝ : Encodable α
s : Multiset α
⊢ decodeMultiset (encodeMultiset s) = some s
[PROOFSTEP]
simp [encodeMultiset, decodeMultiset, encodek]
[GOAL]
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
⊢ Encodable α
[PROOFSTEP]
classical exact (Fintype.truncEncodable α).out
[GOAL]
α✝ : Type u_1
α : Type u_2
inst✝ : Fintype α
⊢ Encodable α
[PROOFSTEP]
exact (Fintype.truncEncodable α).out
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ∃ a, a ∈ decodeList 0 ∧ encodeList a = 0
[PROOFSTEP]
rw [decodeList]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ∃ a, a ∈ some [] ∧ encodeList a = 0
[PROOFSTEP]
exact ⟨_, rfl, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v : ℕ
⊢ ∃ a, a ∈ decodeList (succ v) ∧ encodeList a = succ v
[PROOFSTEP]
cases' e : unpair v with v₁ v₂
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ ∃ a, a ∈ decodeList (succ v) ∧ encodeList a = succ v
[PROOFSTEP]
have h := unpair_right_le v
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (unpair v).snd ≤ v
⊢ ∃ a, a ∈ decodeList (succ v) ∧ encodeList a = succ v
[PROOFSTEP]
rw [e] at h
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).snd ≤ v
⊢ ∃ a, a ∈ decodeList (succ v) ∧ encodeList a = succ v
[PROOFSTEP]
rcases have : v₂ < succ v := lt_succ_of_le h
  denumerable_list_aux v₂ with
  ⟨a, h₁, h₂⟩
[GOAL]
case mk.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).snd ≤ v
a : List α
h₁ : a ∈ decodeList v₂
h₂ : encodeList a = v₂
⊢ ∃ a, a ∈ decodeList (succ v) ∧ encodeList a = succ v
[PROOFSTEP]
rw [Option.mem_def] at h₁
[GOAL]
case mk.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).snd ≤ v
a : List α
h₁ : decodeList v₂ = some a
h₂ : encodeList a = v₂
⊢ ∃ a, a ∈ decodeList (succ v) ∧ encodeList a = succ v
[PROOFSTEP]
use ofNat α v₁ :: a
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).snd ≤ v
a : List α
h₁ : decodeList v₂ = some a
h₂ : encodeList a = v₂
⊢ ofNat α v₁ :: a ∈ decodeList (succ v) ∧ encodeList (ofNat α v₁ :: a) = succ v
[PROOFSTEP]
simp [decodeList, e, h₂, h₁, encodeList, pair_unpair' e]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
⊢ ofNat (List α) 0 = []
[PROOFSTEP]
rw [← @encode_list_nil α, ofNat_encode]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v : ℕ
⊢ decodeList (succ v) = some (ofNat α (unpair v).fst :: ofNat (List α) (unpair v).snd)
[PROOFSTEP]
cases' e : unpair v with v₁ v₂
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ decodeList (succ v) = some (ofNat α (v₁, v₂).fst :: ofNat (List α) (v₁, v₂).snd)
[PROOFSTEP]
simp [decodeList, e]
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ (Seq.seq (some fun x => ofNat α v₁ :: x) fun x => decodeList v₂) = some (ofNat α v₁ :: ofNat (List α) v₂)
[PROOFSTEP]
rw [show decodeList v₂ = decode (α := List α) v₂ from rfl, decode_eq_ofNat, Option.seq_some, Option.some.injEq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
⊢ lower (raise (m :: l) n) n = m :: l
[PROOFSTEP]
rw [raise, lower, add_tsub_cancel_right, lower_raise l]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
h : Sorted (fun x x_1 => x ≤ x_1) (n :: m :: l)
⊢ raise (lower (m :: l) n) n = m :: l
[PROOFSTEP]
have : n ≤ m := List.rel_of_sorted_cons h _ (l.mem_cons_self _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
h : Sorted (fun x x_1 => x ≤ x_1) (n :: m :: l)
this : n ≤ m
⊢ raise (lower (m :: l) n) n = m :: l
[PROOFSTEP]
simp [raise, lower, tsub_add_cancel_of_le this, raise_lower h.of_cons]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
s : Multiset α
⊢ (fun n => Multiset.map (ofNat α) ↑(raise (ofNat (List ℕ) n) 0))
      ((fun s => encode (lower (Multiset.sort (fun x x_1 => x ≤ x_1) (Multiset.map encode s)) 0)) s) =
    s
[PROOFSTEP]
have := raise_lower (List.sorted_cons.2 ⟨fun n _ => Nat.zero_le n, (s.map encode).sort_sorted _⟩)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
s : Multiset α
this :
  raise (lower (Multiset.sort (fun x x_1 => x ≤ x_1) (Multiset.map encode s)) 0) 0 =
    Multiset.sort (fun x x_1 => x ≤ x_1) (Multiset.map encode s)
⊢ (fun n => Multiset.map (ofNat α) ↑(raise (ofNat (List ℕ) n) 0))
      ((fun s => encode (lower (Multiset.sort (fun x x_1 => x ≤ x_1) (Multiset.map encode s)) 0)) s) =
    s
[PROOFSTEP]
simp [-Multiset.coe_map, this]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (fun s => encode (lower (Multiset.sort (fun x x_1 => x ≤ x_1) (Multiset.map encode s)) 0))
      ((fun n => Multiset.map (ofNat α) ↑(raise (ofNat (List ℕ) n) 0)) n) =
    n
[PROOFSTEP]
simp [-Multiset.coe_map, List.mergeSort_eq_self _ (raise_sorted _ _), lower_raise]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
⊢ lower' (raise' (m :: l) n) n = m :: l
[PROOFSTEP]
simp [raise', lower', add_tsub_cancel_right, lower_raise']
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
h₁ : ∀ (m_1 : ℕ), m_1 ∈ m :: l → n ≤ m_1
h₂ : Sorted (fun x x_1 => x < x_1) (m :: l)
⊢ raise' (lower' (m :: l) n) n = m :: l
[PROOFSTEP]
have : n ≤ m := h₁ _ (l.mem_cons_self _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
h₁ : ∀ (m_1 : ℕ), m_1 ∈ m :: l → n ≤ m_1
h₂ : Sorted (fun x x_1 => x < x_1) (m :: l)
this : n ≤ m
⊢ raise' (lower' (m :: l) n) n = m :: l
[PROOFSTEP]
simp [raise', lower', tsub_add_cancel_of_le this, raise_lower' (List.rel_of_sorted_cons h₂ : ∀ a ∈ l, m < a) h₂.of_cons]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
s : Finset α
⊢ ((fun n => Finset.map (Equiv.toEmbedding (eqv α).symm) (raise'Finset (ofNat (List ℕ) n) 0))
        ((fun s => encode (lower' (Finset.sort (fun x x_1 => x ≤ x_1) (Finset.map (Equiv.toEmbedding (eqv α)) s)) 0))
          s)).val =
    s.val
[PROOFSTEP]
simp [-Multiset.coe_map, raise'Finset, raise_lower' (fun n _ => Nat.zero_le n) (Finset.sort_sorted_lt _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (fun s => encode (lower' (Finset.sort (fun x x_1 => x ≤ x_1) (Finset.map (Equiv.toEmbedding (eqv α)) s)) 0))
      ((fun n => Finset.map (Equiv.toEmbedding (eqv α).symm) (raise'Finset (ofNat (List ℕ) n) 0)) n) =
    n
[PROOFSTEP]
simp [-Multiset.coe_map, Finset.map, raise'Finset, Finset.sort,
  List.mergeSort_eq_self (· ≤ ·) ((raise'_sorted _ _).imp (@le_of_lt _ _)), lower_raise']
[GOAL]
u : List Unit
⊢ length ((fun n => replicate n ()) (length u)) = length u
[PROOFSTEP]
simp


[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ min a b = if a ≤ b then a else b
[PROOFSTEP]
rw [LinearOrder.min_def a]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ max a b = if a ≤ b then b else a
[PROOFSTEP]
rw [LinearOrder.max_def a]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ min a b ≤ a
[PROOFSTEP]
if h : a ≤ b then simp [min_def, if_pos h, le_refl] else simp [min_def, if_neg h]; exact le_of_not_le h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ min a b ≤ a
[PROOFSTEP]
simp [min_def, if_pos h, le_refl]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ min a b ≤ a
[PROOFSTEP]
simp [min_def, if_neg h]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ b ≤ a
[PROOFSTEP]
exact le_of_not_le h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ min a b ≤ b
[PROOFSTEP]
if h : a ≤ b then simp [min_def, if_pos h]; exact h else simp [min_def, if_neg h, le_refl]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ min a b ≤ b
[PROOFSTEP]
simp [min_def, if_pos h]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ a ≤ b
[PROOFSTEP]
exact h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ min a b ≤ b
[PROOFSTEP]
simp [min_def, if_neg h, le_refl]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
⊢ c ≤ min a b
[PROOFSTEP]
if h : a ≤ b then simp [min_def, if_pos h]; exact h₁ else simp [min_def, if_neg h]; exact h₂
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
h : a ≤ b
⊢ c ≤ min a b
[PROOFSTEP]
simp [min_def, if_pos h]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
h : a ≤ b
⊢ c ≤ a
[PROOFSTEP]
exact h₁
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
h : ¬a ≤ b
⊢ c ≤ min a b
[PROOFSTEP]
simp [min_def, if_neg h]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
h : ¬a ≤ b
⊢ c ≤ b
[PROOFSTEP]
exact h₂
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ a ≤ max a b
[PROOFSTEP]
if h : a ≤ b then simp [max_def, if_pos h]; exact h else simp [max_def, if_neg h, le_refl]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ a ≤ max a b
[PROOFSTEP]
simp [max_def, if_pos h]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ a ≤ b
[PROOFSTEP]
exact h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ a ≤ max a b
[PROOFSTEP]
simp [max_def, if_neg h, le_refl]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
⊢ b ≤ max a b
[PROOFSTEP]
if h : a ≤ b then simp [max_def, if_pos h, le_refl] else simp [max_def, if_neg h]; exact le_of_not_le h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ b ≤ max a b
[PROOFSTEP]
simp [max_def, if_pos h, le_refl]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ b ≤ max a b
[PROOFSTEP]
simp [max_def, if_neg h]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ b ≤ a
[PROOFSTEP]
exact le_of_not_le h
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
h₁ : a ≤ c
h₂ : b ≤ c
⊢ max a b ≤ c
[PROOFSTEP]
if h : a ≤ b then simp [max_def, if_pos h]; exact h₂ else simp [max_def, if_neg h]; exact h₁
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
h₁ : a ≤ c
h₂ : b ≤ c
h : a ≤ b
⊢ max a b ≤ c
[PROOFSTEP]
simp [max_def, if_pos h]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
h₁ : a ≤ c
h₂ : b ≤ c
h : a ≤ b
⊢ b ≤ c
[PROOFSTEP]
exact h₂
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
h₁ : a ≤ c
h₂ : b ≤ c
h : ¬a ≤ b
⊢ max a b ≤ c
[PROOFSTEP]
simp [max_def, if_neg h]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
h₁ : a ≤ c
h₂ : b ≤ c
h : ¬a ≤ b
⊢ a ≤ c
[PROOFSTEP]
exact h₁
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c = min a (min b c)
[PROOFSTEP]
apply eq_min
[GOAL]
case h₁
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c ≤ a
[PROOFSTEP]
apply le_trans
[GOAL]
case h₁.a
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c ≤ ?h₁.b
case h₁.a
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ ?h₁.b ≤ a
case h₁.b α : Type u inst✝ : LinearOrder α a b c : α ⊢ α
[PROOFSTEP]
apply min_le_left
[GOAL]
case h₁.a
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min a b ≤ a
[PROOFSTEP]
apply min_le_left
[GOAL]
case h₂
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c ≤ min b c
[PROOFSTEP]
apply le_min
[GOAL]
case h₂.h₁
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c ≤ b
case h₂.h₂ α : Type u inst✝ : LinearOrder α a b c : α ⊢ min (min a b) c ≤ c
[PROOFSTEP]
apply le_trans
[GOAL]
case h₂.h₁.a
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c ≤ ?h₂.h₁.b
case h₂.h₁.a
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ ?h₂.h₁.b ≤ b
case h₂.h₁.b
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ α
case h₂.h₂ α : Type u inst✝ : LinearOrder α a b c : α ⊢ min (min a b) c ≤ c
[PROOFSTEP]
apply min_le_left
[GOAL]
case h₂.h₁.a
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min a b ≤ b
case h₂.h₂ α : Type u inst✝ : LinearOrder α a b c : α ⊢ min (min a b) c ≤ c
[PROOFSTEP]
apply min_le_right
[GOAL]
case h₂.h₂
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min (min a b) c ≤ c
[PROOFSTEP]
apply min_le_right
[GOAL]
case h₃
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ ∀ {d : α}, d ≤ a → d ≤ min b c → d ≤ min (min a b) c
[PROOFSTEP]
intro d h₁ h₂
[GOAL]
case h₃
α : Type u
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ d ≤ min (min a b) c
[PROOFSTEP]
apply le_min
[GOAL]
case h₃.h₁
α : Type u
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ d ≤ min a b
case h₃.h₂ α : Type u inst✝ : LinearOrder α a b c d : α h₁ : d ≤ a h₂ : d ≤ min b c ⊢ d ≤ c
[PROOFSTEP]
apply le_min h₁
[GOAL]
case h₃.h₁
α : Type u
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ d ≤ b
case h₃.h₂ α : Type u inst✝ : LinearOrder α a b c d : α h₁ : d ≤ a h₂ : d ≤ min b c ⊢ d ≤ c
[PROOFSTEP]
apply le_trans h₂
[GOAL]
case h₃.h₁
α : Type u
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ min b c ≤ b
case h₃.h₂ α : Type u inst✝ : LinearOrder α a b c d : α h₁ : d ≤ a h₂ : d ≤ min b c ⊢ d ≤ c
[PROOFSTEP]
apply min_le_left
[GOAL]
case h₃.h₂
α : Type u
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ d ≤ c
[PROOFSTEP]
apply le_trans h₂
[GOAL]
case h₃.h₂
α : Type u
inst✝ : LinearOrder α
a b c d : α
h₁ : d ≤ a
h₂ : d ≤ min b c
⊢ min b c ≤ c
[PROOFSTEP]
apply min_le_right
[GOAL]
α : Type u
inst✝ : LinearOrder α
a : α
⊢ min a a = a
[PROOFSTEP]
simp [min_def]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ min a b = a
[PROOFSTEP]
apply Eq.symm
[GOAL]
case h
α : Type u
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ a = min a b
[PROOFSTEP]
apply eq_min (le_refl _) h
[GOAL]
case h
α : Type u
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ ∀ {d : α}, d ≤ a → d ≤ b → d ≤ a
[PROOFSTEP]
intros
[GOAL]
case h
α : Type u
inst✝ : LinearOrder α
a b : α
h : a ≤ b
d✝ : α
a✝¹ : d✝ ≤ a
a✝ : d✝ ≤ b
⊢ d✝ ≤ a
[PROOFSTEP]
assumption
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ max (max a b) c = max a (max b c)
[PROOFSTEP]
apply eq_max
[GOAL]
case h₁
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ a ≤ max (max a b) c
[PROOFSTEP]
apply le_trans
[GOAL]
case h₁.a
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ a ≤ ?h₁.b
case h₁.a
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ ?h₁.b ≤ max (max a b) c
case h₁.b α : Type u inst✝ : LinearOrder α a b c : α ⊢ α
[PROOFSTEP]
apply le_max_left a b
[GOAL]
case h₁.a
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ max a b ≤ max (max a b) c
[PROOFSTEP]
apply le_max_left
[GOAL]
case h₂
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ max b c ≤ max (max a b) c
[PROOFSTEP]
apply max_le
[GOAL]
case h₂.h₁
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ b ≤ max (max a b) c
case h₂.h₂ α : Type u inst✝ : LinearOrder α a b c : α ⊢ c ≤ max (max a b) c
[PROOFSTEP]
apply le_trans
[GOAL]
case h₂.h₁.a
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ b ≤ ?h₂.h₁.b
case h₂.h₁.a
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ ?h₂.h₁.b ≤ max (max a b) c
case h₂.h₁.b
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ α
case h₂.h₂ α : Type u inst✝ : LinearOrder α a b c : α ⊢ c ≤ max (max a b) c
[PROOFSTEP]
apply le_max_right a b
[GOAL]
case h₂.h₁.a
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ max a b ≤ max (max a b) c
case h₂.h₂ α : Type u inst✝ : LinearOrder α a b c : α ⊢ c ≤ max (max a b) c
[PROOFSTEP]
apply le_max_left
[GOAL]
case h₂.h₂
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ c ≤ max (max a b) c
[PROOFSTEP]
apply le_max_right
[GOAL]
case h₃
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ ∀ {d : α}, a ≤ d → max b c ≤ d → max (max a b) c ≤ d
[PROOFSTEP]
intro d h₁ h₂
[GOAL]
case h₃
α : Type u
inst✝ : LinearOrder α
a b c d : α
h₁ : a ≤ d
h₂ : max b c ≤ d
⊢ max (max a b) c ≤ d
[PROOFSTEP]
apply max_le
[GOAL]
case h₃.h₁
α : Type u
inst✝ : LinearOrder α
a b c d : α
h₁ : a ≤ d
h₂ : max b c ≤ d
⊢ max a b ≤ d
case h₃.h₂ α : Type u inst✝ : LinearOrder α a b c d : α h₁ : a ≤ d h₂ : max b c ≤ d ⊢ c ≤ d
[PROOFSTEP]
apply max_le h₁
[GOAL]
case h₃.h₁
α : Type u
inst✝ : LinearOrder α
a b c d : α
h₁ : a ≤ d
h₂ : max b c ≤ d
⊢ b ≤ d
case h₃.h₂ α : Type u inst✝ : LinearOrder α a b c d : α h₁ : a ≤ d h₂ : max b c ≤ d ⊢ c ≤ d
[PROOFSTEP]
apply le_trans (le_max_left _ _) h₂
[GOAL]
case h₃.h₂
α : Type u
inst✝ : LinearOrder α
a b c d : α
h₁ : a ≤ d
h₂ : max b c ≤ d
⊢ c ≤ d
[PROOFSTEP]
apply le_trans (le_max_right _ _) h₂
[GOAL]
α : Type u
inst✝ : LinearOrder α
a : α
⊢ max a a = a
[PROOFSTEP]
simp [max_def]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ max a b = a
[PROOFSTEP]
apply Eq.symm
[GOAL]
case h
α : Type u
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ a = max a b
[PROOFSTEP]
apply eq_max (le_refl _) h
[GOAL]
case h
α : Type u
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ ∀ {d : α}, a ≤ d → b ≤ d → a ≤ d
[PROOFSTEP]
intros
[GOAL]
case h
α : Type u
inst✝ : LinearOrder α
a b : α
h : b ≤ a
d✝ : α
a✝¹ : a ≤ d✝
a✝ : b ≤ d✝
⊢ a ≤ d✝
[PROOFSTEP]
assumption
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
h₁ : a < b
h₂ : a < c
h : b ≤ c
⊢ a < min b c
[PROOFSTEP]
rwa [min_eq_left h]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
h₁ : a < b
h₂ : a < c
h : b > c
⊢ a < min b c
[PROOFSTEP]
rwa [min_eq_right_of_lt h]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
h₁ : a < c
h₂ : b < c
h : a ≤ b
⊢ max a b < c
[PROOFSTEP]
rwa [max_eq_right h]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
h₁ : a < c
h₂ : b < c
h : a > b
⊢ max a b < c
[PROOFSTEP]
rwa [max_eq_left_of_lt h]


[GOAL]
n iv : ℕ
ilt₁ : iv < n
jv : ℕ
jlt₁ : jv < n
h : { val := iv, isLt := ilt₁ }.val = { val := jv, isLt := jlt₁ }.val
⊢ { val := iv, isLt := ilt₁ } = { val := jv, isLt := jlt₁ }
[PROOFSTEP]
cases h
[GOAL]
case refl
n iv : ℕ
ilt₁ jlt₁ : iv < n
⊢ { val := iv, isLt := ilt₁ } = { val := iv, isLt := jlt₁ }
[PROOFSTEP]
rfl


[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ (List.bind l fun x => [x]) = l
[PROOFSTEP]
induction l
[GOAL]
case nil
α : Type u
β : Type v
γ : Type w
⊢ (List.bind [] fun x => [x]) = []
[PROOFSTEP]
simp [*]
[GOAL]
case cons
α : Type u
β : Type v
γ : Type w
head✝ : α
tail✝ : List α
tail_ih✝ : (List.bind tail✝ fun x => [x]) = tail✝
⊢ (List.bind (head✝ :: tail✝) fun x => [x]) = head✝ :: tail✝
[PROOFSTEP]
simp [*]
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map f l = List.bind l fun x => [f x]
[PROOFSTEP]
simp only [← map_singleton]
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map f l = List.bind l fun x => map f [x]
[PROOFSTEP]
rw [← bind_singleton' l, bind_map, bind_singleton']
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
l : List α
f : α → List β
g : β → List γ
⊢ List.bind (List.bind l f) g = List.bind l fun x => List.bind (f x) g
[PROOFSTEP]
induction l
[GOAL]
case nil
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
f : α → List β
g : β → List γ
⊢ List.bind (List.bind [] f) g = List.bind [] fun x => List.bind (f x) g
[PROOFSTEP]
simp [*]
[GOAL]
case cons
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
f : α → List β
g : β → List γ
head✝ : α
tail✝ : List α
tail_ih✝ : List.bind (List.bind tail✝ f) g = List.bind tail✝ fun x => List.bind (f x) g
⊢ List.bind (List.bind (head✝ :: tail✝) f) g = List.bind (head✝ :: tail✝) fun x => List.bind (f x) g
[PROOFSTEP]
simp [*]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
⊢ ¬∃ x, x ∈ [] ∧ p x
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
h₂ : ∃ x, x ∈ xs ∧ p x
⊢ ∃ x_1, x_1 ∈ x :: xs ∧ p x_1
[PROOFSTEP]
cases' h₂ with y h
[GOAL]
case intro
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
y : α
h : y ∈ xs ∧ p y
⊢ ∃ x_1, x_1 ∈ x :: xs ∧ p x_1
[PROOFSTEP]
cases' h with hm hp
[GOAL]
case intro.intro
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
y : α
hm : y ∈ xs
hp : p y
⊢ ∃ x_1, x_1 ∈ x :: xs ∧ p x_1
[PROOFSTEP]
exact ⟨y, mem_cons_of_mem _ hm, hp⟩
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
h₂ : ¬∃ x, x ∈ xs ∧ p x
⊢ ¬∃ x_1, x_1 ∈ x :: xs ∧ p x_1
[PROOFSTEP]
intro h
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
h₂ : ¬∃ x, x ∈ xs ∧ p x
h : ∃ x_1, x_1 ∈ x :: xs ∧ p x_1
⊢ False
[PROOFSTEP]
cases' h with y h
[GOAL]
case intro
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
h₂ : ¬∃ x, x ∈ xs ∧ p x
y : α
h : y ∈ x :: xs ∧ p y
⊢ False
[PROOFSTEP]
cases' h with hm hp
[GOAL]
case intro.intro
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
h₂ : ¬∃ x, x ∈ xs ∧ p x
y : α
hm : y ∈ x :: xs
hp : p y
⊢ False
[PROOFSTEP]
cases' mem_cons.1 hm with h h
[GOAL]
case intro.intro.inl
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
h₂ : ¬∃ x, x ∈ xs ∧ p x
y : α
hm : y ∈ x :: xs
hp : p y
h : y = x
⊢ False
[PROOFSTEP]
rw [h] at hp
[GOAL]
case intro.intro.inl
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
h₂ : ¬∃ x, x ∈ xs ∧ p x
y : α
hm : y ∈ x :: xs
hp : p x
h : y = x
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case intro.intro.inr
α✝ : Type u
β : Type v
γ : Type w
α : Type u
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
h₁ : ¬p x
h₂ : ¬∃ x, x ∈ xs ∧ p x
y : α
hm : y ∈ x :: xs
hp : p y
h : y ∈ xs
⊢ False
[PROOFSTEP]
exact absurd ⟨y, h, hp⟩ h₂


[GOAL]
α : Type u
b : Bool
a : α
⊢ (bif b then a else a) = a
[PROOFSTEP]
cases b
[GOAL]
case false
α : Type u
a : α
⊢ (bif false then a else a) = a
[PROOFSTEP]
rfl
[GOAL]
case true
α : Type u
a : α
⊢ (bif true then a else a) = a
[PROOFSTEP]
rfl
[GOAL]
b : Bool
⊢ xor b b = false
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ xor false false = false
[PROOFSTEP]
simp
[GOAL]
case true
⊢ xor true true = false
[PROOFSTEP]
simp
[GOAL]
b : Bool
⊢ xor b true = !b
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ xor false true = !false
[PROOFSTEP]
simp
[GOAL]
case true
⊢ xor true true = !true
[PROOFSTEP]
simp
[GOAL]
b : Bool
⊢ xor b false = b
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ xor false false = false
[PROOFSTEP]
simp
[GOAL]
case true
⊢ xor true false = true
[PROOFSTEP]
simp
[GOAL]
b : Bool
⊢ xor true b = !b
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ xor true false = !false
[PROOFSTEP]
simp
[GOAL]
case true
⊢ xor true true = !true
[PROOFSTEP]
simp
[GOAL]
b : Bool
⊢ xor false b = b
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ xor false false = false
[PROOFSTEP]
simp
[GOAL]
case true
⊢ xor false true = true
[PROOFSTEP]
simp
[GOAL]
⊢ ¬true = false
[PROOFSTEP]
decide
[GOAL]
⊢ ¬false = true
[PROOFSTEP]
decide
[GOAL]
b : Bool
⊢ (¬b = true) = (b = false)
[PROOFSTEP]
simp
[GOAL]
b : Bool
⊢ (¬b = false) = (b = true)
[PROOFSTEP]
simp
[GOAL]
a b : Bool
⊢ ((a && b) = true) = (a = true ∧ b = true)
[PROOFSTEP]
simp
[GOAL]
a b : Bool
⊢ ((a || b) = true) = (a = true ∨ b = true)
[PROOFSTEP]
simp
[GOAL]
a : Bool
⊢ ((!a) = true) = (a = false)
[PROOFSTEP]
cases a
[GOAL]
case false
⊢ ((!false) = true) = (false = false)
[PROOFSTEP]
simp
[GOAL]
case true
⊢ ((!true) = true) = (true = false)
[PROOFSTEP]
simp
[GOAL]
a b : Bool
⊢ ((a && b) = false) = (a = false ∨ b = false)
[PROOFSTEP]
cases a
[GOAL]
case false
b : Bool
⊢ ((false && b) = false) = (false = false ∨ b = false)
[PROOFSTEP]
cases b
[GOAL]
case true
b : Bool
⊢ ((true && b) = false) = (true = false ∨ b = false)
[PROOFSTEP]
cases b
[GOAL]
case false.false
⊢ ((false && false) = false) = (false = false ∨ false = false)
[PROOFSTEP]
simp
[GOAL]
case false.true
⊢ ((false && true) = false) = (false = false ∨ true = false)
[PROOFSTEP]
simp
[GOAL]
case true.false
⊢ ((true && false) = false) = (true = false ∨ false = false)
[PROOFSTEP]
simp
[GOAL]
case true.true
⊢ ((true && true) = false) = (true = false ∨ true = false)
[PROOFSTEP]
simp
[GOAL]
a b : Bool
⊢ ((a || b) = false) = (a = false ∧ b = false)
[PROOFSTEP]
cases a
[GOAL]
case false
b : Bool
⊢ ((false || b) = false) = (false = false ∧ b = false)
[PROOFSTEP]
cases b
[GOAL]
case true
b : Bool
⊢ ((true || b) = false) = (true = false ∧ b = false)
[PROOFSTEP]
cases b
[GOAL]
case false.false
⊢ ((false || false) = false) = (false = false ∧ false = false)
[PROOFSTEP]
simp
[GOAL]
case false.true
⊢ ((false || true) = false) = (false = false ∧ true = false)
[PROOFSTEP]
simp
[GOAL]
case true.false
⊢ ((true || false) = false) = (true = false ∧ false = false)
[PROOFSTEP]
simp
[GOAL]
case true.true
⊢ ((true || true) = false) = (true = false ∧ true = false)
[PROOFSTEP]
simp
[GOAL]
a : Bool
⊢ ((!a) = false) = (a = true)
[PROOFSTEP]
cases a
[GOAL]
case false
⊢ ((!false) = false) = (false = true)
[PROOFSTEP]
simp
[GOAL]
case true
⊢ ((!true) = false) = (true = true)
[PROOFSTEP]
simp
[GOAL]
⊢ (false = true) = False
[PROOFSTEP]
simp
[GOAL]
⊢ (true = true) = True
[PROOFSTEP]
simp
[GOAL]
⊢ (false = true) = False
[PROOFSTEP]
simp
[GOAL]
⊢ (true = true) = True
[PROOFSTEP]
simp
[GOAL]
p : Prop
d : Decidable p
⊢ decide p = true ↔ p
[PROOFSTEP]
simp
[GOAL]
b : Bool
⊢ ¬b = true ↔ b = false
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ ¬false = true ↔ false = false
[PROOFSTEP]
exact by decide
[GOAL]
⊢ ¬false = true ↔ false = false
[PROOFSTEP]
decide
[GOAL]
case true
⊢ ¬true = true ↔ true = false
[PROOFSTEP]
exact by decide
[GOAL]
⊢ ¬true = true ↔ true = false
[PROOFSTEP]
decide
[GOAL]
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p ↔ q
⊢ decide p = decide q
[PROOFSTEP]
cases h' : decide q with
| false => exact decide_false (mt h.1 <| of_decide_false h')
| true => exact decide_true (h.2 <| of_decide_true h')
[GOAL]
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p ↔ q
x✝ : Bool
h' : decide q = x✝
⊢ decide p = x✝
[PROOFSTEP]
cases h' : decide q with
| false => exact decide_false (mt h.1 <| of_decide_false h')
| true => exact decide_true (h.2 <| of_decide_true h')
[GOAL]
case false
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p ↔ q
h' : decide q = false
⊢ decide p = false
[PROOFSTEP]

| false => exact decide_false (mt h.1 <| of_decide_false h')
[GOAL]
case false
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p ↔ q
h' : decide q = false
⊢ decide p = false
[PROOFSTEP]
exact decide_false (mt h.1 <| of_decide_false h')
[GOAL]
case true
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p ↔ q
h' : decide q = true
⊢ decide p = true
[PROOFSTEP]

| true => exact decide_true (h.2 <| of_decide_true h')
[GOAL]
case true
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p ↔ q
h' : decide q = true
⊢ decide p = true
[PROOFSTEP]
exact decide_true (h.2 <| of_decide_true h')
[GOAL]
a b : Bool
⊢ (a || b) = true ↔ a = true ∨ b = true
[PROOFSTEP]
simp
[GOAL]
a b : Bool
⊢ (a && b) = true ↔ a = true ∧ b = true
[PROOFSTEP]
simp
[GOAL]
a b : Bool
⊢ xor a b = true ↔ Xor' (a = true) (b = true)
[PROOFSTEP]
cases a
[GOAL]
case false
b : Bool
⊢ xor false b = true ↔ Xor' (false = true) (b = true)
[PROOFSTEP]
cases b
[GOAL]
case true
b : Bool
⊢ xor true b = true ↔ Xor' (true = true) (b = true)
[PROOFSTEP]
cases b
[GOAL]
case false.false
⊢ xor false false = true ↔ Xor' (false = true) (false = true)
[PROOFSTEP]
exact by decide
[GOAL]
⊢ xor false false = true ↔ Xor' (false = true) (false = true)
[PROOFSTEP]
decide
[GOAL]
case false.true
⊢ xor false true = true ↔ Xor' (false = true) (true = true)
[PROOFSTEP]
exact by decide
[GOAL]
⊢ xor false true = true ↔ Xor' (false = true) (true = true)
[PROOFSTEP]
decide
[GOAL]
case true.false
⊢ xor true false = true ↔ Xor' (true = true) (false = true)
[PROOFSTEP]
exact by decide
[GOAL]
⊢ xor true false = true ↔ Xor' (true = true) (false = true)
[PROOFSTEP]
decide
[GOAL]
case true.true
⊢ xor true true = true ↔ Xor' (true = true) (true = true)
[PROOFSTEP]
exact by decide
[GOAL]
⊢ xor true true = true ↔ Xor' (true = true) (true = true)
[PROOFSTEP]
decide
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Bool
⊢ ((if c then a else b) = true) = if c then a = true else b = true
[PROOFSTEP]
by_cases c
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Bool
⊢ ((if c then a else b) = true) = if c then a = true else b = true
[PROOFSTEP]
by_cases c
[GOAL]
case pos
c : Prop
inst✝ : Decidable c
a b : Bool
h : c
⊢ ((if c then a else b) = true) = if c then a = true else b = true
[PROOFSTEP]
simp [*]
[GOAL]
case neg
c : Prop
inst✝ : Decidable c
a b : Bool
h : ¬c
⊢ ((if c then a else b) = true) = if c then a = true else b = true
[PROOFSTEP]
simp [*]
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Bool
⊢ ((if c then a else b) = false) = if c then a = false else b = false
[PROOFSTEP]
by_cases c
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Bool
⊢ ((if c then a else b) = false) = if c then a = false else b = false
[PROOFSTEP]
by_cases c
[GOAL]
case pos
c : Prop
inst✝ : Decidable c
a b : Bool
h : c
⊢ ((if c then a else b) = false) = if c then a = false else b = false
[PROOFSTEP]
simp [*]
[GOAL]
case neg
c : Prop
inst✝ : Decidable c
a b : Bool
h : ¬c
⊢ ((if c then a else b) = false) = if c then a = false else b = false
[PROOFSTEP]
simp [*]


[GOAL]
c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt
[PROOFSTEP]
by_cases c
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt
[PROOFSTEP]
by_cases c
[GOAL]
case pos
c : Prop
inst✝ : Decidable c
a b : Ordering
h : c
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt
[PROOFSTEP]
simp [*]
[GOAL]
case neg
c : Prop
inst✝ : Decidable c
a b : Ordering
h : ¬c
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt
[PROOFSTEP]
simp [*]
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq
[PROOFSTEP]
by_cases c
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq
[PROOFSTEP]
by_cases c
[GOAL]
case pos
c : Prop
inst✝ : Decidable c
a b : Ordering
h : c
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq
[PROOFSTEP]
simp [*]
[GOAL]
case neg
c : Prop
inst✝ : Decidable c
a b : Ordering
h : ¬c
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq
[PROOFSTEP]
simp [*]
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt
[PROOFSTEP]
by_cases c
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt
[PROOFSTEP]
by_cases c
[GOAL]
case pos
c : Prop
inst✝ : Decidable c
a b : Ordering
h : c
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt
[PROOFSTEP]
simp [*]
[GOAL]
case neg
c : Prop
inst✝ : Decidable c
a b : Ordering
h : ¬c
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
lt : α → α → Prop
inst✝ : DecidableRel lt
a b : α
⊢ (cmpUsing lt a b = Ordering.lt) = lt a b
[PROOFSTEP]
simp
[GOAL]
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ (cmpUsing lt a b = Ordering.gt) = lt b a
[PROOFSTEP]
simp only [cmpUsing, Ordering.ite_eq_gt_distrib, if_false_right_eq_and, and_true, if_false_left_eq_and]
[GOAL]
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ (¬lt a b ∧ lt b a) = lt b a
[PROOFSTEP]
apply propext
[GOAL]
case a
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ ¬lt a b ∧ lt b a ↔ lt b a
[PROOFSTEP]
apply Iff.intro
[GOAL]
case a.mp
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ ¬lt a b ∧ lt b a → lt b a
[PROOFSTEP]
exact fun h => h.2
[GOAL]
case a.mpr
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
⊢ lt b a → ¬lt a b ∧ lt b a
[PROOFSTEP]
intro hba
[GOAL]
case a.mpr
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
hba : lt b a
⊢ ¬lt a b ∧ lt b a
[PROOFSTEP]
constructor
[GOAL]
case a.mpr.left
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
hba : lt b a
⊢ ¬lt a b
[PROOFSTEP]
intro hab
[GOAL]
case a.mpr.left
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
hba : lt b a
hab : lt a b
⊢ False
[PROOFSTEP]
exact absurd (_root_.trans hab hba) (irrefl a)
[GOAL]
case a.mpr.right
α : Type u
lt : α → α → Prop
inst✝¹ : DecidableRel lt
inst✝ : IsStrictOrder α lt
a b : α
hba : lt b a
⊢ lt b a
[PROOFSTEP]
assumption
[GOAL]
α : Type u
lt : α → α → Prop
inst✝ : DecidableRel lt
a b : α
⊢ (cmpUsing lt a b = Ordering.eq) = (¬lt a b ∧ ¬lt b a)
[PROOFSTEP]
simp


[GOAL]
n m : ℕ
⊢ succ n * m = 0 → succ n = 0 ∨ m = 0
[PROOFSTEP]
rw [succ_mul]
[GOAL]
n m : ℕ
⊢ n * m + m = 0 → succ n = 0 ∨ m = 0
[PROOFSTEP]
intro h
[GOAL]
n m : ℕ
h : n * m + m = 0
⊢ succ n = 0 ∨ m = 0
[PROOFSTEP]
exact Or.inr (Nat.eq_zero_of_add_eq_zero_left h)
[GOAL]
m : ℕ
h : bit0 0 = bit0 (m + 1)
⊢ 0 = m + 1
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
h : bit0 (n + 1) = bit0 0
⊢ n + 1 = 0
[PROOFSTEP]
contradiction
[GOAL]
n m : ℕ
h : bit0 (n + 1) = bit0 (m + 1)
⊢ n + 1 = m + 1
[PROOFSTEP]
have : succ (succ (n + n)) = succ (succ (m + m)) :=
  by
  unfold bit0 at h ; simp [add_one, add_succ, succ_add] at h
  have aux : n + n = m + m := h; rw [aux]
[GOAL]
n m : ℕ
h : bit0 (n + 1) = bit0 (m + 1)
⊢ succ (succ (n + n)) = succ (succ (m + m))
[PROOFSTEP]
unfold bit0 at h
[GOAL]
n m : ℕ
h : n + 1 + (n + 1) = m + 1 + (m + 1)
⊢ succ (succ (n + n)) = succ (succ (m + m))
[PROOFSTEP]
simp [add_one, add_succ, succ_add] at h
[GOAL]
n m : ℕ
h : n + n = m + m
⊢ succ (succ (n + n)) = succ (succ (m + m))
[PROOFSTEP]
have aux : n + n = m + m := h
[GOAL]
n m : ℕ
h aux : n + n = m + m
⊢ succ (succ (n + n)) = succ (succ (m + m))
[PROOFSTEP]
rw [aux]
[GOAL]
n m : ℕ
h : bit0 (n + 1) = bit0 (m + 1)
this : succ (succ (n + n)) = succ (succ (m + m))
⊢ n + 1 = m + 1
[PROOFSTEP]
have : n + n = m + m := by repeat injection this with this
[GOAL]
n m : ℕ
h : bit0 (n + 1) = bit0 (m + 1)
this : succ (succ (n + n)) = succ (succ (m + m))
⊢ n + n = m + m
[PROOFSTEP]
repeat injection this with this
[GOAL]
n m : ℕ
h : bit0 (n + 1) = bit0 (m + 1)
this : succ (succ (n + n)) = succ (succ (m + m))
⊢ n + n = m + m
[PROOFSTEP]
injection this with this
[GOAL]
n m : ℕ
h : bit0 (n + 1) = bit0 (m + 1)
this : succ (n + n) = succ (m + m)
⊢ n + n = m + m
[PROOFSTEP]
injection this with this
[GOAL]

[PROOFSTEP]
injection this with this
[GOAL]
n m : ℕ
h : bit0 (n + 1) = bit0 (m + 1)
this✝ : succ (succ (n + n)) = succ (succ (m + m))
this : n + n = m + m
⊢ n + 1 = m + 1
[PROOFSTEP]
have : n = m := Nat.bit0_inj this
[GOAL]
n m : ℕ
h : bit0 (n + 1) = bit0 (m + 1)
this✝¹ : succ (succ (n + n)) = succ (succ (m + m))
this✝ : n + n = m + m
this : n = m
⊢ n + 1 = m + 1
[PROOFSTEP]
rw [this]
[GOAL]
n m : ℕ
h : bit1 n = bit1 m
⊢ succ (bit0 n) = succ (bit0 m)
[PROOFSTEP]
simp [Nat.bit1_eq_succ_bit0] at h
[GOAL]
n m : ℕ
h : bit0 n = bit0 m
⊢ succ (bit0 n) = succ (bit0 m)
[PROOFSTEP]
rw [h]
[GOAL]
n m : ℕ
h : bit1 n = bit1 m
this : succ (bit0 n) = succ (bit0 m)
⊢ bit0 n = bit0 m
[PROOFSTEP]
injection this
[GOAL]
h : 0 ≠ 0
⊢ 1 < bit1 0
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
_h : succ n ≠ 0
⊢ 1 < bit1 (succ n)
[PROOFSTEP]
rw [Nat.bit1_succ_eq]
[GOAL]
n : ℕ
_h : succ n ≠ 0
⊢ 1 < succ (succ (bit1 n))
[PROOFSTEP]
apply succ_lt_succ
[GOAL]
case a
n : ℕ
_h : succ n ≠ 0
⊢ 0 < bit1 n + 1
[PROOFSTEP]
apply zero_lt_succ
[GOAL]
h : 0 ≠ 0
⊢ 1 < bit0 0
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
_h : succ n ≠ 0
⊢ 1 < bit0 (succ n)
[PROOFSTEP]
rw [Nat.bit0_succ_eq]
[GOAL]
n : ℕ
_h : succ n ≠ 0
⊢ 1 < succ (succ (bit0 n))
[PROOFSTEP]
apply succ_lt_succ
[GOAL]
case a
n : ℕ
_h : succ n ≠ 0
⊢ 0 < bit0 n + 1
[PROOFSTEP]
apply zero_lt_succ
[GOAL]
n m : ℕ
h : n < succ m
this✝ : n ≤ m
this : succ (n + n) ≤ succ (m + m)
⊢ succ (n + n) ≤ succ m + m
[PROOFSTEP]
rw [succ_add]
[GOAL]
n m : ℕ
h : n < succ m
this✝ : n ≤ m
this : succ (n + n) ≤ succ (m + m)
⊢ succ (n + n) ≤ succ (m + m)
[PROOFSTEP]
assumption
[GOAL]
B : Sort u
n : ℕ
H1 : n = 0 → B
H2 : (m : ℕ) → n = succ m → B
⊢ B
[PROOFSTEP]
induction' h : n
[GOAL]
case zero
B : Sort u
n : ℕ
H1 : n = 0 → B
H2 : (m : ℕ) → n = succ m → B
x✝ : ℕ
h✝ : n = x✝
h : n = zero
⊢ B
[PROOFSTEP]
exact H1 h
[GOAL]
case succ
B : Sort u
n : ℕ
H1 : n = 0 → B
H2 : (m : ℕ) → n = succ m → B
x✝ : ℕ
h✝ : n = x✝
n✝ : ℕ
n_ih✝ : n = n✝ → B
h : n = succ n✝
⊢ B
[PROOFSTEP]
exact H2 _ h
[GOAL]
x y k : ℕ
h : k ≤ y
⊢ x ≤ y - k ↔ x + k ≤ y
[PROOFSTEP]
rw [← Nat.add_sub_cancel x k, Nat.sub_le_sub_iff_right h, Nat.add_sub_cancel]
[GOAL]
m n k : ℕ
⊢ m - n - k = m - k - n
[PROOFSTEP]
rw [Nat.sub_sub, Nat.sub_sub, Nat.add_comm]
[GOAL]
x : ℕ
d : Decidable (x % 2 = 1)
⊢ (bif decide (x % 2 = 1) then 1 else 0) = x % 2
[PROOFSTEP]
by_cases h : x % 2 = 1
[GOAL]
case pos
x : ℕ
d : Decidable (x % 2 = 1)
h : x % 2 = 1
⊢ (bif decide (x % 2 = 1) then 1 else 0) = x % 2
[PROOFSTEP]
simp! [*]
[GOAL]
case neg
x : ℕ
d : Decidable (x % 2 = 1)
h : ¬x % 2 = 1
⊢ (bif decide (x % 2 = 1) then 1 else 0) = x % 2
[PROOFSTEP]
cases mod_two_eq_zero_or_one x
[GOAL]
case neg.inl
x : ℕ
d : Decidable (x % 2 = 1)
h : ¬x % 2 = 1
h✝ : x % 2 = 0
⊢ (bif decide (x % 2 = 1) then 1 else 0) = x % 2
[PROOFSTEP]
simp! [*, Nat.zero_ne_one]
[GOAL]
case neg.inr
x : ℕ
d : Decidable (x % 2 = 1)
h : ¬x % 2 = 1
h✝ : x % 2 = 1
⊢ (bif decide (x % 2 = 1) then 1 else 0) = x % 2
[PROOFSTEP]
simp! [*, Nat.zero_ne_one]
[GOAL]
m n k : ℕ
H : 0 < m
⊢ m * n / (m * k) = n / k
[PROOFSTEP]
rw [← Nat.div_div_eq_div_mul, Nat.mul_div_cancel_left _ H]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
n : ℕ
pn : p n
m✝ m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc Nat.lbp k
k : ℕ
kn : n ≤ k + succ m
y : ℕ
r : Nat.lbp y k
_a : ∀ (k_1 : ℕ), k_1 ≤ k → ¬p k_1
⊢ n ≤ k + 1 + m
[PROOFSTEP]
rw [Nat.add_right_comm]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
n : ℕ
pn : p n
m✝ m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc Nat.lbp k
k : ℕ
kn : n ≤ k + succ m
y : ℕ
r : Nat.lbp y k
_a : ∀ (k_1 : ℕ), k_1 ≤ k → ¬p k_1
⊢ n ≤ k + m + 1
[PROOFSTEP]
exact kn
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
m : ℕ
IH : (y : ℕ) → Nat.lbp y m → (fun k => (∀ (n : ℕ), n < k → ¬p n) → { n // p n ∧ ∀ (m : ℕ), m < n → ¬p m }) y
al : ∀ (n : ℕ), n < m → ¬p n
pm : ¬p m
n : ℕ
h : n ≤ m
e : n = m
⊢ ¬p n
[PROOFSTEP]
rw [e]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
m : ℕ
IH : (y : ℕ) → Nat.lbp y m → (fun k => (∀ (n : ℕ), n < k → ¬p n) → { n // p n ∧ ∀ (m : ℕ), m < n → ¬p m }) y
al : ∀ (n : ℕ), n < m → ¬p n
pm : ¬p m
n : ℕ
h : n ≤ m
e : n = m
⊢ ¬p m
[PROOFSTEP]
exact pm
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
⊢ ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
[PROOFSTEP]
induction f with (simp only [Nat.toDigitsCore, List.length]; intro n l1 l2 hlen)
| zero => assumption
| succ f ih =>
  by_cases hx : n / b = 0
  case pos => simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
  case neg =>
    simp only [hx, if_false]
    specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
    simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
    exact ih trivial
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
⊢ ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
[PROOFSTEP]
induction f with (simp only [Nat.toDigitsCore, List.length]; intro n l1 l2 hlen)
| zero => assumption
| succ f ih =>
  by_cases hx : n / b = 0
  case pos => simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
  case neg =>
    simp only [hx, if_false]
    specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
    simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
    exact ih trivial
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
⊢ ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b zero n l1) = List.length (toDigitsCore b zero n l2)
[PROOFSTEP]
simp only [Nat.toDigitsCore, List.length]
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
⊢ ℕ → ∀ (l1 l2 : List Char), List.length l1 = List.length l2 → List.length l1 = List.length l2
[PROOFSTEP]
intro n l1 l2 hlen
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
⊢ List.length l1 = List.length l2
[PROOFSTEP]

| zero => assumption
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
⊢ List.length l1 = List.length l2
[PROOFSTEP]
assumption
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
⊢ ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 →
      List.length (toDigitsCore b (succ f) n l1) = List.length (toDigitsCore b (succ f) n l2)
[PROOFSTEP]
simp only [Nat.toDigitsCore, List.length]
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
⊢ ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 →
      List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
        List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
intro n l1 l2 hlen
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]

| succ f ih =>
  by_cases hx : n / b = 0
  case pos => simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
  case neg =>
    simp only [hx, if_false]
    specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
    simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
    exact ih trivial
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
by_cases hx : n / b = 0
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : n / b = 0
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : ¬n / b = 0
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
case pos => simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : n / b = 0
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
case pos => simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : n / b = 0
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : ¬n / b = 0
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
case neg =>
  simp only [hx, if_false]
  specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
  simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
  exact ih trivial
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : ¬n / b = 0
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
case neg =>
  simp only [hx, if_false]
  specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
  simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
  exact ih trivial
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : ¬n / b = 0
⊢ List.length (if n / b = 0 then digitChar (n % b) :: l1 else toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (if n / b = 0 then digitChar (n % b) :: l2 else toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
simp only [hx, if_false]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char),
    List.length l1 = List.length l2 → List.length (toDigitsCore b f n l1) = List.length (toDigitsCore b f n l2)
n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : ¬n / b = 0
⊢ List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : ¬n / b = 0
ih :
  List.length (digitChar (n % b) :: l1) = List.length (digitChar (n % b) :: l2) →
    List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
      List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
⊢ List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f n : ℕ
l1 l2 : List Char
hlen : List.length l1 = List.length l2
hx : ¬n / b = 0
ih :
  True →
    List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
      List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
⊢ List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l1)) =
    List.length (toDigitsCore b f (n / b) (digitChar (n % b) :: l2))
[PROOFSTEP]
exact ih trivial
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
[PROOFSTEP]
induction f with (intro n c tl; simp only [Nat.toDigitsCore, List.length])
| succ f ih =>
  by_cases hnb : (n / b) = 0
  case pos => simp only [hnb, if_true, List.length]
  case neg =>
    generalize hx : Nat.digitChar (n % b) = x
    simp only [hx, hnb, if_false] at ih
    simp only [hnb, if_false]
    specialize ih (n / b) c (x :: tl)
    rw [← ih]
    have lens_eq : (x :: (c :: tl)).length = (c :: x :: tl).length := by simp
    apply to_digits_core_lens_eq_aux
    exact lens_eq
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
[PROOFSTEP]
induction f with (intro n c tl; simp only [Nat.toDigitsCore, List.length])
| succ f ih =>
  by_cases hnb : (n / b) = 0
  case pos => simp only [hnb, if_true, List.length]
  case neg =>
    generalize hx : Nat.digitChar (n % b) = x
    simp only [hx, hnb, if_false] at ih
    simp only [hnb, if_false]
    specialize ih (n / b) c (x :: tl)
    rw [← ih]
    have lens_eq : (x :: (c :: tl)).length = (c :: x :: tl).length := by simp
    apply to_digits_core_lens_eq_aux
    exact lens_eq
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b (succ f) n (c :: tl)) = List.length (toDigitsCore b (succ f) n tl) + 1
[PROOFSTEP]
intro n c tl
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
⊢ List.length (toDigitsCore b (succ f) n (c :: tl)) = List.length (toDigitsCore b (succ f) n tl) + 1
[PROOFSTEP]
simp only [Nat.toDigitsCore, List.length]
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
[PROOFSTEP]

| succ f ih =>
  by_cases hnb : (n / b) = 0
  case pos => simp only [hnb, if_true, List.length]
  case neg =>
    generalize hx : Nat.digitChar (n % b) = x
    simp only [hx, hnb, if_false] at ih
    simp only [hnb, if_false]
    specialize ih (n / b) c (x :: tl)
    rw [← ih]
    have lens_eq : (x :: (c :: tl)).length = (c :: x :: tl).length := by simp
    apply to_digits_core_lens_eq_aux
    exact lens_eq
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
[PROOFSTEP]
by_cases hnb : (n / b) = 0
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : n / b = 0
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
[PROOFSTEP]
case pos => simp only [hnb, if_true, List.length]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : n / b = 0
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
[PROOFSTEP]
case pos => simp only [hnb, if_true, List.length]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : n / b = 0
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
[PROOFSTEP]
simp only [hnb, if_true, List.length]
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
[PROOFSTEP]
case neg =>
  generalize hx : Nat.digitChar (n % b) = x
  simp only [hx, hnb, if_false] at ih
  simp only [hnb, if_false]
  specialize ih (n / b) c (x :: tl)
  rw [← ih]
  have lens_eq : (x :: (c :: tl)).length = (c :: x :: tl).length := by simp
  apply to_digits_core_lens_eq_aux
  exact lens_eq
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
[PROOFSTEP]
case neg =>
  generalize hx : Nat.digitChar (n % b) = x
  simp only [hx, hnb, if_false] at ih
  simp only [hnb, if_false]
  specialize ih (n / b) c (x :: tl)
  rw [← ih]
  have lens_eq : (x :: (c :: tl)).length = (c :: x :: tl).length := by simp
  apply to_digits_core_lens_eq_aux
  exact lens_eq
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
⊢ List.length
      (if n / b = 0 then digitChar (n % b) :: c :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: c :: tl)) =
    List.length (if n / b = 0 then digitChar (n % b) :: tl else toDigitsCore b f (n / b) (digitChar (n % b) :: tl)) + 1
[PROOFSTEP]
generalize hx : Nat.digitChar (n % b) = x
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : digitChar (n % b) = x
⊢ List.length (if n / b = 0 then x :: c :: tl else toDigitsCore b f (n / b) (x :: c :: tl)) =
    List.length (if n / b = 0 then x :: tl else toDigitsCore b f (n / b) (x :: tl)) + 1
[PROOFSTEP]
simp only [hx, hnb, if_false] at ih
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : digitChar (n % b) = x
⊢ List.length (if n / b = 0 then x :: c :: tl else toDigitsCore b f (n / b) (x :: c :: tl)) =
    List.length (if n / b = 0 then x :: tl else toDigitsCore b f (n / b) (x :: tl)) + 1
[PROOFSTEP]
simp only [hnb, if_false]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f : ℕ
ih :
  ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b f n (c :: tl)) = List.length (toDigitsCore b f n tl) + 1
n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : digitChar (n % b) = x
⊢ List.length (toDigitsCore b f (n / b) (x :: c :: tl)) = List.length (toDigitsCore b f (n / b) (x :: tl)) + 1
[PROOFSTEP]
specialize ih (n / b) c (x :: tl)
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : digitChar (n % b) = x
ih : List.length (toDigitsCore b f (n / b) (c :: x :: tl)) = List.length (toDigitsCore b f (n / b) (x :: tl)) + 1
⊢ List.length (toDigitsCore b f (n / b) (x :: c :: tl)) = List.length (toDigitsCore b f (n / b) (x :: tl)) + 1
[PROOFSTEP]
rw [← ih]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : digitChar (n % b) = x
ih : List.length (toDigitsCore b f (n / b) (c :: x :: tl)) = List.length (toDigitsCore b f (n / b) (x :: tl)) + 1
⊢ List.length (toDigitsCore b f (n / b) (x :: c :: tl)) = List.length (toDigitsCore b f (n / b) (c :: x :: tl))
[PROOFSTEP]
have lens_eq : (x :: (c :: tl)).length = (c :: x :: tl).length := by simp
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : digitChar (n % b) = x
ih : List.length (toDigitsCore b f (n / b) (c :: x :: tl)) = List.length (toDigitsCore b f (n / b) (x :: tl)) + 1
⊢ List.length (x :: c :: tl) = List.length (c :: x :: tl)
[PROOFSTEP]
simp
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : digitChar (n % b) = x
ih : List.length (toDigitsCore b f (n / b) (c :: x :: tl)) = List.length (toDigitsCore b f (n / b) (x :: tl)) + 1
lens_eq : List.length (x :: c :: tl) = List.length (c :: x :: tl)
⊢ List.length (toDigitsCore b f (n / b) (x :: c :: tl)) = List.length (toDigitsCore b f (n / b) (c :: x :: tl))
[PROOFSTEP]
apply to_digits_core_lens_eq_aux
[GOAL]
case a
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b f n : ℕ
c : Char
tl : List Char
hnb : ¬n / b = 0
x : Char
hx : digitChar (n % b) = x
ih : List.length (toDigitsCore b f (n / b) (c :: x :: tl)) = List.length (toDigitsCore b f (n / b) (x :: tl)) + 1
lens_eq : List.length (x :: c :: tl) = List.length (c :: x :: tl)
⊢ List.length (x :: c :: tl) = List.length (c :: x :: tl)
[PROOFSTEP]
exact lens_eq
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char),
    List.length (toDigitsCore b zero n (c :: tl)) = List.length (toDigitsCore b zero n tl) + 1
[PROOFSTEP]
intro n c tl
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b n : ℕ
c : Char
tl : List Char
⊢ List.length (toDigitsCore b zero n (c :: tl)) = List.length (toDigitsCore b zero n tl) + 1
[PROOFSTEP]
simp only [Nat.toDigitsCore, List.length]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
n b e : ℕ
h_b_pos : 0 < b
⊢ n < b ^ succ e → n / b < b ^ e
[PROOFSTEP]
simp only [Nat.pow_succ]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
n b e : ℕ
h_b_pos : 0 < b
⊢ n < b ^ e * b → n / b < b ^ e
[PROOFSTEP]
exact (@Nat.div_lt_iff_lt_mul b n (b ^ e) h_b_pos).mpr
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ e
h_e_pos : 0 < e
⊢ List.length (toDigitsCore b f n []) ≤ e
[PROOFSTEP]
induction f generalizing n e hlt h_e_pos with simp only [Nat.toDigitsCore, List.length, Nat.zero_le]
| succ f ih =>
  cases e with
  | zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
  | succ e =>
    by_cases h_pred_pos : 0 < e
    case pos =>
      have _ : 0 < b := Nat.lt_trans (by decide) h
      specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
      by_cases hdiv_ten : n / b = 0
      case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
      case neg =>
        simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
        exact Nat.succ_le_succ ih
    case neg =>
      have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
      rw [‹e = 0›]
      have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
      have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
      simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ e
h_e_pos : 0 < e
⊢ List.length (toDigitsCore b f n []) ≤ e
[PROOFSTEP]
induction f generalizing n e hlt h_e_pos with simp only [Nat.toDigitsCore, List.length, Nat.zero_le]
| succ f ih =>
  cases e with
  | zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
  | succ e =>
    by_cases h_pred_pos : 0 < e
    case pos =>
      have _ : 0 < b := Nat.lt_trans (by decide) h
      specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
      by_cases hdiv_ten : n / b = 0
      case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
      case neg =>
        simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
        exact Nat.succ_le_succ ih
    case neg =>
      have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
      rw [‹e = 0›]
      have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
      have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
      simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ e
h_e_pos : 0 < e
⊢ List.length (toDigitsCore b (succ f) n []) ≤ e
[PROOFSTEP]
simp only [Nat.toDigitsCore, List.length, Nat.zero_le]
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ e
h_e_pos : 0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ e
[PROOFSTEP]

| succ f ih =>
  cases e with
  | zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
  | succ e =>
    by_cases h_pred_pos : 0 < e
    case pos =>
      have _ : 0 < b := Nat.lt_trans (by decide) h
      specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
      by_cases hdiv_ten : n / b = 0
      case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
      case neg =>
        simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
        exact Nat.succ_le_succ ih
    case neg =>
      have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
      rw [‹e = 0›]
      have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
      have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
      simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ e
h_e_pos : 0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ e
[PROOFSTEP]
cases e with
| zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
| succ e =>
  by_cases h_pred_pos : 0 < e
  case pos =>
    have _ : 0 < b := Nat.lt_trans (by decide) h
    specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
    by_cases hdiv_ten : n / b = 0
    case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
    case neg =>
      simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
      exact Nat.succ_le_succ ih
  case neg =>
    have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
    rw [‹e = 0›]
    have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
    have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
    simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ e
h_e_pos : 0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ e
[PROOFSTEP]
cases e with
| zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
| succ e =>
  by_cases h_pred_pos : 0 < e
  case pos =>
    have _ : 0 < b := Nat.lt_trans (by decide) h
    specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
    by_cases hdiv_ten : n / b = 0
    case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
    case neg =>
      simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
      exact Nat.succ_le_succ ih
  case neg =>
    have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
    rw [‹e = 0›]
    have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
    have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
    simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
case succ.zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n : ℕ
hlt : n < b ^ zero
h_e_pos : 0 < zero
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ zero
[PROOFSTEP]

| zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
[GOAL]
case succ.zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n : ℕ
hlt : n < b ^ zero
h_e_pos : 0 < zero
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ zero
[PROOFSTEP]
exact False.elim (Nat.lt_irrefl 0 h_e_pos)
[GOAL]
case succ.succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]

| succ e =>
  by_cases h_pred_pos : 0 < e
  case pos =>
    have _ : 0 < b := Nat.lt_trans (by decide) h
    specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
    by_cases hdiv_ten : n / b = 0
    case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
    case neg =>
      simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
      exact Nat.succ_le_succ ih
  case neg =>
    have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
    rw [‹e = 0›]
    have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
    have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
    simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
case succ.succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
by_cases h_pred_pos : 0 < e
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
case pos =>
  have _ : 0 < b := Nat.lt_trans (by decide) h
  specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
  by_cases hdiv_ten : n / b = 0
  case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
  case neg =>
    simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
    exact Nat.succ_le_succ ih
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
case pos =>
  have _ : 0 < b := Nat.lt_trans (by decide) h
  specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
  by_cases hdiv_ten : n / b = 0
  case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
  case neg =>
    simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
    exact Nat.succ_le_succ ih
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
have _ : 0 < b := Nat.lt_trans (by decide) h
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
⊢ 0 < 1
[PROOFSTEP]
decide
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
specialize ih (n / b) e (nat_repr_len_aux n b e ‹0 < b› hlt) h_pred_pos
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
by_cases hdiv_ten : n / b = 0
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : n / b = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : ¬n / b = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : n / b = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
case pos => simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : n / b = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
simp only [hdiv_ten]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : n / b = 0
⊢ List.length (if True then [digitChar (n % b)] else toDigitsCore b f 0 [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
exact Nat.le.step h_pred_pos
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : ¬n / b = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
case neg =>
  simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
  exact Nat.succ_le_succ ih
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : ¬n / b = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
case neg =>
  simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
  exact Nat.succ_le_succ ih
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : ¬n / b = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
simp only [hdiv_ten, to_digits_core_lens_eq b f (n / b) (Nat.digitChar $ n % b), if_false]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : 0 < e
x✝ : 0 < b
ih : List.length (toDigitsCore b f (n / b) []) ≤ e
hdiv_ten : ¬n / b = 0
⊢ List.length (toDigitsCore b f (n / b) []) + 1 ≤ succ e
[PROOFSTEP]
exact Nat.succ_le_succ ih
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
case neg =>
  have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
  rw [‹e = 0›]
  have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
  have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
  simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
case neg =>
  have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
  rw [‹e = 0›]
  have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
  have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
  simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
have _ : e = 0 := Nat.eq_zero_of_nonpos e h_pred_pos
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
x✝ : e = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ e
[PROOFSTEP]
rw [‹e = 0›]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
x✝ : e = 0
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ 0
[PROOFSTEP]
have _ : b ^ 1 = b := by simp only [pow_succ, pow_zero, Nat.one_mul]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
x✝ : e = 0
⊢ b ^ 1 = b
[PROOFSTEP]
simp only [pow_succ, pow_zero, Nat.one_mul]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
x✝¹ : e = 0
x✝ : b ^ 1 = b
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ 0
[PROOFSTEP]
have _ : n < b := ‹b ^ 1 = b› ▸ (‹e = 0› ▸ hlt : n < b ^ Nat.succ 0)
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → List.length (toDigitsCore b f n []) ≤ e
n e : ℕ
hlt : n < b ^ succ e
h_e_pos : 0 < succ e
h_pred_pos : ¬0 < e
x✝² : e = 0
x✝¹ : b ^ 1 = b
x✝ : n < b
⊢ List.length (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b f (n / b) [digitChar (n % b)]) ≤ succ 0
[PROOFSTEP]
simp only [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0), if_true, List.length]
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
b : ℕ
h : 2 ≤ b
n e : ℕ
hlt : n < b ^ e
h_e_pos : 0 < e
⊢ List.length (toDigitsCore b zero n []) ≤ e
[PROOFSTEP]
simp only [Nat.toDigitsCore, List.length, Nat.zero_le]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
n e : ℕ
⊢ 0 < e → n < 10 ^ e → String.length (Nat.repr n) ≤ e
[PROOFSTEP]
cases n with (intro e0 he; simp only [Nat.repr, Nat.toDigits, String.length, List.asString])
| zero => assumption
| succ n =>
  by_cases hterm : n.succ / 10 = 0
  case pos => simp only [hterm, Nat.toDigitsCore]; assumption
  case neg => exact to_digits_core_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
n e : ℕ
⊢ 0 < e → n < 10 ^ e → String.length (Nat.repr n) ≤ e
[PROOFSTEP]
cases n with (intro e0 he; simp only [Nat.repr, Nat.toDigits, String.length, List.asString])
| zero => assumption
| succ n =>
  by_cases hterm : n.succ / 10 = 0
  case pos => simp only [hterm, Nat.toDigitsCore]; assumption
  case neg => exact to_digits_core_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e : ℕ
⊢ 0 < e → zero < 10 ^ e → String.length (Nat.repr zero) ≤ e
[PROOFSTEP]
intro e0 he
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e : ℕ
e0 : 0 < e
he : zero < 10 ^ e
⊢ String.length (Nat.repr zero) ≤ e
[PROOFSTEP]
simp only [Nat.repr, Nat.toDigits, String.length, List.asString]
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e : ℕ
e0 : 0 < e
he : zero < 10 ^ e
⊢ List.length (toDigitsCore 10 (zero + 1) zero []) ≤ e
[PROOFSTEP]

| zero => assumption
[GOAL]
case zero
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e : ℕ
e0 : 0 < e
he : zero < 10 ^ e
⊢ List.length (toDigitsCore 10 (zero + 1) zero []) ≤ e
[PROOFSTEP]
assumption
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
⊢ 0 < e → succ n < 10 ^ e → String.length (Nat.repr (succ n)) ≤ e
[PROOFSTEP]
intro e0 he
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
⊢ String.length (Nat.repr (succ n)) ≤ e
[PROOFSTEP]
simp only [Nat.repr, Nat.toDigits, String.length, List.asString]
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
[PROOFSTEP]

| succ n =>
  by_cases hterm : n.succ / 10 = 0
  case pos => simp only [hterm, Nat.toDigitsCore]; assumption
  case neg => exact to_digits_core_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0
[GOAL]
case succ
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
[PROOFSTEP]
by_cases hterm : n.succ / 10 = 0
[GOAL]
case pos
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : succ n / 10 = 0
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : ¬succ n / 10 = 0
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
[PROOFSTEP]
case pos => simp only [hterm, Nat.toDigitsCore]; assumption
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : succ n / 10 = 0
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
[PROOFSTEP]
case pos => simp only [hterm, Nat.toDigitsCore]; assumption
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : succ n / 10 = 0
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
[PROOFSTEP]
simp only [hterm, Nat.toDigitsCore]
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : succ n / 10 = 0
⊢ List.length
      (if True then [digitChar (succ n % 10)]
      else
        if True then [digitChar (0 % 10), digitChar (succ n % 10)]
        else toDigitsCore 10 n (0 / 10) [digitChar (0 % 10), digitChar (succ n % 10)]) ≤
    e
[PROOFSTEP]
assumption
[GOAL]
case neg
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : ¬succ n / 10 = 0
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
[PROOFSTEP]
case neg => exact to_digits_core_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : ¬succ n / 10 = 0
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
[PROOFSTEP]
case neg => exact to_digits_core_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : ¬succ n / 10 = 0
⊢ List.length (toDigitsCore 10 (succ n + 1) (succ n) []) ≤ e
[PROOFSTEP]
exact to_digits_core_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0
[GOAL]
p : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
e n : ℕ
e0 : 0 < e
he : succ n < 10 ^ e
hterm : ¬succ n / 10 = 0
⊢ 2 ≤ 10
[PROOFSTEP]
decide