n : ℕ
x : PartENat
⊢ ↑n ≤ x ↔ ∀ (h : x.Dom), n ≤ Part.get x h
n : ℕ
x : PartENat
⊢ ↑n ≤ x ↔ ∀ (h : x.Dom), n ≤ Part.get x h
rw [← some_eq_natCast]
n : ℕ
x : PartENat
⊢ (∀ (hy : x.Dom), Part.get ↑n (_ : (↑n).Dom) ≤ Part.get x hy) ↔ ∀ (h : x.Dom), n ≤ Part.get x h
n : ℕ
x : PartENat
⊢ ↑n ≤ x ↔ ∀ (h : x.Dom), n ≤ Part.get x h
simp only [le_def, exists_prop_of_true, dom_some, forall_true_iff]
no goals
n : ℕ
x : PartENat
⊢ (∀ (hy : x.Dom), Part.get ↑n (_ : (↑n).Dom) ≤ Part.get x hy) ↔ ∀ (h : x.Dom), n ≤ Part.get x h
rfl