[GOAL]
P : PartENat → Prop
⊢ ∀ (a : PartENat), P ⊤ → (∀ (n : ℕ), P ↑n) → P a
[PROOFSTEP]
exact PartENat.casesOn'
[GOAL]
x : PartENat
⊢ x + ⊤ = ⊤
[PROOFSTEP]
rw [add_comm, top_add]
[GOAL]
x : PartENat
h : x.Dom
⊢ ↑(Part.get x h) = x
[PROOFSTEP]
exact Part.ext' (iff_of_true trivial h) fun _ _ => rfl
[GOAL]
x : ℕ
h : (↑x).Dom
⊢ Part.get (↑x) h = x
[PROOFSTEP]
rw [← natCast_inj, natCast_get]
[GOAL]
x : ℕ
y : PartENat
h : (↑x + y).Dom
⊢ Part.get (↑x + y) h = x + Part.get y (_ : y.Dom)
[PROOFSTEP]
rfl
[GOAL]
a : PartENat
ha : a.Dom
b : ℕ
⊢ Part.get a ha = b ↔ a = ↑b
[PROOFSTEP]
rw [get_eq_iff_eq_some]
[GOAL]
a : PartENat
ha : a.Dom
b : ℕ
⊢ a = ↑b ↔ a = ↑b
[PROOFSTEP]
rfl
[GOAL]
x : PartENat
y : ℕ
h : x ≤ ↑y
⊢ x.Dom
[PROOFSTEP]
exact dom_of_le_some h
[GOAL]
x y : PartENat
inst✝¹ : Decidable x.Dom
inst✝ : Decidable y.Dom
hx : x.Dom
⊢ ?m.35650 x y hx ↔ x ≤ y
[PROOFSTEP]
rw [le_def]
[GOAL]
x y : PartENat
⊢ x < y ↔ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
[PROOFSTEP]
rw [lt_iff_le_not_le, le_def, le_def, not_exists]
[GOAL]
x y : PartENat
⊢ ((∃ h, ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy) ∧
      ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy) ↔
    ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
[PROOFSTEP]
constructor
[GOAL]
case mp
x y : PartENat
⊢ ((∃ h, ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy) ∧
      ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy) →
    ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
[PROOFSTEP]
rintro ⟨⟨hyx, H⟩, h⟩
[GOAL]
case mp.intro.intro
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
[PROOFSTEP]
by_cases hx : x.Dom
[GOAL]
case pos
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : x.Dom
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
[PROOFSTEP]
use hx
[GOAL]
case h
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : x.Dom
⊢ ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
[PROOFSTEP]
intro hy
[GOAL]
case h
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : x.Dom
hy : y.Dom
⊢ Part.get x hx < Part.get y hy
[PROOFSTEP]
specialize H hy
[GOAL]
case h
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : Part.get x (_ : x.Dom) ≤ Part.get y hy
⊢ Part.get x hx < Part.get y hy
[PROOFSTEP]
specialize h fun _ => hy
[GOAL]
case h
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : Part.get x (_ : x.Dom) ≤ Part.get y hy
h : ¬∀ (hy_1 : x.Dom), Part.get y hy ≤ Part.get x hy_1
⊢ Part.get x hx < Part.get y hy
[PROOFSTEP]
rw [not_forall] at h
[GOAL]
case h
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : Part.get x (_ : x.Dom) ≤ Part.get y hy
h : ∃ x_1, ¬Part.get y hy ≤ Part.get x x_1
⊢ Part.get x hx < Part.get y hy
[PROOFSTEP]
cases' h with hx' h
[GOAL]
case h.intro
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : Part.get x (_ : x.Dom) ≤ Part.get y hy
hx' : x.Dom
h : ¬Part.get y hy ≤ Part.get x hx'
⊢ Part.get x hx < Part.get y hy
[PROOFSTEP]
rw [not_le] at h
[GOAL]
case h.intro
x y : PartENat
hyx : y.Dom → x.Dom
hx : x.Dom
hy : y.Dom
H : Part.get x (_ : x.Dom) ≤ Part.get y hy
hx' : x.Dom
h : Part.get x hx' < Part.get y hy
⊢ Part.get x hx < Part.get y hy
[PROOFSTEP]
exact h
[GOAL]
case neg
x y : PartENat
h : ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : ¬x.Dom
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
[PROOFSTEP]
specialize h fun hx' => (hx hx').elim
[GOAL]
case neg
x y : PartENat
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : ¬x.Dom
h : ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
[PROOFSTEP]
rw [not_forall] at h
[GOAL]
case neg
x y : PartENat
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : ¬x.Dom
h : ∃ x_1, ¬Part.get y (_ : y.Dom) ≤ Part.get x x_1
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
[PROOFSTEP]
cases' h with hx' h
[GOAL]
case neg.intro
x y : PartENat
hyx : y.Dom → x.Dom
H : ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy
hx : ¬x.Dom
hx' : x.Dom
h : ¬Part.get y (_ : y.Dom) ≤ Part.get x hx'
⊢ ∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
[PROOFSTEP]
exact (hx hx').elim
[GOAL]
case mpr
x y : PartENat
⊢ (∃ hx, ∀ (hy : y.Dom), Part.get x hx < Part.get y hy) →
    (∃ h, ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy) ∧
      ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
[PROOFSTEP]
rintro ⟨hx, H⟩
[GOAL]
case mpr.intro
x y : PartENat
hx : x.Dom
H : ∀ (hy : y.Dom), Part.get x hx < Part.get y hy
⊢ (∃ h, ∀ (hy : y.Dom), Part.get x (_ : x.Dom) ≤ Part.get y hy) ∧
    ∀ (x_1 : x.Dom → y.Dom), ¬∀ (hy : x.Dom), Part.get y (_ : y.Dom) ≤ Part.get x hy
[PROOFSTEP]
exact ⟨⟨fun _ => hx, fun hy => (H hy).le⟩, fun hxy h => not_lt_of_le (h _) (H _)⟩
[GOAL]
x y : ℕ
⊢ ↑x ≤ ↑y ↔ x ≤ y
[PROOFSTEP]
exact ⟨fun ⟨_, h⟩ => h trivial, fun h => ⟨fun _ => trivial, fun _ => h⟩⟩
[GOAL]
x y : ℕ
⊢ ↑x < ↑y ↔ x < y
[PROOFSTEP]
rw [lt_iff_le_not_le, lt_iff_le_not_le, coe_le_coe, coe_le_coe]
[GOAL]
x y : PartENat
hx : x.Dom
hy : y.Dom
⊢ Part.get x hx ≤ Part.get y hy ↔ x ≤ y
[PROOFSTEP]
conv =>
  lhs
  rw [← coe_le_coe, natCast_get, natCast_get]
[GOAL]
x y : PartENat
hx : x.Dom
hy : y.Dom
| Part.get x hx ≤ Part.get y hy ↔ x ≤ y
[PROOFSTEP]
  lhs
  rw [← coe_le_coe, natCast_get, natCast_get]
[GOAL]
x y : PartENat
hx : x.Dom
hy : y.Dom
| Part.get x hx ≤ Part.get y hy ↔ x ≤ y
[PROOFSTEP]
  lhs
  rw [← coe_le_coe, natCast_get, natCast_get]
[GOAL]
x y : PartENat
hx : x.Dom
hy : y.Dom
| Part.get x hx ≤ Part.get y hy ↔ x ≤ y
[PROOFSTEP]
lhs
[GOAL]
x y : PartENat
hx : x.Dom
hy : y.Dom
| Part.get x hx ≤ Part.get y hy
[PROOFSTEP]
rw [← coe_le_coe, natCast_get, natCast_get]
[GOAL]
x : PartENat
n : ℕ
⊢ x ≤ ↑n ↔ ∃ h, Part.get x h ≤ n
[PROOFSTEP]
show (∃ h : True → x.Dom, _) ↔ ∃ h : x.Dom, x.get h ≤ n
[GOAL]
x : PartENat
n : ℕ
⊢ (∃ h, ∀ (hy : (↑n).Dom), Part.get x (_ : x.Dom) ≤ Part.get (↑n) hy) ↔ ∃ h, Part.get x h ≤ n
[PROOFSTEP]
simp only [forall_prop_of_true, dom_natCast, get_natCast']
[GOAL]
x : PartENat
n : ℕ
⊢ x < ↑n ↔ ∃ h, Part.get x h < n
[PROOFSTEP]
simp only [lt_def, forall_prop_of_true, get_natCast', dom_natCast]
[GOAL]
n : ℕ
x : PartENat
⊢ ↑n ≤ x ↔ ∀ (h : x.Dom), n ≤ Part.get x h
[PROOFSTEP]
rw [← some_eq_natCast]
[GOAL]
n : ℕ
x : PartENat
⊢ ↑n ≤ x ↔ ∀ (h : x.Dom), n ≤ Part.get x h
[PROOFSTEP]
simp only [le_def, exists_prop_of_true, dom_some, forall_true_iff]
[GOAL]
n : ℕ
x : PartENat
⊢ (∀ (hy : x.Dom), Part.get ↑n (_ : (↑n).Dom) ≤ Part.get x hy) ↔ ∀ (h : x.Dom), n ≤ Part.get x h
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
x : PartENat
⊢ ↑n < x ↔ ∀ (h : x.Dom), n < Part.get x h
[PROOFSTEP]
rw [← some_eq_natCast]
[GOAL]
n : ℕ
x : PartENat
⊢ ↑n < x ↔ ∀ (h : x.Dom), n < Part.get x h
[PROOFSTEP]
simp only [lt_def, exists_prop_of_true, dom_some, forall_true_iff]
[GOAL]
n : ℕ
x : PartENat
⊢ (∀ (hy : x.Dom), Part.get ↑n (_ : (↑n).Dom) < Part.get x hy) ↔ ∀ (h : x.Dom), n < Part.get x h
[PROOFSTEP]
rfl
[GOAL]
⊢ ¬1 = 0
[PROOFSTEP]
decide
[GOAL]
x : ℕ
h : ↑x = ⊤
⊢ ¬(↑x).Dom = ⊤.Dom
[PROOFSTEP]
simp only [dom_natCast]
[GOAL]
x : ℕ
h : ↑x = ⊤
⊢ ¬True = ⊤.Dom
[PROOFSTEP]
exact true_ne_false
[GOAL]
x : PartENat
⊢ x ≠ ⊤ ↔ ∃ n, x = ↑n
[PROOFSTEP]
simpa only [← some_eq_natCast] using Part.ne_none_iff
[GOAL]
x : PartENat
⊢ x ≠ ⊤ ↔ x.Dom
[PROOFSTEP]
classical exact not_iff_comm.1 Part.eq_none_iff'.symm
[GOAL]
x : PartENat
⊢ x ≠ ⊤ ↔ x.Dom
[PROOFSTEP]
exact not_iff_comm.1 Part.eq_none_iff'.symm
[GOAL]
x : PartENat
⊢ x = ⊤ ↔ ∀ (n : ℕ), ↑n < x
[PROOFSTEP]
constructor
[GOAL]
case mp
x : PartENat
⊢ x = ⊤ → ∀ (n : ℕ), ↑n < x
[PROOFSTEP]
rintro rfl n
[GOAL]
case mp
n : ℕ
⊢ ↑n < ⊤
[PROOFSTEP]
exact natCast_lt_top _
[GOAL]
case mpr
x : PartENat
⊢ (∀ (n : ℕ), ↑n < x) → x = ⊤
[PROOFSTEP]
contrapose!
[GOAL]
case mpr
x : PartENat
⊢ x ≠ ⊤ → ∃ n, ¬↑n < x
[PROOFSTEP]
rw [ne_top_iff]
[GOAL]
case mpr
x : PartENat
⊢ (∃ n, x = ↑n) → ∃ n, ¬↑n < x
[PROOFSTEP]
rintro ⟨n, rfl⟩
[GOAL]
case mpr.intro
n : ℕ
⊢ ∃ n_1, ¬↑n_1 < ↑n
[PROOFSTEP]
exact ⟨n, irrefl _⟩
[GOAL]
x : PartENat
⊢ 0 < ⊤ ↔ 1 ≤ ⊤
[PROOFSTEP]
simp only [iff_true_iff, le_top, natCast_lt_top, ← @Nat.cast_zero PartENat]
[GOAL]
x : PartENat
n : ℕ
⊢ 0 < ↑n ↔ 1 ≤ ↑n
[PROOFSTEP]
rw [← Nat.cast_zero, ← Nat.cast_one, PartENat.coe_lt_coe, PartENat.coe_le_coe]
[GOAL]
x : PartENat
n : ℕ
⊢ 0 < n ↔ 1 ≤ n
[PROOFSTEP]
rfl
[GOAL]
src✝ : PartialOrder PartENat := partialOrder
a b : PartENat
⊢ max a b = if a ≤ b then b else a
[PROOFSTEP]
change (fun a b => a ⊔ b) a b = _
[GOAL]
src✝ : PartialOrder PartENat := partialOrder
a b : PartENat
⊢ (fun a b => a ⊔ b) a b = if a ≤ b then b else a
[PROOFSTEP]
rw [@sup_eq_maxDefault PartENat _ (id _) _]
[GOAL]
src✝ : PartialOrder PartENat := partialOrder
a b : PartENat
⊢ maxDefault a b = if a ≤ b then b else a
src✝ : PartialOrder PartENat := partialOrder a b : PartENat ⊢ DecidableRel fun x x_1 => x ≤ x_1
[PROOFSTEP]
rfl
[GOAL]
src✝¹ : LinearOrder PartENat := linearOrder
src✝ : AddCommMonoid PartENat := addCommMonoid
a b : PartENat
x✝ : a ≤ b
c : PartENat
h₁ : b.Dom → a.Dom
h₂ : ∀ (hy : b.Dom), Part.get a (_ : a.Dom) ≤ Part.get b hy
⊢ ⊤ + a ≤ ⊤ + b
[PROOFSTEP]
simp
[GOAL]
src✝¹ : LinearOrder PartENat := linearOrder
src✝ : AddCommMonoid PartENat := addCommMonoid
a b : PartENat
x✝ : a ≤ b
c✝ : PartENat
h₁ : b.Dom → a.Dom
h₂ : ∀ (hy : b.Dom), Part.get a (_ : a.Dom) ≤ Part.get b hy
c : ℕ
h : (↑c + b).Dom
⊢ Part.get (↑c + a) (_ : (↑c).Dom ∧ a.Dom) ≤ Part.get (↑c + b) h
[PROOFSTEP]
simpa only [coe_add_get] using add_le_add_left (h₂ _) c
[GOAL]
src✝² : SemilatticeSup PartENat := semilatticeSup
src✝¹ : OrderBot PartENat := orderBot
src✝ : OrderedAddCommMonoid PartENat := orderedAddCommMonoid
a✝ b✝ : PartENat
b a : ℕ
h : ↑a ≤ ↑b
⊢ ↑b = ↑a + ↑(b - a)
[PROOFSTEP]
rw [← Nat.cast_add, natCast_inj, add_comm, tsub_add_cancel_of_le (coe_le_coe.1 h)]
[GOAL]
x y : PartENat
n : ℕ
h : x + y = ↑n
⊢ x = ↑(n - Part.get y (_ : y.Dom))
[PROOFSTEP]
lift x to ℕ using dom_of_le_natCast ((le_add_right le_rfl).trans_eq h)
[GOAL]
case intro
y : PartENat
n x : ℕ
h : ↑x + y = ↑n
⊢ ↑x = ↑(n - Part.get y (_ : y.Dom))
[PROOFSTEP]
lift y to ℕ using dom_of_le_natCast ((le_add_left le_rfl).trans_eq h)
[GOAL]
case intro.intro
n x y : ℕ
h : ↑x + ↑y = ↑n
⊢ ↑x = ↑(n - Part.get ↑y (_ : (↑y).Dom))
[PROOFSTEP]
rw [← Nat.cast_add, natCast_inj] at h
[GOAL]
case intro.intro
n x y : ℕ
h✝ : ↑x + ↑y = ↑n
h : x + y = n
⊢ ↑x = ↑(n - Part.get ↑y (_ : (↑y).Dom))
[PROOFSTEP]
rw [get_natCast, natCast_inj, eq_tsub_of_add_eq h]
[GOAL]
x y z : PartENat
h : x < y
hz : z ≠ ⊤
⊢ x + z < y + z
[PROOFSTEP]
rcases ne_top_iff.mp (ne_top_of_lt h) with ⟨m, rfl⟩
[GOAL]
case intro
y z : PartENat
hz : z ≠ ⊤
m : ℕ
h : ↑m < y
⊢ ↑m + z < y + z
[PROOFSTEP]
rcases ne_top_iff.mp hz with ⟨k, rfl⟩
[GOAL]
case intro.intro
y : PartENat
m : ℕ
h : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
⊢ ↑m + ↑k < y + ↑k
[PROOFSTEP]
induction' y using PartENat.casesOn with n
[GOAL]
case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
h : ↑m < ⊤
⊢ ↑m + ↑k < ⊤ + ↑k
[PROOFSTEP]
rw [top_add]
  -- Porting note: was apply_mod_cast natCast_lt_top
[GOAL]
case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
h : ↑m < ⊤
⊢ ↑m + ↑k < ⊤
[PROOFSTEP]
norm_cast
[GOAL]
case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
h : ↑m < ⊤
⊢ ↑(m + k) < ⊤
[PROOFSTEP]
apply natCast_lt_top
[GOAL]
case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
n : ℕ
h : ↑m < ↑n
⊢ ↑m + ↑k < ↑n + ↑k
[PROOFSTEP]
norm_cast at h
[GOAL]
case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
n : ℕ
h : m < n
⊢ ↑m + ↑k < ↑n + ↑k
[PROOFSTEP]
norm_cast
[GOAL]
case intro.intro.a
y : PartENat
m : ℕ
h✝ : ↑m < y
k : ℕ
hz : ↑k ≠ ⊤
n : ℕ
h : m < n
⊢ m + k < n + k
[PROOFSTEP]
apply add_lt_add_right h
[GOAL]
x y z : PartENat
hz : z ≠ ⊤
⊢ z + x < z + y ↔ x < y
[PROOFSTEP]
rw [add_comm z, add_comm z, PartENat.add_lt_add_iff_right hz]
[GOAL]
x y : PartENat
hx : x ≠ ⊤
⊢ x < x + y ↔ 0 < y
[PROOFSTEP]
conv_rhs => rw [← PartENat.add_lt_add_iff_left hx]
[GOAL]
x y : PartENat
hx : x ≠ ⊤
| 0 < y
[PROOFSTEP]
rw [← PartENat.add_lt_add_iff_left hx]
[GOAL]
x y : PartENat
hx : x ≠ ⊤
| 0 < y
[PROOFSTEP]
rw [← PartENat.add_lt_add_iff_left hx]
[GOAL]
x y : PartENat
hx : x ≠ ⊤
| 0 < y
[PROOFSTEP]
rw [← PartENat.add_lt_add_iff_left hx]
[GOAL]
x y : PartENat
hx : x ≠ ⊤
⊢ x < x + y ↔ x + 0 < x + y
[PROOFSTEP]
rw [add_zero]
[GOAL]
x : PartENat
hx : x ≠ ⊤
⊢ x < x + 1
[PROOFSTEP]
rw [PartENat.lt_add_iff_pos_right hx]
[GOAL]
x : PartENat
hx : x ≠ ⊤
⊢ 0 < 1
[PROOFSTEP]
norm_cast
[GOAL]
x y : PartENat
h : x < y + 1
⊢ x ≤ y
[PROOFSTEP]
induction' y using PartENat.casesOn with n
[GOAL]
case a
x y : PartENat
h✝ : x < y + 1
h : x < ⊤ + 1
⊢ x ≤ ⊤
[PROOFSTEP]
apply le_top
[GOAL]
case a
x y : PartENat
h✝ : x < y + 1
n : ℕ
h : x < ↑n + 1
⊢ x ≤ ↑n
[PROOFSTEP]
rcases ne_top_iff.mp (ne_top_of_lt h) with
  ⟨m, rfl⟩
    -- Porting note: was `apply_mod_cast Nat.le_of_lt_succ; apply_mod_cast h`
[GOAL]
case a.intro
y : PartENat
n m : ℕ
h✝ : ↑m < y + 1
h : ↑m < ↑n + 1
⊢ ↑m ≤ ↑n
[PROOFSTEP]
norm_cast
[GOAL]
case a.intro
y : PartENat
n m : ℕ
h✝ : ↑m < y + 1
h : ↑m < ↑n + 1
⊢ m ≤ n
[PROOFSTEP]
apply Nat.le_of_lt_succ
[GOAL]
case a.intro.a
y : PartENat
n m : ℕ
h✝ : ↑m < y + 1
h : ↑m < ↑n + 1
⊢ m < Nat.succ n
[PROOFSTEP]
norm_cast at h
[GOAL]
x y : PartENat
h : x < y
⊢ x + 1 ≤ y
[PROOFSTEP]
induction' y using PartENat.casesOn with n
[GOAL]
case a
x y : PartENat
h✝ : x < y
h : x < ⊤
⊢ x + 1 ≤ ⊤
[PROOFSTEP]
apply le_top
[GOAL]
case a
x y : PartENat
h✝ : x < y
n : ℕ
h : x < ↑n
⊢ x + 1 ≤ ↑n
[PROOFSTEP]
rcases ne_top_iff.mp (ne_top_of_lt h) with
  ⟨m, rfl⟩
    -- Porting note: was `apply_mod_cast Nat.succ_le_of_lt; apply_mod_cast h`
[GOAL]
case a.intro
y : PartENat
n m : ℕ
h✝ : ↑m < y
h : ↑m < ↑n
⊢ ↑m + 1 ≤ ↑n
[PROOFSTEP]
norm_cast
[GOAL]
case a.intro
y : PartENat
n m : ℕ
h✝ : ↑m < y
h : ↑m < ↑n
⊢ m + 1 ≤ n
[PROOFSTEP]
apply Nat.succ_le_of_lt
[GOAL]
case a.intro.h
y : PartENat
n m : ℕ
h✝ : ↑m < y
h : ↑m < ↑n
⊢ m < n
[PROOFSTEP]
norm_cast at h
[GOAL]
x y : PartENat
hx : x ≠ ⊤
⊢ x + 1 ≤ y ↔ x < y
[PROOFSTEP]
refine ⟨fun h => ?_, add_one_le_of_lt⟩
[GOAL]
x y : PartENat
hx : x ≠ ⊤
h : x + 1 ≤ y
⊢ x < y
[PROOFSTEP]
rcases ne_top_iff.mp hx with ⟨m, rfl⟩
[GOAL]
case intro
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h : ↑m + 1 ≤ y
⊢ ↑m < y
[PROOFSTEP]
induction' y using PartENat.casesOn with n
[GOAL]
case intro.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m + 1 ≤ y
h : ↑m + 1 ≤ ⊤
⊢ ↑m < ⊤
[PROOFSTEP]
apply natCast_lt_top
[GOAL]
case intro.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m + 1 ≤ y
n : ℕ
h : ↑m + 1 ≤ ↑n
⊢ ↑m < ↑n
[PROOFSTEP]
norm_cast
[GOAL]
case intro.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m + 1 ≤ y
n : ℕ
h : ↑m + 1 ≤ ↑n
⊢ m < n
[PROOFSTEP]
apply Nat.lt_of_succ_le
[GOAL]
case intro.a.h
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m + 1 ≤ y
n : ℕ
h : ↑m + 1 ≤ ↑n
⊢ Nat.succ m ≤ n
[PROOFSTEP]
norm_cast at h
[GOAL]
n : ℕ
e : PartENat
⊢ ↑(Nat.succ n) ≤ e ↔ ↑n < e
[PROOFSTEP]
rw [Nat.succ_eq_add_one n, Nat.cast_add, Nat.cast_one, add_one_le_iff_lt (natCast_ne_top n)]
[GOAL]
x y : PartENat
hx : x ≠ ⊤
⊢ x < y + 1 ↔ x ≤ y
[PROOFSTEP]
refine ⟨le_of_lt_add_one, fun h => ?_⟩
[GOAL]
x y : PartENat
hx : x ≠ ⊤
h : x ≤ y
⊢ x < y + 1
[PROOFSTEP]
rcases ne_top_iff.mp hx with ⟨m, rfl⟩
[GOAL]
case intro
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h : ↑m ≤ y
⊢ ↑m < y + 1
[PROOFSTEP]
induction' y using PartENat.casesOn with n
[GOAL]
case intro.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m ≤ y
h : ↑m ≤ ⊤
⊢ ↑m < ⊤ + 1
[PROOFSTEP]
rw [top_add]
[GOAL]
case intro.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m ≤ y
h : ↑m ≤ ⊤
⊢ ↑m < ⊤
[PROOFSTEP]
apply natCast_lt_top
[GOAL]
case intro.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m ≤ y
n : ℕ
h : ↑m ≤ ↑n
⊢ ↑m < ↑n + 1
[PROOFSTEP]
norm_cast
[GOAL]
case intro.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m ≤ y
n : ℕ
h : ↑m ≤ ↑n
⊢ m < n + 1
[PROOFSTEP]
apply Nat.lt_succ_of_le
[GOAL]
case intro.a.a
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h✝ : ↑m ≤ y
n : ℕ
h : ↑m ≤ ↑n
⊢ m ≤ n
[PROOFSTEP]
norm_cast at h
[GOAL]
x : PartENat
n : ℕ
hx : x ≠ ⊤
⊢ x < ↑(Nat.succ n) ↔ x ≤ ↑n
[PROOFSTEP]
rw [Nat.succ_eq_add_one n, Nat.cast_add, Nat.cast_one, lt_add_one_iff_lt hx]
[GOAL]
a b : PartENat
⊢ a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤
[PROOFSTEP]
refine PartENat.casesOn a ?_ ?_
[GOAL]
case refine_1
a b : PartENat
⊢ ⊤ + b = ⊤ ↔ ⊤ = ⊤ ∨ b = ⊤
[PROOFSTEP]
refine PartENat.casesOn b ?_ ?_
[GOAL]
case refine_2
a b : PartENat
⊢ ∀ (n : ℕ), ↑n + b = ⊤ ↔ ↑n = ⊤ ∨ b = ⊤
[PROOFSTEP]
refine PartENat.casesOn b ?_ ?_
[GOAL]
case refine_1.refine_1
a b : PartENat
⊢ ⊤ + ⊤ = ⊤ ↔ ⊤ = ⊤ ∨ ⊤ = ⊤
[PROOFSTEP]
simp
[GOAL]
case refine_1.refine_2
a b : PartENat
⊢ ∀ (n : ℕ), ⊤ + ↑n = ⊤ ↔ ⊤ = ⊤ ∨ ↑n = ⊤
[PROOFSTEP]
simp
[GOAL]
case refine_2.refine_1
a b : PartENat
⊢ ∀ (n : ℕ), ↑n + ⊤ = ⊤ ↔ ↑n = ⊤ ∨ ⊤ = ⊤
[PROOFSTEP]
simp
[GOAL]
case refine_2.refine_2
a b : PartENat
⊢ ∀ (n n_1 : ℕ), ↑n_1 + ↑n = ⊤ ↔ ↑n_1 = ⊤ ∨ ↑n = ⊤
[PROOFSTEP]
simp
[GOAL]
case refine_2.refine_2
a b : PartENat
⊢ ∀ (n n_1 : ℕ), ¬↑n_1 + ↑n = ⊤
[PROOFSTEP]
simp only [← Nat.cast_add, PartENat.natCast_ne_top, forall_const]
[GOAL]
a b c : PartENat
hc : c ≠ ⊤
⊢ a + c = b + c ↔ a = b
[PROOFSTEP]
rcases ne_top_iff.1 hc with ⟨c, rfl⟩
[GOAL]
case intro
a b : PartENat
c : ℕ
hc : ↑c ≠ ⊤
⊢ a + ↑c = b + ↑c ↔ a = b
[PROOFSTEP]
refine PartENat.casesOn a ?_ ?_
[GOAL]
case intro.refine_1
a b : PartENat
c : ℕ
hc : ↑c ≠ ⊤
⊢ ⊤ + ↑c = b + ↑c ↔ ⊤ = b
[PROOFSTEP]
refine PartENat.casesOn b ?_ ?_
[GOAL]
case intro.refine_2
a b : PartENat
c : ℕ
hc : ↑c ≠ ⊤
⊢ ∀ (n : ℕ), ↑n + ↑c = b + ↑c ↔ ↑n = b
[PROOFSTEP]
refine PartENat.casesOn b ?_ ?_
[GOAL]
case intro.refine_1.refine_1
a b : PartENat
c : ℕ
hc : ↑c ≠ ⊤
⊢ ⊤ + ↑c = ⊤ + ↑c ↔ ⊤ = ⊤
[PROOFSTEP]
simp [add_eq_top_iff, natCast_ne_top, @eq_comm _ (⊤ : PartENat)]
[GOAL]
case intro.refine_1.refine_2
a b : PartENat
c : ℕ
hc : ↑c ≠ ⊤
⊢ ∀ (n : ℕ), ⊤ + ↑c = ↑n + ↑c ↔ ⊤ = ↑n
[PROOFSTEP]
simp [add_eq_top_iff, natCast_ne_top, @eq_comm _ (⊤ : PartENat)]
[GOAL]
case intro.refine_2.refine_1
a b : PartENat
c : ℕ
hc : ↑c ≠ ⊤
⊢ ∀ (n : ℕ), ↑n + ↑c = ⊤ + ↑c ↔ ↑n = ⊤
[PROOFSTEP]
simp [add_eq_top_iff, natCast_ne_top, @eq_comm _ (⊤ : PartENat)]
[GOAL]
case intro.refine_2.refine_2
a b : PartENat
c : ℕ
hc : ↑c ≠ ⊤
⊢ ∀ (n n_1 : ℕ), ↑n_1 + ↑c = ↑n + ↑c ↔ ↑n_1 = ↑n
[PROOFSTEP]
simp [add_eq_top_iff, natCast_ne_top, @eq_comm _ (⊤ : PartENat)]
[GOAL]
case intro.refine_2.refine_2
a b : PartENat
c : ℕ
hc : ↑c ≠ ⊤
⊢ ∀ (n n_1 : ℕ), ↑n_1 + ↑c = ↑n + ↑c ↔ n_1 = n
[PROOFSTEP]
simp only [← Nat.cast_add, add_left_cancel_iff, PartENat.natCast_inj, add_comm, forall_const]
[GOAL]
a b c : PartENat
ha : a ≠ ⊤
⊢ a + b = a + c ↔ b = c
[PROOFSTEP]
rw [add_comm a, add_comm a, PartENat.add_right_cancel_iff ha]
[GOAL]
h : Decidable ⊤.Dom
⊢ toWithTop ⊤ = ⊤
[PROOFSTEP]
convert toWithTop_top
[GOAL]
h : Decidable 0.Dom
⊢ toWithTop 0 = 0
[PROOFSTEP]
convert toWithTop_zero
[GOAL]
n : ℕ
x✝ : Decidable (↑n).Dom
⊢ toWithTop ↑n = ↑n
[PROOFSTEP]
simp only [← toWithTop_some]
[GOAL]
n : ℕ
x✝ : Decidable (↑n).Dom
⊢ toWithTop ↑n = toWithTop ↑n
[PROOFSTEP]
congr
[GOAL]
n : ℕ
h : Decidable (↑n).Dom
⊢ toWithTop ↑n = ↑n
[PROOFSTEP]
rw [toWithTop_natCast n]
[GOAL]
x y : PartENat
hx : Decidable x.Dom
hy : Decidable y.Dom
⊢ toWithTop x ≤ toWithTop y ↔ x ≤ y
[PROOFSTEP]
induction y using PartENat.casesOn generalizing hy
[GOAL]
case a
x : PartENat
hx : Decidable x.Dom
hy : Decidable ⊤.Dom
⊢ toWithTop x ≤ toWithTop ⊤ ↔ x ≤ ⊤
[PROOFSTEP]
simp
[GOAL]
case a
x : PartENat
hx : Decidable x.Dom
n✝ : ℕ
hy : Decidable (↑n✝).Dom
⊢ toWithTop x ≤ toWithTop ↑n✝ ↔ x ≤ ↑n✝
[PROOFSTEP]
induction x using PartENat.casesOn generalizing hx
[GOAL]
case a.a
n✝ : ℕ
hy : Decidable (↑n✝).Dom
hx : Decidable ⊤.Dom
⊢ toWithTop ⊤ ≤ toWithTop ↑n✝ ↔ ⊤ ≤ ↑n✝
[PROOFSTEP]
simp
[GOAL]
case a.a
n✝¹ : ℕ
hy : Decidable (↑n✝¹).Dom
n✝ : ℕ
hx : Decidable (↑n✝).Dom
⊢ toWithTop ↑n✝ ≤ toWithTop ↑n✝¹ ↔ ↑n✝ ≤ ↑n✝¹
[PROOFSTEP]
simp
  -- Porting note: this takes too long.
[GOAL]
⊢ ↑Option.none = ⊤
[PROOFSTEP]
rfl
  -- Porting note : new
[GOAL]
n : ℕ
⊢ ↑(Option.some n) = ↑n
[PROOFSTEP]
rfl
  -- Porting note : new
[GOAL]
n : ℕ∞
x✝ : Decidable (↑n).Dom
⊢ toWithTop ↑n = n
[PROOFSTEP]
induction n with
| none => simp
| some n =>
  simp only [toWithTop_natCast', ofENat_some]
  rfl
[GOAL]
n : ℕ∞
x✝ : Decidable (↑n).Dom
⊢ toWithTop ↑n = n
[PROOFSTEP]
induction n with
| none => simp
| some n =>
  simp only [toWithTop_natCast', ofENat_some]
  rfl
[GOAL]
case none
x✝ : Decidable (↑Option.none).Dom
⊢ toWithTop ↑Option.none = Option.none
[PROOFSTEP]

| none => simp
[GOAL]
case none
x✝ : Decidable (↑Option.none).Dom
⊢ toWithTop ↑Option.none = Option.none
[PROOFSTEP]
simp
[GOAL]
case some
n : ℕ
x✝ : Decidable (↑(Option.some n)).Dom
⊢ toWithTop ↑(Option.some n) = Option.some n
[PROOFSTEP]

| some n =>
  simp only [toWithTop_natCast', ofENat_some]
  rfl
[GOAL]
case some
n : ℕ
x✝ : Decidable (↑(Option.some n)).Dom
⊢ toWithTop ↑(Option.some n) = Option.some n
[PROOFSTEP]
simp only [toWithTop_natCast', ofENat_some]
[GOAL]
case some
n : ℕ
x✝ : Decidable (↑(Option.some n)).Dom
⊢ ↑n = Option.some n
[PROOFSTEP]
rfl
[GOAL]
x y : PartENat
⊢ toWithTop (x + y) = toWithTop x + toWithTop y
[PROOFSTEP]
refine PartENat.casesOn y ?_ ?_
[GOAL]
case refine_1
x y : PartENat
⊢ toWithTop (x + ⊤) = toWithTop x + toWithTop ⊤
[PROOFSTEP]
refine
  PartENat.casesOn x ?_
    ?_
      --Porting note: was `simp [← Nat.cast_add, ← ENat.coe_add]`
[GOAL]
case refine_2
x y : PartENat
⊢ ∀ (n : ℕ), toWithTop (x + ↑n) = toWithTop x + toWithTop ↑n
[PROOFSTEP]
refine
  PartENat.casesOn x ?_
    ?_
      --Porting note: was `simp [← Nat.cast_add, ← ENat.coe_add]`
[GOAL]
case refine_1.refine_1
x y : PartENat
⊢ toWithTop (⊤ + ⊤) = toWithTop ⊤ + toWithTop ⊤
[PROOFSTEP]
simp only [add_top, toWithTop_top', _root_.add_top]
[GOAL]
case refine_1.refine_2
x y : PartENat
⊢ ∀ (n : ℕ), toWithTop (↑n + ⊤) = toWithTop ↑n + toWithTop ⊤
[PROOFSTEP]
simp only [add_top, toWithTop_top', toWithTop_natCast', _root_.add_top, forall_const]
[GOAL]
case refine_2.refine_1
x y : PartENat
⊢ ∀ (n : ℕ), toWithTop (⊤ + ↑n) = toWithTop ⊤ + toWithTop ↑n
[PROOFSTEP]
simp only [top_add, toWithTop_top', toWithTop_natCast', _root_.top_add, forall_const]
[GOAL]
case refine_2.refine_2
x y : PartENat
⊢ ∀ (n n_1 : ℕ), toWithTop (↑n + ↑n_1) = toWithTop ↑n + toWithTop ↑n_1
[PROOFSTEP]
simp_rw [toWithTop_natCast', ← Nat.cast_add, toWithTop_natCast', forall_const]
[GOAL]
x : PartENat
⊢ (fun x => ↑x) ((fun x => toWithTop x) x) = x
[PROOFSTEP]
induction x using PartENat.casesOn
[GOAL]
case a
⊢ (fun x => ↑x) ((fun x => toWithTop x) ⊤) = ⊤
[PROOFSTEP]
intros
[GOAL]
case a
n✝ : ℕ
⊢ (fun x => ↑x) ((fun x => toWithTop x) ↑n✝) = ↑n✝
[PROOFSTEP]
intros
[GOAL]
case a
⊢ (fun x => ↑x) ((fun x => toWithTop x) ⊤) = ⊤
[PROOFSTEP]
simp
[GOAL]
case a
n✝ : ℕ
⊢ (fun x => ↑x) ((fun x => toWithTop x) ↑n✝) = ↑n✝
[PROOFSTEP]
simp
[GOAL]
case a
⊢ ↑⊤ = ⊤
[PROOFSTEP]
rfl
[GOAL]
case a
n✝ : ℕ
⊢ ↑↑n✝ = ↑n✝
[PROOFSTEP]
rfl
[GOAL]
x : ℕ∞
⊢ (fun x => toWithTop x) ((fun x => ↑x) x) = x
[PROOFSTEP]
simp [toWithTop_ofENat]
[GOAL]
⊢ ↑withTopEquiv 0 = 0
[PROOFSTEP]
simpa only [Nat.cast_zero] using withTopEquiv_natCast 0
[GOAL]
x y : ℕ∞
⊢ ↑withTopEquiv.symm x ≤ ↑withTopEquiv.symm y ↔ x ≤ y
[PROOFSTEP]
rw [← withTopEquiv_le]
[GOAL]
x y : ℕ∞
⊢ ↑withTopEquiv (↑withTopEquiv.symm x) ≤ ↑withTopEquiv (↑withTopEquiv.symm y) ↔ x ≤ y
[PROOFSTEP]
simp
[GOAL]
x y : ℕ∞
⊢ ↑withTopEquiv.symm x < ↑withTopEquiv.symm y ↔ x < y
[PROOFSTEP]
rw [← withTopEquiv_lt]
[GOAL]
x y : ℕ∞
⊢ ↑withTopEquiv (↑withTopEquiv.symm x) < ↑withTopEquiv (↑withTopEquiv.symm y) ↔ x < y
[PROOFSTEP]
simp
[GOAL]
src✝ : PartENat ≃ ℕ∞ := withTopEquiv
x y : PartENat
⊢ Equiv.toFun
      { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (x + y) =
    Equiv.toFun
        { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        x +
      Equiv.toFun
        { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        y
[PROOFSTEP]
simp only [withTopEquiv]
[GOAL]
src✝ : PartENat ≃ ℕ∞ := withTopEquiv
x y : PartENat
⊢ toWithTop (x + y) = toWithTop x + toWithTop y
[PROOFSTEP]
exact toWithTop_add
[GOAL]
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
classical
change WellFounded fun a b : PartENat => a < b
simp_rw [← withTopEquiv_lt]
exact InvImage.wf _ (WithTop.wellFounded_lt Nat.lt_wfRel.wf)
[GOAL]
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
change WellFounded fun a b : PartENat => a < b
[GOAL]
⊢ WellFounded fun a b => a < b
[PROOFSTEP]
simp_rw [← withTopEquiv_lt]
[GOAL]
⊢ WellFounded fun a b => ↑withTopEquiv a < ↑withTopEquiv b
[PROOFSTEP]
exact InvImage.wf _ (WithTop.wellFounded_lt Nat.lt_wfRel.wf)
[GOAL]
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ (m : ℕ), m ≤ n → ¬P m
⊢ ↑n < find P
[PROOFSTEP]
rw [coe_lt_iff]
[GOAL]
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ (m : ℕ), m ≤ n → ¬P m
⊢ ∀ (h : (find P).Dom), n < Part.get (find P) h
[PROOFSTEP]
intro h₁
[GOAL]
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ (m : ℕ), m ≤ n → ¬P m
h₁ : (find P).Dom
⊢ n < Part.get (find P) h₁
[PROOFSTEP]
rw [find_get]
[GOAL]
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ (m : ℕ), m ≤ n → ¬P m
h₁ : (find P).Dom
⊢ n < Nat.find h₁
[PROOFSTEP]
have h₂ := @Nat.find_spec P _ h₁
[GOAL]
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ (m : ℕ), m ≤ n → ¬P m
h₁ : (find P).Dom
h₂ : P (Nat.find h₁)
⊢ n < Nat.find h₁
[PROOFSTEP]
revert h₂
[GOAL]
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ (m : ℕ), m ≤ n → ¬P m
h₁ : (find P).Dom
⊢ P (Nat.find h₁) → n < Nat.find h₁
[PROOFSTEP]
contrapose!
[GOAL]
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ (m : ℕ), m ≤ n → ¬P m
h₁ : (find P).Dom
⊢ Nat.find h₁ ≤ n → ¬P (Nat.find h₁)
[PROOFSTEP]
exact h _
[GOAL]
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ ↑n < find P ↔ ∀ (m : ℕ), m ≤ n → ¬P m
[PROOFSTEP]
refine' ⟨_, lt_find P n⟩
[GOAL]
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ ↑n < find P → ∀ (m : ℕ), m ≤ n → ¬P m
[PROOFSTEP]
intro h m hm
[GOAL]
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
⊢ ¬P m
[PROOFSTEP]
by_cases H : (find P).Dom
[GOAL]
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
H : (find P).Dom
⊢ ¬P m
[PROOFSTEP]
apply Nat.find_min H
[GOAL]
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
H : (find P).Dom
⊢ m < Nat.find H
[PROOFSTEP]
rw [coe_lt_iff] at h
[GOAL]
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ (h : (find P).Dom), n < Part.get (find P) h
m : ℕ
hm : m ≤ n
H : (find P).Dom
⊢ m < Nat.find H
[PROOFSTEP]
specialize h H
[GOAL]
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n m : ℕ
hm : m ≤ n
H : (find P).Dom
h : n < Part.get (find P) H
⊢ m < Nat.find H
[PROOFSTEP]
exact lt_of_le_of_lt hm h
[GOAL]
case neg
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
H : ¬(find P).Dom
⊢ ¬P m
[PROOFSTEP]
exact not_exists.mp H m
[GOAL]
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : P n
⊢ find P ≤ ↑n
[PROOFSTEP]
rw [le_coe_iff]
[GOAL]
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : P n
⊢ ∃ h, Part.get (find P) h ≤ n
[PROOFSTEP]
refine' ⟨⟨_, h⟩, @Nat.find_min' P _ _ _ h⟩


[GOAL]
n m : ℕ
⊢ dist n m = dist m n
[PROOFSTEP]
simp [dist.def, add_comm]
[GOAL]
n : ℕ
⊢ dist n n = 0
[PROOFSTEP]
simp [dist.def, tsub_self]
[GOAL]
n m : ℕ
h : n = m
⊢ dist n m = 0
[PROOFSTEP]
rw [h, dist_self]
[GOAL]
n m : ℕ
h : n ≤ m
⊢ dist n m = m - n
[PROOFSTEP]
rw [dist.def, tsub_eq_zero_iff_le.mpr h, zero_add]
[GOAL]
n m : ℕ
h : m ≤ n
⊢ dist n m = n - m
[PROOFSTEP]
rw [dist_comm]
[GOAL]
n m : ℕ
h : m ≤ n
⊢ dist m n = n - m
[PROOFSTEP]
apply dist_eq_sub_of_le h
[GOAL]
n m : ℕ
⊢ m ≤ n + dist n m
[PROOFSTEP]
rw [add_comm]
[GOAL]
n m : ℕ
⊢ m ≤ dist n m + n
[PROOFSTEP]
apply dist_tri_left
[GOAL]
n m : ℕ
⊢ n ≤ dist n m + m
[PROOFSTEP]
rw [dist_comm]
[GOAL]
n m : ℕ
⊢ n ≤ dist m n + m
[PROOFSTEP]
apply dist_tri_left
[GOAL]
n m : ℕ
⊢ n ≤ m + dist n m
[PROOFSTEP]
rw [dist_comm]
[GOAL]
n m : ℕ
⊢ n ≤ m + dist m n
[PROOFSTEP]
apply dist_tri_right
[GOAL]
n k m : ℕ
⊢ n + k - (m + k) + (m + k - (n + k)) = n - m + (m + k - (n + k))
[PROOFSTEP]
rw [@add_tsub_add_eq_tsub_right]
[GOAL]
n k m : ℕ
⊢ n - m + (m + k - (n + k)) = n - m + (m - n)
[PROOFSTEP]
rw [@add_tsub_add_eq_tsub_right]
[GOAL]
k n m : ℕ
⊢ dist (k + n) (k + m) = dist n m
[PROOFSTEP]
rw [add_comm k n, add_comm k m]
[GOAL]
k n m : ℕ
⊢ dist (n + k) (m + k) = dist n m
[PROOFSTEP]
apply dist_add_add_right
[GOAL]
n m k l : ℕ
h : n + m = k + l
⊢ dist n k = dist (n + m) (k + m)
[PROOFSTEP]
rw [dist_add_add_right]
[GOAL]
n m k l : ℕ
h : n + m = k + l
⊢ dist (n + m) (k + m) = dist (k + l) (k + m)
[PROOFSTEP]
rw [h]
[GOAL]
n m k l : ℕ
h : n + m = k + l
⊢ dist (k + l) (k + m) = dist l m
[PROOFSTEP]
rw [dist_add_add_left]
[GOAL]
n m k : ℕ
⊢ dist n k ≤ dist n m + dist m k
[PROOFSTEP]
have : dist n m + dist m k = n - m + (m - k) + (k - m + (m - n)) := by
  simp [dist.def, add_comm, add_left_comm, add_assoc]
[GOAL]
n m k : ℕ
⊢ dist n m + dist m k = n - m + (m - k) + (k - m + (m - n))
[PROOFSTEP]
simp [dist.def, add_comm, add_left_comm, add_assoc]
[GOAL]
n m k : ℕ
this : dist n m + dist m k = n - m + (m - k) + (k - m + (m - n))
⊢ dist n k ≤ dist n m + dist m k
[PROOFSTEP]
rw [this, dist.def]
[GOAL]
n m k : ℕ
this : dist n m + dist m k = n - m + (m - k) + (k - m + (m - n))
⊢ n - k + (k - n) ≤ n - m + (m - k) + (k - m + (m - n))
[PROOFSTEP]
exact add_le_add tsub_le_tsub_add_tsub tsub_le_tsub_add_tsub
[GOAL]
n k m : ℕ
⊢ dist (n * k) (m * k) = dist n m * k
[PROOFSTEP]
rw [dist.def, dist.def, right_distrib, tsub_mul n, tsub_mul m]
[GOAL]
k n m : ℕ
⊢ dist (k * n) (k * m) = k * dist n m
[PROOFSTEP]
rw [mul_comm k n, mul_comm k m, dist_mul_right, mul_comm]
[GOAL]
i j : ℕ
⊢ i < j → dist i j = max i j - min i j
[PROOFSTEP]
intro h
[GOAL]
i j : ℕ
h : i < j
⊢ dist i j = max i j - min i j
[PROOFSTEP]
rw [max_eq_right_of_lt h, min_eq_left_of_lt h, dist_eq_sub_of_le (Nat.le_of_lt h)]
[GOAL]
i j : ℕ
⊢ i ≥ j → dist i j = max i j - min i j
[PROOFSTEP]
intro h
[GOAL]
i j : ℕ
h : i ≥ j
⊢ dist i j = max i j - min i j
[PROOFSTEP]
rw [max_eq_left h, min_eq_right h, dist_eq_sub_of_le_right h]
[GOAL]
i j : ℕ
⊢ dist (succ i) (succ j) = dist i j
[PROOFSTEP]
simp [dist.def, succ_sub_succ]
[GOAL]
i j : ℕ
hne : i ≠ j
h : i < j
⊢ 0 < dist i j
[PROOFSTEP]
rw [dist_eq_sub_of_le (le_of_lt h)]
[GOAL]
i j : ℕ
hne : i ≠ j
h : i < j
⊢ 0 < j - i
[PROOFSTEP]
apply tsub_pos_of_lt h
[GOAL]
i j : ℕ
hne : i ≠ j
h : i = j
⊢ 0 < dist i j
[PROOFSTEP]
contradiction
[GOAL]
i j : ℕ
hne : i ≠ j
h : i > j
⊢ 0 < dist i j
[PROOFSTEP]
rw [dist_eq_sub_of_le_right (le_of_lt h)]
[GOAL]
i j : ℕ
hne : i ≠ j
h : i > j
⊢ 0 < i - j
[PROOFSTEP]
apply tsub_pos_of_lt h


[GOAL]
a b : PosNum
⊢ Decidable ((fun x x_1 => x < x_1) a b)
[PROOFSTEP]
dsimp [LT.lt]
[GOAL]
a b : PosNum
⊢ Decidable (cmp a b = lt)
[PROOFSTEP]
infer_instance
[GOAL]
a b : PosNum
⊢ Decidable ((fun x x_1 => x ≤ x_1) a b)
[PROOFSTEP]
dsimp [LE.le]
[GOAL]
a b : PosNum
⊢ Decidable ¬b < a
[PROOFSTEP]
infer_instance
[GOAL]
a b : Num
⊢ Decidable ((fun x x_1 => x < x_1) a b)
[PROOFSTEP]
dsimp [LT.lt]
[GOAL]
a b : Num
⊢ Decidable (cmp a b = lt)
[PROOFSTEP]
infer_instance
[GOAL]
a b : Num
⊢ Decidable ((fun x x_1 => x ≤ x_1) a b)
[PROOFSTEP]
dsimp [LE.le]
[GOAL]
a b : Num
⊢ Decidable ¬b < a
[PROOFSTEP]
infer_instance
[GOAL]
a b : ZNum
⊢ Decidable ((fun x x_1 => x < x_1) a b)
[PROOFSTEP]
dsimp [LT.lt]
[GOAL]
a b : ZNum
⊢ Decidable (cmp a b = lt)
[PROOFSTEP]
infer_instance
[GOAL]
a b : ZNum
⊢ Decidable ((fun x x_1 => x ≤ x_1) a b)
[PROOFSTEP]
dsimp [LE.le]
[GOAL]
a b : ZNum
⊢ Decidable ¬b < a
[PROOFSTEP]
infer_instance