funny error on line 59

gistfile1.txt

import analysis.real 

def S (a : {n : ℕ // n ≥ 1} → ℝ) 
  (n : ℕ) (H : n ≥ 1) := { r: ℝ | ∃ (m : ℕ) (Hm : m ≥ n), r = a ⟨m,ge_trans Hm H⟩ }

noncomputable def a2 : {n : ℕ // n ≥ 1} → ℝ := λ N, 1/N.val 

def liminf (a : {n : ℕ // n ≥ 1} → ℝ) (linf : ℝ) : Prop :=
  ∃ c : { n : ℕ // n ≥ 1} → ℝ, is_lub { x : ℝ | ∃ (n : ℕ) (H : n ≥ 1), x = c ⟨n,H⟩} linf 
  ∧ ∀ (n : ℕ) (H : n ≥ 1), is_glb (S a n H) (c ⟨n,H⟩) 

set_option pp.all true 
  
theorem Q6c2' : liminf a2 0 :=
begin
existsi (λ _,(0:ℝ)),
split,
{ split,
  { 
  intros x Hx,
  cases Hx with m Hm,
  cases Hm with H1 H2,
  rw H2,
  exact le_refl _,
  },
  intros y Hy,
  apply Hy,
  existsi 1,
  existsi _,refl,
  show 1 ≤ 1,
  exact le_refl _
},
intros n Hn,
split,
{ intros x Hx,
  cases Hx with m Hm,
  cases Hm with H1 H2,
  show 0 ≤ x,
  rw H2,
  unfold a2,
  show 0 ≤ 1/(↑m:ℝ),
  rw [←inv_eq_one_div],
  apply le_of_lt _,
  apply inv_pos,
  rw [←nat.cast_zero,nat.cast_lt],
  exact calc 0 < 1 : zero_lt_one ... ≤ n : Hn ... ≤ m : H1
},
intros x Hx,
show x ≤ 0,
    refine not_lt.1 _,
    intro Hny,
    cases (exists_lt_nat (max (1/x) n)) with m Hm,
    have H1 := Hx (1/m),
    rw ←inv_eq_one_div at Hm,
    have H2 : n ≤ m,
    { suffices : ↑n < (↑m:ℝ),exact le_of_lt (nat.cast_lt.1 this), exact lt_of_le_of_lt (le_max_right _ _) Hm },
    have H2' : m ≥ 1,
    { refine le_trans Hn _, exact H2},
    have H4 : 1 / (↑m:ℝ) ∈ {x : ℝ | ∃ (m : ℕ) (H : m ≥ n), x = a2 ⟨m, H2'⟩},
    admit,
end