x : PartENat
n : ℕ
⊢ (∃ h, ∀ (hy : (↑n).Dom), Part.get x (_ : x.Dom) ≤ Part.get (↑n) hy) ↔ ∃ h, Part.get x h ≤ n
x : PartENat
n : ℕ
⊢ x ≤ ↑n ↔ ∃ h, Part.get x h ≤ n
show (∃ h : True → x.Dom, _) ↔ ∃ h : x.Dom, x.get h ≤ n
no goals
x : PartENat
n : ℕ
⊢ (∃ h, ∀ (hy : (↑n).Dom), Part.get x (_ : x.Dom) ≤ Part.get (↑n) hy) ↔ ∃ h, Part.get x h ≤ n
simp only [forall_prop_of_true, dom_natCast, get_natCast']